Homotopy type theory in Lean

DOI10.1007/978-3-319-66107-0_30zbMath1484.68319arXiv1704.06781OpenAlexW2608494448MaRDI QIDQ1687770

Ulrik Buchholtz, Floris van Doorn, Jakob von Raumer

Publication date: 4 January 2018

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

zbMATH Keywords

homotopy type theoryproof assistantsformalized mathematicsLean

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Topological categories, foundations of homotopy theory (55U40) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (7)

Unnamed Item ⋮ Higher Structures in Homotopy Type Theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Formalizing abstract computability: Turing categories in Coq

Uses Software

• Agda
• UniMath
• HoTT
• Lean
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Inductive families
• The simplicial model of univalent foundations (after Voevodsky)
• The Lean Theorem Prover (System Description)
• Homotopy theoretic models of identity types
• A coherence theorem for Martin-Löf's type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A Cubical Approach to Synthetic Homotopy Theory
• Computational higher-dimensional type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalent categories and the Rezk completion
• Developing the Algebraic Hierarchy with Type Classes in Coq
• Eliminating Dependent Pattern Matching

This page was built for publication: Homotopy type theory in Lean