A C-system defined by a universe category
Vladimir Voevodsky · Theory and applications of categories · 2015
This is the third paper in a series started in [9].In it we construct a C-system CC(C, p) starting from a category C together with a morphism p : U → 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 → 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.