Simplicial Type Theory and Synthetic Infinity-Categories

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Opening obstruction

Ordinary identity paths are invertible and therefore cannot serve as the directed arrows of a synthetic infinity-category.

Development contract

In the Riehl–Shulman shape/tope calculus, begin with a directed $2$-simplex whose edges are $f:x\to y$, $g:y\to z$, and $h:x\to z$. Extension types express its boundary, and the Segal condition makes the space of fillers with $h=g\circ f$ contractible; use this calculus to derive Rezk types, covariant families, and dependent Yoneda. For Segal types $A$ and $B$, prove the Rzk-checked equivalence between quasi-transposing and quasi-diagrammatic adjunctions, under the file’s assumptions funext and extext. This check is not a normalization theorem for the calculus.