The (Pi,lambda)-structures on the C-systems defined by universe categories
Category Theory
2017-06-13 v1
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.
Cite
@article{arxiv.1706.03618,
title = {The (Pi,lambda)-structures on the C-systems defined by universe categories},
author = {Vladimir Voevodsky},
journal= {arXiv preprint arXiv:1706.03618},
year = {2017}
}
Comments
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