FSUMATH
Florida State University Seal

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