Geodesic
The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories
Theory and applications of categories, Tome 32 (2017), pp. 113-121

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

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.

Publié le :
Classification : 03F50, 18C50, 03B15, 18D15
Keywords: Type theory, Contextual category, Universe category, dependent product, product of families of types 
@article{TAC_2017_32_a3,
     author = {Vladimir Voevodsky},
     title = {The $(\Pi,\lambda)$-structures on the {C-systems} defined by universe categories},
     journal = {Theory and applications of categories},
     pages = {113--121},
     publisher = {mathdoc},
     volume = {32},
     year = {2017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2017_32_a3/}
}
TY  - JOUR
AU  - Vladimir Voevodsky
TI  - The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories
JO  - Theory and applications of categories
PY  - 2017
SP  - 113
EP  - 121
VL  - 32
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2017_32_a3/
LA  - en
ID  - TAC_2017_32_a3
ER  - 
%0 Journal Article
%A Vladimir Voevodsky
%T The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories
%J Theory and applications of categories
%D 2017
%P 113-121
%V 32
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2017_32_a3/
%G en
%F TAC_2017_32_a3
Vladimir Voevodsky. The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories. Theory and applications of categories, Tome 32 (2017), pp. 113-121. http://geodesic.mathdoc.fr/item/TAC_2017_32_a3/