Yes, this has been known from Nicolai's work on truncation (e.g. "The
General Universal Property"). I just learned that this has been mechanized
in Agda by Nils as well.
http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html#18216
By
the way, the condition (∏ x, c x x = idpath (f x)) is provable from
transitivity. -Favonia

On Sun, Apr 2, 2017 at 8:35 PM Daniel R. Grayson <
danielrich...@gmail.com> 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.
For more options, visit https://groups.google.com/d/optout.