The law of excluded middle in the simplicial model of type theory

Chris Kapulkin and Peter LeFanu Lumsdaine

We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.

Keywords: Univalent foundations, homotopy type theory, simplicial sets, law of excluded middle, dependent type theory

2020 MSC: 03B15 (primary), 55U10, 18C50

Theory and Applications of Categories, Vol. 35, 2020, No. 40, pp 1546-1548.

Published 2020-09-03.

TAC Home