#
C-systems defined by universe categories: presheaves

##
Vladimir Voevodsky

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.

http://www.tac.mta.ca/tac/volumes/32/3/32-03.pdf

TAC Home