Title: A type theory for synthetic $\infty$-categories,
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.