Andrej Bauer: Kan simplicial sets – what's their problem?

Datum objave: 2. 12. 2013
Seminar za temelje matematike in teoretično računalništvo
Torek, 3. 12. 2013, od 12h do 14h, Plemljev seminar, Jadranska 21
Abstract: Kan simplicial sets are (essentially) the only known model of homotopy type theory which validates the univalence axiom, due to a result of Voevodsky. A major stumbling block in giving a computable interpretation of the univalence axiom is the fact that it seems hard to constructivize Kan simplicial sets. In this talk we shall scrutinize the classical construction and pinpoint the places where the law of excluded middle is used.