Monthly Archives: July 2015
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
Universal Properties of Truncations
Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation , and I want to write this blog post in case … Continue reading
Posted in Foundations, Homotopy Theory, Models, Paper, Talk
3 Comments
Modules for Modalities
As defined in chapter 7 of the book, a modality is an operation on types that behaves somewhat like the n-truncation. Specifically, it consists of a collection of types, called the modal ones, together with a way to turn any … Continue reading
Posted in Code, Programming
19 Comments
Homotopy Type Theory 