2020/07/06 by Martin E. Bidlingmaier, Bidlingmaier, Martin E.
Computer Science · Mathematics · #03B38 #18C50 #Category Theory (math.CT) #F.3.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2007.02900
openalex publication_date 2020/07/06 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
Locally cartesian closed (lcc) categories are natural categorical models of\nextensional dependent type theory. This paper introduces the "gros" semantics\nin the category of lcc categories: Instead of constructing an interpretation in\na given individual lcc category, we show that also the category of all lcc\ncategories can be endowed with the structure of a model of dependent type\ntheory. The original interpretation in an individual lcc category can then be\nrecovered by slicing. As in the original interpretation, we face the issue of\ncoherence: Categorical structure is usually preserved by functors only up to\nisomorphism, whereas syntactic substitution commutes strictly with all type\ntheoretic structure. Our solution involves a suitable presentation of the\nhigher category of lcc categories as model category. To that end, we construct\na model category of lcc sketches, from which we obtain by the formalism of\nalgebraically (co)fibrant objects model categories of strict lcc categories and\nthen algebraically cofibrant strict lcc categories. The latter is our model of\ndependent type theory.\n