The homotopy theory of type theories
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2016
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910012296658944 |
|---|---|
| author | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| author_facet | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| contents | We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,Σ(,Π_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories.
This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1610_00037 |
| institution | arXiv |
| publishDate | 2016 |
| record_format | arxiv |
| spellingShingle | The homotopy theory of type theories Kapulkin, Chris Lumsdaine, Peter LeFanu Category Theory 18G55 Homotopical algebra (primary) 03B15 Higher-order logic & type theory 18C50 Cat'l semantics of formal languages 55U35 Abstract & axiomatic homotopy theory We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,Σ(,Π_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures. |
| title | The homotopy theory of type theories |
| topic | Category Theory 18G55 Homotopical algebra (primary) 03B15 Higher-order logic & type theory 18C50 Cat'l semantics of formal languages 55U35 Abstract & axiomatic homotopy theory |
| url | https://arxiv.org/abs/1610.00037 |