whether it's already known. It gives a criterion for factoring through the propositional truncation
when the target is of h-level 3.
Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
(f : X -> Y) (c : ∏ x x', f x = f x') :
(∏ x, c x x = idpath (f x)) ->
(∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
∥ X ∥ -> Y.