The Interpretation Lifting Theorem for C-Systems

TL;DR

This paper proves Voevodsky's conjecture on lifting functors from C-systems to morphisms of C-systems, providing a significant theoretical advancement in the understanding of C-systems and their functorial properties.

Contribution

The paper offers a proof of Voevodsky's conjecture, establishing conditions under which functors from C-systems can be lifted to morphisms of C-systems.

Findings

Proof of Voevodsky's conjecture on C-systems

Conditions for lifting functors to morphisms

Enhanced understanding of C-system structures

Abstract

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.