DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2026.38

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Authors: Daniël Otten and Matteo Spadetto

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.

Cite as

Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2026.38,
  author =	{Otten, Dani\"{e}l and Spadetto, Matteo},
  title =	{{The Biequivalence of Path Categories and Axiomatic Martin-L\"{o}f Type Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{38:1--38:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38},
  URN =		{urn:nbn:de:0030-drops-254633},
  doi =		{10.4230/LIPIcs.CSL.2026.38},
  annote =	{Keywords: Axiomatic type theory, cubical type theory, propositional equality, biequivalence, display map categories, path categories, homotopy theory, coherence}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2021.87

The Gödel Fibration

Authors: Davide Trotta, Matteo Spadetto, and Valeria de Paiva

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract

We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principles of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula. Building up from Hofstra’s earlier fibrational characterization of de Paiva’s categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. This result establishes an intrinsic presentation of the Dialectica fibration, contributing to the understanding of the Dialectica construction itself and of its properties from a logical perspective.

Cite as

Davide Trotta, Matteo Spadetto, and Valeria de Paiva. The Gödel Fibration. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 87:1-87:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{trotta_et_al:LIPIcs.MFCS.2021.87,
  author =	{Trotta, Davide and Spadetto, Matteo and de Paiva, Valeria},
  title =	{{The G\"{o}del Fibration}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{87:1--87:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.87},
  URN =		{urn:nbn:de:0030-drops-145272},
  doi =		{10.4230/LIPIcs.MFCS.2021.87},
  annote =	{Keywords: Dialectica category, G\"{o}del fibration, Pseudo-monad}
}

Search Results

Documents authored by Spadetto, Matteo

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Abstract

Cite as

The Gödel Fibration

Abstract

Cite as

Thanks for your feedback!

Could not send message