arXiv Analytics

Sign in

arXiv:1705.07442 [math.CT]AbstractReferencesReviewsResources

A type theory for synthetic $\infty$-categories

Emily Riehl, Michael Shulman

Published 2017-05-21Version 1

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. First we develop a simplicial type theory within a new three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. The simplices are then used to probe the internal categorical structures of types, allowing us to 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. The single contractibility condition characterizing Segal types in fact ensures coherent categorical structure at all dimensions. In particular, from it we can prove that composition is associative and unital and develop a theory of functors and natural transformations. We then define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct notions of adjunction between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.

Related articles: Most relevant | Search more
arXiv:1804.05045 [math.CT] (Published 2018-04-13)
Morita equivalences between algebraic dependent type theories
arXiv:math/0608436 [math.CT] (Published 2006-08-17)
Strict $\infty $-categories. Concrete Duality
arXiv:2107.12356 [math.CT] (Published 2021-07-26)
Cartesian Fibrations of $(\infty,2)$-categories