#
Products of families of types and $(\Pi,\lambda)$-structures on C-systems

##
Vladimir Voevodsky

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.

Keywords:
Type theory, contextual category, dependent product

2010 MSC:
03F50, 18C50, 03B15, 18D15

*Theory and Applications of Categories,*
Vol. 31, 2016,
No. 36, pp 1044-1094.

Published 2016-11-22.

http://www.tac.mta.ca/tac/volumes/31/36/31-36.pdf

TAC Home