The law of excluded middle in the simplicial model of type theory
arXiv:2006.13694
Abstract
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.
Short note, 2 pages. v2: various revisions, no change in numbering