Homotopical inverse diagrams in categories with attributes
Chris Kapulkin, Peter LeFanu Lumsdaine

TL;DR
This paper develops a framework for homotopical inverse diagrams within categories with attributes, enabling the construction of diagram models of type theory with lifted logical structures.
Contribution
It introduces a method to build categories of homotopical diagrams and lift logical structures, broadening the modeling of type theories.
Findings
Constructed categories of homotopical diagrams of shape I in C
Lifted logical structures such as Pi-types and identity types
Provided groundwork for diagram models of type theory
Abstract
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes and an ordered homotopical inverse category , we construct the category with attributes of homotopical diagrams of shape in and Reedy types over these; and we show how various logical structure (-types, identity types, and so on) lifts from to . 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Logic, programming, and type systems · Topological and Geometric Data Analysis
