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

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.

This is the third of the three papers into which the preprint "Products of families of types on the C-systems defined by a universe category" evolved during publication. The paper is published in Theory and Applications of Categories