From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Sun, 2 Apr 2017 17:35:04 -0700 (PDT)
From: "Daniel R. Grayson" <danielrich...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com>
In-Reply-To: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com>
References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com>
Subject: Re: Conjecture
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1339_807701966.1491179704569"

------=_Part_1339_807701966.1491179704569
Content-Type: multipart/alternative; 
	boundary="----=_Part_1340_1458806433.1491179704570"

------=_Part_1340_1458806433.1491179704570
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Here's a fact related to the current discussion, which I have formalized=20
today.  I would appreciate knowing
whether it's already known.  It gives a criterion for factoring through the=
=20
propositional truncation
when the target is of h-level 3.

  Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
             (f : X -> Y) (c : =E2=88=8F x x', f x =3D f x') :
    (=E2=88=8F x, c x x =3D idpath (f x)) ->
    (=E2=88=8F x x' x'', c x x'' =3D c x x' @ c x' x'') ->
    =E2=88=A5 X =E2=88=A5 -> Y.

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



------=_Part_1340_1458806433.1491179704570
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Here&#39;s a fact related to the current discussion, which=
 I have formalized today. =C2=A0I would appreciate knowing<div>whether it&#=
39;s already known. =C2=A0It gives a criterion for factoring through the pr=
opositional truncation</div><div>when the target is of h-level 3.</div><div=
><br></div><div><div><font face=3D"courier new, monospace">=C2=A0 Definitio=
n squash_to_HLevel_3 {X : UU} {Y : HLevel 3}</font></div><div><font face=3D=
"courier new, monospace">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(f=
 : X -&gt; Y) (c : =E2=88=8F x x&#39;, f x =3D f x&#39;) :</font></div><div=
><font face=3D"courier new, monospace">=C2=A0 =C2=A0 (=E2=88=8F x, c x x =
=3D idpath (f x)) -&gt;</font></div><div><font face=3D"courier new, monospa=
ce">=C2=A0 =C2=A0 (=E2=88=8F x x&#39; x&#39;&#39;, c x x&#39;&#39; =3D c x =
x&#39; @ c x&#39; x&#39;&#39;) -&gt;</font></div><div><font face=3D"courier=
 new, monospace">=C2=A0 =C2=A0 =E2=88=A5 X =E2=88=A5 -&gt; Y.</font></div><=
/div><div><font face=3D"arial, sans-serif"><br></font></div><div><font face=
=3D"arial, sans-serif">You may find it in=C2=A0<a href=3D"https://github.co=
m/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrdered=
Sets.v">WellOrderedSets.v</a>=C2=A0on one of my branches.</font></div><div>=
<font face=3D"courier new, monospace"><br></font></div><div><br></div></div=
>
------=_Part_1340_1458806433.1491179704570--

------=_Part_1339_807701966.1491179704569--