Author Archives: Floris van Doorn
The Lean Theorem Prover
Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code … Continue reading
Posted in Code, Higher Inductive Types, Programming
48 Comments
Constructing the Propositional Truncation using Nonrecursive HITs
In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another … Continue reading
Posted in Code, Higher Inductive Types
25 Comments
Homotopy Type Theory 