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.
TAC Home