2025/03/19 by Otten, Daniël, Spadetto, Matteo
#03B38 #03B70 #03F50 #03G30 #18C10 #18D30 #18N45 #55U35 #55U40 #Algebraic Topology (math.AT) #Category Theory (math.CT) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2503.15431
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categories, while adding Pi-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 1- and Sigma-types are biequivalent to certain path categories, while adding axiomatic Pi-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 1-, Sigma-, and Pi-types.