Publication Type:
Journal ArticleSource:
Theory and Applications of Categories, Volume 32, Issue 4, p.113-121 (2017)URL:
http://www.tac.mta.ca/tac/volumes/32/4/32-04abs.htmlAbstract:
<p>We define the notion of a (P,˜P)-structure on a universe p in a locally cartesian closed category category with a binary product structure and construct a (Π,λ)-structure on the C-systems CC(C,p) from a (P,˜P)-structure on p. We then define homomorphisms of C-systems with (Π,λ)-structures and functors of universe categories with (P,˜P)-structures and show that our construction is functorial relative to these definitions.The proofs in this paper rely on the general constructions of the previous paper "C-systems defined by universe categories: presheaves". Keywords: Type theory, Contextual category, Universe category, dependent product, product of families of types</p>
Comments:
Test
Weight:
6