The Interpretation Lifting Theorem for C-Systems

2017/10/05 by Anthony Bordg, Bordg, Anthony
Mathematics · #Advanced Topology and Set Theory #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO)

paper · pdf · doi:10.48550/arxiv.1710.02028

openalex publication_date 2017/10/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 CC → C, where CC is a C-system and C a category, to a morphism of C-systems M'\colon CC → CC(\widehatC,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.

Related

• Subsystems and regular quotients of C-systems
• Products of families of types in the C-systems defined by a universe category
• A C-system defined by a universe category
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• C-system of a module over a Jf-relative monad