Egbert Rijke: Finite mathematics in homotopy type theory

Abstract: In homotopy type theory, equivalent types are equal. It follows that isomorphic groups are equal, and in particular that isomorphic finite groups are equal. Therefore we can count the number of isomorphism classes of finite groups of a fixed cardinality by counting the number of connected components in the type of all finite groups of that cardinality. In this talk I will present some work in progress and formalisations towards counting finite structures up to isomorphism with the help of the univalence axiom.