Geodesic
Products of families of types and $(\Pi,\lambda)$-structures on C-systems
Theory and applications of categories, Tome 31 (2016), pp. 1044-1094.

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

In this paper we continue, following the pioneering works by J. Cartmell and T. Streicher, the study of the most important structures on C-systems, the structures that correspond, in the case of the syntactic C-systems, to the $(\Pi,\lambda,app,\beta,\eta)$-system of inference rules. One such structure was introduced by J. Cartmell and later studied by T. Streicher under the name of the products of families of types. We introduce the notion of a $(\Pi,\lambda)$-structure and construct a bijection, for a given C-system, between the set of $(\Pi,\lambda)$-structures and the set of Cartmell-Streicher structures. In the following paper we will show how to construct, and in some cases fully classify, the $(\Pi,\lambda)$-structures on the C-systems that correspond to universe categories. The first section of the paper provides careful proofs of many of the properties of general C-systems.Methods of the paper are fully constructive, that is, neither the axiom of excluded middle nor the axiom of choice are used.
Publié le :
Classification : 03F50, 18C50, 03B15, 18D15
Keywords: Type theory, contextual category, dependent product 
@article{TAC_2016_31_a35,
     author = {Vladimir Voevodsky},
     title = {Products of families of types and $(\Pi,\lambda)$-structures on {C-systems}},
     journal = {Theory and applications of categories},
     pages = {1044--1094},
     publisher = {mathdoc},
     volume = {31},
     year = {2016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2016_31_a35/}
}
TY  - JOUR
AU  - Vladimir Voevodsky
TI  - Products of families of types and $(\Pi,\lambda)$-structures on C-systems
JO  - Theory and applications of categories
PY  - 2016
SP  - 1044
EP  - 1094
VL  - 31
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2016_31_a35/
LA  - en
ID  - TAC_2016_31_a35
ER  - 
%0 Journal Article
%A Vladimir Voevodsky
%T Products of families of types and $(\Pi,\lambda)$-structures on C-systems
%J Theory and applications of categories
%D 2016
%P 1044-1094
%V 31
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2016_31_a35/
%G en
%F TAC_2016_31_a35
Vladimir Voevodsky. Products of families of types and $(\Pi,\lambda)$-structures on C-systems. Theory and applications of categories, Tome 31 (2016), pp. 1044-1094. http://geodesic.mathdoc.fr/item/TAC_2016_31_a35/