Egbert Rijke: Finite mathematics in homotopy type theory

Datum objave: 21. 1. 2021
Seminar za temelje matematike in teoretično računalništvo
četrtek
21
januar
Ura:
10.00 - 12.00
Lokacija:
Zoom
ID: 989 0478 8985

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.