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