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

2017/06/12 by Vladimir Voevodsky, Voevodsky, Vladimir
Computer Science · Decision Sciences · Mathematics · #03F50 18C50 03B15 #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Mathematics #Fuzzy and Soft Set Theory #Rings, Modules, and Algebras

paper · pdf · doi:10.48550/arxiv.1706.03618

openalex publication_date 2017/06/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Generalised algebraic theories and contextual categories

Related

• Products of families of types in the C-systems defined by a universe category
• Products of families of types and (Pi,lambda)-structures on C-systems
• A C-system defined by a universe category
• C-systems defined by universe categories: presheaves
• The Interpretation Lifting Theorem for C-Systems