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

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.