Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Tom de Jong, Nicolai Kraus, Axel Ljungström

TL;DR

This work addresses coherence management in simplicial type theory by deriving all higher coherences from unique inner-horn fillers for Segal types. It introduces and exploits the Leibniz adjunction within the wild category of types, establishing an internal 1-categorical-like adjunction between pushout-products and pullback-homs and linking wild maps to wild families via univalence. The main technical contribution generalizes prior results to all inner horns and provides a formal Cubical Agda formalization, offering a robust framework for reasoning about Segal types and STT. The findings advance synthetic higher category theory in type theory and deliver a solid formal verification basis for STT constructions and coherence results with practical implications for formalized higher-categorical reasoning.

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.

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

TL;DR

This work addresses coherence management in simplicial type theory by deriving all higher coherences from unique inner-horn fillers for Segal types. It introduces and exploits the Leibniz adjunction within the wild category of types, establishing an internal 1-categorical-like adjunction between pushout-products and pullback-homs and linking wild maps to wild families via univalence. The main technical contribution generalizes prior results to all inner horns and provides a formal Cubical Agda formalization, offering a robust framework for reasoning about Segal types and STT. The findings advance synthetic higher category theory in type theory and deliver a solid formal verification basis for STT constructions and coherence results with practical implications for formalized higher-categorical reasoning.

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 -horns, it has unique fillers for all inner -horns. This generalizes a result of Riehl and Shulman for the case . 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.
Paper Structure (17 sections, 17 theorems, 40 equations)

This paper contains 17 sections, 17 theorems, 40 equations.

Table of Contents

  1. Introduction
  2. Foundational setup
  3. Related work
  4. Formalization
  5. Preliminaries
  6. The Leibniz Adjunction for Types
  7. Wild categories and functors
  8. The wild category of maps
  9. The wild category of families
  10. The wild categories of maps and families are equivalent
  11. The pushout-product and pullback-hom on Fam
  12. The pushout-product and pullback-hom as adjoints
  13. Application: Orthogonality and Simplicial Type Theory
  14. Orthogonality
  15. Simplicial Type Theory
  16. ...and 2 more sections

Key Result

Proposition 3.3

The equivalence $\chi$ extends to an isomorphism of the wild categories ${\mathop{\mathrm{\textup{Map}}}\nolimits}$ and ${\mathop{\mathrm{\textup{Fam}}}\nolimits}$.

Theorems & Definitions (42)

  • Definition 3.1: \baseurl#Definition-3-1 Isomorphism of wild categories
  • Remark 3.2: \baseurl#Remark-3-2
  • Proposition 3.3: \baseurl#Proposition-3-3
  • proof
  • Proposition 3.4: \baseurl#Proposition-3-4
  • Definition 3.5: \baseurl#Definition-3-5 Pushout-product of families, $(A,B) \mathbin{\widehat{\times}} (X,Y)$
  • Proposition 3.6: \baseurl#Proposition-3-6
  • proof
  • Proposition 3.7: \baseurl#Proposition-3-7
  • Definition 3.8: \baseurl#Definition-3-8 Constant maps, $\mathop{\mathrm{const}}\nolimits f$
  • ...and 32 more