Homotopy type theory in Lean

DOI10.1007/978-3-319-66107-0_30MaRDI QIDQ1687770zbMATH OpenOpenAlexFDO

Authors Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz

Publication date 4 January 2018

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

zbMATH Keywords

proof assistantshomotopy type theoryformalized mathematicsLean

Mathematics Subject Classification ID

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

Abstract: We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.

Recommendations

• A cubical approach to synthetic homotopy theory
• Homotopy limits in type theory
• Homotopy type theory and Voevodsky's univalent foundations
• Inductive types in homotopy type theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory

Cites work

• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• A coherence theorem for Martin-Löf's type theory
• A cubical approach to synthetic homotopy theory
• Computational higher-dimensional type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Developing the algebraic hierarchy with type classes in Coq
• Eliminating Dependent Pattern Matching
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• Inductive families
• The Cayley-Dickson construction in homotopy type theory
• The Lean theorem prover (system description)
• The simplicial model of univalent foundations (after Voevodsky)
• Univalent categories and the Rezk completion

Cited in

(14)

• scientific article; zbMATH DE number 7215286 (Why is no real title available?)
• Constructing higher inductive types as groupoid quotients
• Path spaces of higher inductive types in homotopy type theory
• Higher Structures in Homotopy Type Theory
• Homotopy limits in type theory
• Formalizing double groupoids and cross modules in the Lean theorem prover
• Coherence via well-foundedness. Taming set-quotients in homotopy type theory
• scientific article; zbMATH DE number 7649964 (Why is no real title available?)
• Nilpotent types and fracture squares in homotopy type theory
• The integers as a higher inductive type
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Formalizing abstract computability: Turing categories in Coq
• Coherence for monoidal groupoids in HoTT
• A cubical approach to synthetic homotopy theory

Describes a project that uses

Uses Software

• Agda
• UniMath
• HoTT
• Lean
• cubicaltt

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687770)