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.

翻译：单纯类型理论扩展了同伦类型理论，并为类型配备了有向态射的概念。Segal类型被定义为其中这些有向态射可复合的类型。我们证明，若将单纯类型理论视为包含一个公设区间类型的同伦类型理论，则所有高阶相干性均可被陈述和推导。从技术角度而言，这意味着如果一个类型具有$(2,1)$-角的唯一填充子，则其具有所有内$(n,k)$-角的唯一填充子。这推广了Riehl和Shulman针对$n = 3, k \in \{1, 2\}$情形的结果。我们的主要技术工具是莱布尼茨伴随：在类型的野生范畴中，推出积是拉回同的左伴随。虽然该伴随在普通范畴论中广为人知，但对于高阶范畴则复杂得多，而能在类型的野生范畴（一个未声明高阶相干性的高阶范畴）中证明该伴随是非平凡的。我们充分利用了映射的野生范畴与族的野生范畴之间的等价性。我们已在Cubical Agda中对结果进行了形式化验证。