arXiv · 1706.03618
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.
Explore related subjects
Keep this discovery
Vladimir Voevodsky. 2017-06-12. The (Pi,lambda)-structures on the C-systems defined by universe categories. https://arxiv.org/abs/1706.03618
Cite the original work for its findings. Save a collection to share your selection of sources.