We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B. Jacobs' comprehension categories, and generalise it to the non-discrete case. The classical equivalence can be summarised in the slogan: "terms as sections". By recognising "terms as coalgebras", we show how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families. The biequivalence restricts to the classical one proved by Hofmann in the discrete case. It also provides a framework where to compare different morphisms of these structures that have appeared in the literature, varying on the degree of preservation of the relevant structure. We consider in particular morphisms defined by Claraimbault-Dybjer, Jacobs, Larrea, and Uemura.
Keywords: dependent type theory, category with families, comprehension category, structure-semantics adjunction, 2-category theory, coalgebra
2020 MSC:18D70, 03B38, 18N45, 18N15, 18C1
Theory and Applications of Categories, Vol. 41, 2024, No. 42, pp 1476-1512.
Published 2024-10-10.
TAC Home