Products of families of types and (Pi,lambda)-structures on C-systems

zbMath1380.03072arXiv1706.03605MaRDI QIDQ2953831

Vladimir Voevodsky

Publication date: 6 January 2017

Full work available at URL: https://arxiv.org/abs/1706.03605

zbMATH Keywords

type theorycontextual categorydependent product

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Metamathematics of constructive systems (03F50)

Related Items (10)

Vladimir Aleksandrovich Voevodsky ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Martin-Löf identity types in C-systems ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ An introduction to univalent foundations for mathematicians ⋮ The homotopy theory of type theories ⋮ Construction of the circle in \textit{UniMath} ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ C-systems defined by universe categories: presheaves ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories

This page was built for publication: Products of families of types and (Pi,lambda)-structures on C-systems