C-systems defined by universe categories: presheaves

zbMath1453.03067arXiv1706.03620MaRDI QIDQ2963470

Vladimir Voevodsky

Publication date: 14 February 2017

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

zbMATH Keywords

type theorycontextual 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) Type theory (03B38)

Related Items (8)

Vladimir Aleksandrovich Voevodsky ⋮ The mysterious story of square ice, piles of cubes, and bijections ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Martin-Löf identity types in C-systems ⋮ The first bijective proof of the refined ASM theorem ⋮ An introduction to univalent foundations for mathematicians ⋮ Construction of the circle in \textit{UniMath} ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories

Cites Work

• Generalized algebraic theories and contextual categories
• Products of families of types and (Pi,lambda)-structures on C-systems
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Subsystems and regular quotients of C-systems
• A C-system defined by a universe category
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item

This page was built for publication: C-systems defined by universe categories: presheaves