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

Date of publication: 2. 12. 2013

Mathematics and theoretical computing seminar

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.