Martin-Löf identity types in C-systems

DOI10.1007/s10240-023-00138-2arXiv1505.06446OpenAlexW4385418011MaRDI QIDQ6139425

Vladimir Voevodsky

Publication date: 18 December 2023

Published in: Publications Mathématiques (Search for Journal in Brave)

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

Mathematics Subject Classification ID

General logic (03Bxx) Proof theory and constructive mathematics (03Fxx) Algebraic logic (03Gxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The identity type weak factorisation system
• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Topological and Simplicial Models of Identity Types
• Products of families of types and (Pi,lambda)-structures on C-systems
• C-systems defined by universe categories: presheaves
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Subsystems and regular quotients of C-systems
• Types are weak ω -groupoids
• A C-system defined by a universe category
• Simplicial radditive functors
• Homotopy theoretic models of identity types
• Internal type theory

This page was built for publication: Martin-Löf identity types in C-systems