Seminars for Pure Mathematics
Jan 19 2023 |
Ettore Aldrovandi (FSU) |
Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory |
Algebra and its Applications |
Time: 3:05 pm |
Location: LOV 0105 |
I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No... More |
Jan 26 2023 |
Ettore Aldrovandi (FSU) |
Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory (Part II) |
Algebra and its Applications |
Time: 3:05 pm |
Location: 0102 LOV |
I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No... More |