  In homotopy type theory, we construct the propositional truncation as a
colimit, using only non-recursive higher inductive types (HITs). This is a
first step towards reducing recursive HITs to non-recursive HITs. This
construction gives a characterization of functions from the propositional
truncation to an arbitrary type, extending the universal property of the
propositional truncation. We have fully formalized all the results in a new
proof assistant, Lean.
