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

zbMath1383.03056arXiv1706.03618MaRDI QIDQ2963471

Vladimir Voevodsky

Publication date: 14 February 2017

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

zbMATH Keywords

type theorycontextual categorydependent productproduct of families of typesuniverse category

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 (9)

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 ⋮ The étale cohomology of the general linear group over a finite field and the Dickson algebra ⋮ An introduction to univalent foundations for mathematicians ⋮ Construction of the circle in \textit{UniMath} ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ C-systems defined by universe categories: presheaves

Uses Software

• UniMath
• GitHub

Cites Work

• Unnamed Item
• Generalized algebraic theories and contextual categories
• Products of families of types and (Pi,lambda)-structures on C-systems
• C-systems defined by universe categories: presheaves
• Subsystems and regular quotients of C-systems
• Locally cartesian closed categories and type theory
• A C-system defined by a universe category
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories

This page was built for publication: The (Pi,lambda)-structures on the C-systems defined by universe categories