Geodesic
The law of excluded middle in the simplicial model of type theory
Theory and applications of categories, Tome 35 (2020), pp. 1546-1548

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Publié le :
Classification : 03B15 (primary), 55U10, 18C50
Keywords: Univalent foundations, homotopy type theory, simplicial sets, law of excluded middle, dependent type theory 
Chris Kapulkin; Peter LeFanu Lumsdaine. The law of excluded middle in the simplicial model of type theory. Theory and applications of categories, Tome 35 (2020), pp. 1546-1548. http://geodesic.mathdoc.fr/item/TAC_2020_35_a39/
@article{TAC_2020_35_a39,
     author = {Chris Kapulkin and Peter LeFanu Lumsdaine},
     title = {The law of excluded middle in the simplicial model of type theory},
     journal = {Theory and applications of categories},
     pages = {1546--1548},
     year = {2020},
     volume = {35},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2020_35_a39/}
}
TY  - JOUR
AU  - Chris Kapulkin
AU  - Peter LeFanu Lumsdaine
TI  - The law of excluded middle in the simplicial model of type theory
JO  - Theory and applications of categories
PY  - 2020
SP  - 1546
EP  - 1548
VL  - 35
UR  - http://geodesic.mathdoc.fr/item/TAC_2020_35_a39/
LA  - en
ID  - TAC_2020_35_a39
ER  - 
%0 Journal Article
%A Chris Kapulkin
%A Peter LeFanu Lumsdaine
%T The law of excluded middle in the simplicial model of type theory
%J Theory and applications of categories
%D 2020
%P 1546-1548
%V 35
%U http://geodesic.mathdoc.fr/item/TAC_2020_35_a39/
%G en
%F TAC_2020_35_a39