The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2601.21843
curl -X POST /api/v1/records/arxiv/2601.21843/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2601.21843/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'