A synthetic theory of ∞-categories in homotopy type theory
Emily Riehl – 31 May 2017
If homotopy type theory describes a "synthetic theory of oo-groupoids" is there a similar directed type theory that describes a "synthetic theory of oo-categories"? In joint work with Mike Shulman, we propose foundations for such a theory motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the oo-cosmos of Rezk spaces, a framework for synthetic oo-category theory developed in joint work with Verity. We introduce simplices and cofibrations into homotopy type theory to probe the internal categorical structure of types, and define Segal types, in which binary composites exist uniquely up to homotopy, and Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. In the model these correspond exactly to the Segal and Rezk spaces. We then demonstrate that these simple definitions suffice to develop the synthetic theory of oo-categories, including functors, natural transformations, co- and contravariant type families with discrete fibers (oo-groupoids), a "dependent" Yoneda lemma that looks like "directed identity-elimination," and the theory of coherent adjunctions.
Back