Geodesic
The Interpretation Lifting Theorem for C-Systems
Theory and applications of categories, Tome 38 (2022), pp. 214-231 Cet article a éte moissonné depuis la source Theory and Applications of Categories website

Voir la notice de l'article

In this article we present a solution to a conjecture of Vladimir Voevodsky regarding C-systems. This conjecture provides, under some assumptions, a lift of a functor M: CC -> C, where CC is a C-system and C a category, to a morphism of C-systems M': CC -> CC(\hat{C}, p_M). We explain the motivation behind this conjecture and introduce the required background material on C-systems. Finally, we give a proof of this conjecture. As we shall see the corresponding theorem allows to lift weak interpretations of type theory to strong ones.

Publié le :
Classification : 18C10, 18C50
Keywords: C-system, universe category, contextual category 
@article{TAC_2022_38_a6,
     author = {Anthony Bordg},
     title = {The  {Interpretation} {Lifting} {Theorem} for {C-Systems}},
     journal = {Theory and applications of categories},
     pages = {214--231},
     year = {2022},
     volume = {38},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2022_38_a6/}
}
TY  - JOUR
AU  - Anthony Bordg
TI  - The  Interpretation Lifting Theorem for C-Systems
JO  - Theory and applications of categories
PY  - 2022
SP  - 214
EP  - 231
VL  - 38
UR  - http://geodesic.mathdoc.fr/item/TAC_2022_38_a6/
LA  - en
ID  - TAC_2022_38_a6
ER  - 
%0 Journal Article
%A Anthony Bordg
%T The  Interpretation Lifting Theorem for C-Systems
%J Theory and applications of categories
%D 2022
%P 214-231
%V 38
%U http://geodesic.mathdoc.fr/item/TAC_2022_38_a6/
%G en
%F TAC_2022_38_a6
Anthony Bordg. The  Interpretation Lifting Theorem for C-Systems. Theory and applications of categories, Tome 38 (2022), pp. 214-231. http://geodesic.mathdoc.fr/item/TAC_2022_38_a6/