Categorical structures for type theory in univalent foundations

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

zbMATH Keywords

type theoryunivalence axiomcategorical semantics

Mathematics Subject Classification ID

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

• Coq
• UniMath
• GitHub

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