Floris van Doorn: Constructing the propositional truncation using non-recursive HITs. CPP 2016: 122-129