Thanks, Nicolai and Favonia.  It's a nice result, Nicolai!

On Monday, April 3, 2017 at 5:56:36 AM UTC-4, Nicolai Kraus wrote:
>
> 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.
>
>