A type theory for synthetic $\infty$-categories

TL;DR

This paper develops a synthetic framework for $( abla,1)$-categories within homotopy type theory, introducing new types and structures to model categorical concepts with homotopical correctness.

Contribution

It introduces Segal and Rezk types, along with covariant fibrations, providing a new foundation for higher category theory in homotopy type theory.

Findings

Defined Segal types with unique binary composition up to homotopy

Established Rezk types with equivalence of isomorphisms and identities

Proved a dependent Yoneda lemma for covariant fibrations

Abstract

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we 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 adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a 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. 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.