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 
@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},
     publisher = {mathdoc},
     volume = {35},
     year = {2020},
     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
PB  - mathdoc
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
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2020_35_a39/
%G en
%F TAC_2020_35_a39
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/