The main result of this paper may be stated as a construction of "almost representations" $\mu_n$ and $\tilde{\mu}_n$ for the presheaves $\Ob_n$ and $\tilde{Ob}_n$ on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these "almost representations" with respect to the universe category functors. In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.
Keywords: Type theory, Contextual category, Universe category
2010 MSC: 03F50, 18C50, 18D15
Theory and Applications of Categories, Vol. 32, 2017, No. 3, pp 53-112.
Published 2017-01-20.
TAC Home