@article {114,
	title = {The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories},
	journal = {Theory and Applications of Categories},
	volume = {32},
	year = {2017},
	month = {01/2017},
	pages = {113-121},
	abstract = {<p>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.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>
},
	url = {http://www.tac.mta.ca/tac/volumes/32/4/32-04abs.html},
	author = {Voevodsky, Vladimir}
}