Defined propositional truncation (both the correct one and the incorrect one) as an instance of a universal HIT.