The (Pi,lambda)-structures on the C-systems defined by universe categories

TL;DR

This paper introduces a new framework for (Pi,lambda)-structures on C-systems derived from universe categories with (P,P-tilde)-structures, establishing their functorial relationships.

Contribution

It defines (P,P-tilde)-structures on universe p in a locally cartesian closed category and constructs corresponding (Pi,lambda)-structures on C-systems, proving functoriality.

Findings

Constructed (Pi,lambda)-structures from (P,P-tilde)-structures.

Established functoriality of the construction.

Provided a categorical framework for (Pi,lambda)-structures.

Abstract

We define the notion of a (P,P-tilde)-structure on a universe p in a locally cartesian closed category category C with a binary product structure and construct a (Pi,lambda)-structure on the C-systems CC(C,p) from a (P,P-tilde)-structure on p. We then define homomorphisms of C-systems with (Pi,lambda)-structures and functors of universe categories with (P,P-tilde)-structures and show that our construction is functorial relative to these definitions.