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.
From: Tom de Jong [view email]
[v1]
Thu, 29 Jan 2026 15:19:28 UTC (24 KB)
[v2]
Wed, 17 Jun 2026 09:08:35 UTC (25 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。