The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

TL;DR

This paper demonstrates that in homotopy type theory extended with an interval type, all higher coherences can be derived, using the Leibniz adjunction to relate pushout-products and pullback-homs in the category of types.

Contribution

It establishes the Leibniz adjunction in the higher category of types and applies it to derive higher coherences in simplicial type theory, formalized in Cubical Agda.

Findings

All higher coherences follow from unique fillers for (2,1)-horns.

The Leibniz adjunction holds in the higher category of types.

Formalization achieved in Cubical Agda.

Abstract

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.