The Interpretation Lifting Theorem for C-Systems

Anthony Bordg

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