Homotopical inverse diagrams in categories with attributes
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2018
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917249496907776 |
|---|---|
| author | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| author_facet | Kapulkin, Chris Lumsdaine, Peter LeFanu |
| contents | We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes.
Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($Π$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory.
In a companion paper "The homotopy theory of type theories" (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1808_01816 |
| institution | arXiv |
| publishDate | 2018 |
| record_format | arxiv |
| spellingShingle | Homotopical inverse diagrams in categories with attributes Kapulkin, Chris Lumsdaine, Peter LeFanu Logic Category Theory 03B15 Higher-order logic and type theory (primary), 03G30 Categorical logic, topoi, 18C50 Categorical semantics of formal languages We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($Π$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory. In a companion paper "The homotopy theory of type theories" (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories. |
| title | Homotopical inverse diagrams in categories with attributes |
| topic | Logic Category Theory 03B15 Higher-order logic and type theory (primary), 03G30 Categorical logic, topoi, 18C50 Categorical semantics of formal languages |
| url | https://arxiv.org/abs/1808.01816 |