Categorical structures for type theory in univalent foundations
From MaRDI portal
Publication:4683858
DOI10.23638/LMCS-14(3:18)2018zbMath1496.03053arXiv1705.04310MaRDI QIDQ4683858
Peter LeFanu Lumsdaine, Benedikt Ahrens, Vladimir Voevodsky
Publication date: 26 September 2018
Full work available at URL: https://arxiv.org/abs/1705.04310
Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Metamathematics of constructive systems (03F50) Topological categories, foundations of homotopy theory (55U40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)
Related Items (6)
Categorical structures for type theory in univalent foundations ⋮ Bicategories in univalent foundations ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Displayed Categories ⋮ Unnamed Item ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed
Uses Software
Cites Work
- Unnamed Item
- Generalized algebraic theories and contextual categories
- Topological and Simplicial Models of Identity Types
- Subsystems and regular quotients of C-systems
- A C-system defined by a universe category
- Monads Need Not Be Endofunctors
- Internal type theory
- Categorical structures for type theory in univalent foundations
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- An experimental library of formalized Mathematics based on the univalent foundations
This page was built for publication: Categorical structures for type theory in univalent foundations
