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.
TAC Home