#
The Interpretation Lifting Theorem for C-Systems

##
Anthony Bordg

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.

Keywords:
C-system, universe category, contextual category

2020 MSC:
18C10, 18C50

*Theory and Applications of Categories,*
Vol. 38, 2022,
No. 7, pp 214-231.

Published 2022-01-20.

http://www.tac.mta.ca/tac/volumes/38/7/38-07.pdf

TAC Home