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

TL;DR

This paper explores the structures on C-systems related to type theory inference rules, introducing (Pi,lambda)-structures and establishing a bijection with Cartmell-Streicher structures, using constructive methods.

Contribution

It introduces (Pi,lambda)-structures on C-systems and proves a bijection with Cartmell-Streicher structures, advancing the understanding of type-theoretic structures on C-systems.

Findings

Defined (Pi,lambda)-structures on C-systems.

Established a bijection with Cartmell-Streicher structures.

Provided constructive proofs without classical logic assumptions.

Abstract

In this paper we continue 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.