#
A C-system defined by a universe category

##
Vladimir Voevodsky

This is the third paper in a series.
In it we construct a C-system CC(C,p) starting from a
category C together with a morphism $p:\tilde{U} \to U$, a
choice of pull-back squares based on $p$ for all morphisms to $U$
and a choice of a final object of C. Such a quadruple is
called a universe category. We then define universe category
functors and construct homomorphisms of C-systems CC(C,p)
defined by universe category functors.
In the sections before the last section we give, for any C-system CC,
three different constructions of pairs ((C,p),H) where (C,p) is a
universe category and $H : CC \to CC(C,p)$ is an isomorphism.
In the last section we construct for any (set) category C with a
choice of a final object and fiber products a C-system and an
equivalence between C and the precategory underlying CC.

Keywords:
contextual category, universe category, C-system

2010 MSC:
03F50, 03B15, 03G25

*Theory and Applications of Categories,*
Vol. 30, 2015,
No. 37, pp 1181-1214.

Published 2015-09-17.

http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf

TAC Home