The Simplicial Model of Univalent Foundations (after Voevodsky)
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2012
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910012291416064 |
|---|---|
| author | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| author_facet | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| contents | We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets.
To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model.
As a corollary, we conclude that Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1211_2851 |
| institution | arXiv |
| publishDate | 2012 |
| record_format | arxiv |
| spellingShingle | The Simplicial Model of Univalent Foundations (after Voevodsky) Kapulkin, Chris Lumsdaine, Peter LeFanu Logic Algebraic Topology Category Theory 03B15, 55U10 (Primary), 18C50, 55U35 (Secondary) We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals. |
| title | The Simplicial Model of Univalent Foundations (after Voevodsky) |
| topic | Logic Algebraic Topology Category Theory 03B15, 55U10 (Primary), 18C50, 55U35 (Secondary) |
| url | https://arxiv.org/abs/1211.2851 |