Dan, this is one instance of my "general universal property of the 
propositional truncation", arXiv:1411.2682.
In that paper I show that, if you fix a number n, then for a type Y of 
h-level n, the function type
   ||X|| -> Y
is equivalent to the Sigma-type with the following components:
(1) a function X -> Y
(2) the condition that (1) is weakly constant
(3) a coherence condition for (2)
(4) a coherence condition for (3)
...
(n) a coherence condition for (n-1)

This can be presented as a natural transformation between 
semi-simplicial types.
What you have formalized is the case n=3 (one direction).
(In my presentation, I don't use the component "c x x = idpath (f x)" 
because it can be inferred,
and if you go higher than 3, this component would make additional 
coherence conditions necessary.)
Nicolai

On 03/04/17 01:35, Daniel R. Grayson wrote:
> 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.
>
>
> -- 
> You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeThe...@googlegroups.com 
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.