THE INTERPRETATION LIFTING THEOREM FOR C-SYSTEMS

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((C) over cap ,pm). 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.