#
The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories

##
Vladimir Voevodsky

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.

http://www.tac.mta.ca/tac/volumes/32/4/32-04.pdf

TAC Home