2015/03/23 by Vladimir Voevodsky, Voevodsky, Vladimir · 1 citation
Mathematics · #03B15 #03F50 #18D15 #18D99 #Advanced Topics in Algebra #Category Theory (math.CT) #FOS: Mathematics #Geometric and Algebraic Topology #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #math.CT #math.LO #msc:03B15 #msc:03F50 #msc:18D15 #msc:18D99
paper · pdf · doi:10.48550/arxiv.1503.07072
openalex publication_date 2015/03/23 · arxiv created 2015/07/29 · arxiv updated 2015/07/31 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
We introduce the notion of a (Π,λ)-structure on a C-system and show that C-systems with (Π,λ)-structures are constructively equivalent to contextual categories with products of families of types. We then show how to construct (Π,λ)-structures on C-systems of the form CC(\cal C,p) defined by a universe p in a locally cartesian closed category \cal C from a simple pull-back square based on p. In the last section we prove a theorem that asserts that our construction is functorial. This version introduces some changes compared to the previous one to ensure rigorous compatibility with arXiv:1409.7925v3.