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\colon \mathrm{ CC} \rightarrow \mathcal{ C}$, where $\mathrm{ CC}$ is a C-system and $\mathcal{ C}$ a category, to a morphism of C-systems $M'\colon \mathrm{ CC} \rightarrow \mathrm{ CC}(\widehat{ \mathcal{ 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.
Categories: math.CT math.LO