2026-07-22T21:02:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25463 2026-03-19T13:28:56Z ddc:004 open_access

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories Otten, Daniël Spadetto, Matteo Axiomatic type theory cubical type theory propositional equality biequivalence display map categories path categories homotopy theory coherence 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Daniël Otten and Matteo Spadetto 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.38 urn:nbn:de:0030-drops-254633 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38 eng https://creativecommons.org/licenses/by/4.0/legalcode