Geodesic
A 2-categorical analysis of context comprehension
Theory and applications of categories, Tome 41 (2024), pp. 1476-1512.

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.
Publié le :
Classification : 8D70, 03B38, 18N45, 18N15, 18C1
Keywords: dependent type theory, category with families, comprehension category, structure-semantics adjunction, 2-category theory, coalgebra 
@article{TAC_2024_41_a41,
     author = {Greta Coraglia and Jacopo Emmenegger},
     title = {A 2-categorical analysis of context comprehension},
     journal = {Theory and applications of categories},
     pages = {1476--1512},
     publisher = {mathdoc},
     volume = {41},
     year = {2024},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2024_41_a41/}
}
TY  - JOUR
AU  - Greta Coraglia
AU  - Jacopo Emmenegger
TI  - A 2-categorical analysis of context comprehension
JO  - Theory and applications of categories
PY  - 2024
SP  - 1476
EP  - 1512
VL  - 41
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2024_41_a41/
LA  - en
ID  - TAC_2024_41_a41
ER  - 
%0 Journal Article
%A Greta Coraglia
%A Jacopo Emmenegger
%T A 2-categorical analysis of context comprehension
%J Theory and applications of categories
%D 2024
%P 1476-1512
%V 41
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2024_41_a41/
%G en
%F TAC_2024_41_a41
Greta Coraglia; Jacopo Emmenegger. A 2-categorical analysis of context comprehension. Theory and applications of categories, Tome 41 (2024), pp. 1476-1512. http://geodesic.mathdoc.fr/item/TAC_2024_41_a41/