The Interpretation Lifting Theorem for C-Systems

zbMath1483.18003arXiv1710.02028MaRDI QIDQ5025082

Anthony Bordg

Publication date: 1 February 2022

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

zbMATH Keywords

type theoryunivalence axiomterm modelcontextual categoryuniverse categoryC-systeminterpretation lifting conjecture

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Categorical semantics of formal languages (18C50) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)

Uses Software

• UniMath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalized algebraic theories and contextual categories
• Univalence for inverse EI diagrams
• The simplicial model of univalent foundations (after Voevodsky)
• Revisiting the categorical interpretation of dependent type theory
• Products of families of types and (Pi,lambda)-structures on C-systems
• The Local Universes Model
• 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
• Natural models of homotopy type theory
• A C-system defined by a universe category
• Internal type theory
• Categorical structures for type theory in univalent foundations
• Lawvere theories and C-systems
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: The Interpretation Lifting Theorem for C-Systems