Here's a fact related to the current discussion, which I have formalized 
today.  I would appreciate knowing
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.

You may find it in WellOrderedSets.v 
<https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on 
one of my branches.