We define the notion of a $(P,\tilde{P})$-structure on a universe $p$ in a locally cartesian closed category category with a binary product structure and construct a $(\Pi,\lambda)$-structure on the C-systems $CC(C,p)$ from a $(P,\tilde{P})$-structure on $p$. We then define homomorphisms of C-systems with $(\Pi,\lambda)$-structures and functors of universe categories with $(P,\tilde{P})$-structures and show that our construction is functorial relative to these definitions.
Keywords: Type theory, Contextual category, Universe category, dependent product, product of families of types
2010 MSC: 03F50, 18C50, 03B15, 18D15
Theory and Applications of Categories, Vol. 32, 2017, No. 4, pp 113-121.
Published 2017-01-27.
TAC Home