From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 3 Apr 2017 04:50:26 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Cc: danielrich...@gmail.com Message-Id: <2a6ce7aa-99c8-48a5-bd16-bbcff260b0b9@googlegroups.com> In-Reply-To: <20eea0d3-b602-9e0d-fb14-89c0cacbf24e@gmail.com> References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com> <20eea0d3-b602-9e0d-fb14-89c0cacbf24e@gmail.com> Subject: Re: [HoTT] Re: Conjecture MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1578_27393152.1491220226509" ------=_Part_1578_27393152.1491220226509 Content-Type: multipart/alternative; boundary="----=_Part_1579_893333320.1491220226510" ------=_Part_1579_893333320.1491220226510 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=20 > propositional truncation", arXiv:1411.2682. > In that paper I show that, if you fix a number n, then for a type Y of=20 > 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= =20 > types. > What you have formalized is the case n=3D3 (one direction).=20 > (In my presentation, I don't use the component "c x x =3D idpath (f x)"= =20 > because it can be inferred,=20 > and if you go higher than 3, this component would make additional=20 > 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= =20 > today. I would appreciate knowing=20 > whether it's already known. It gives a criterion for factoring through= =20 > 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 : =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 > on=20 > one of my branches. > > ------=_Part_1579_893333320.1491220226510 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks, Nicolai and Favonia. =C2=A0It's a nice result,= Nicolai!

On Monday, April 3, 2017 at 5:56:36 AM UTC-4, Nicolai Krau= s wrote:
=20 =20 =20
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
=C2=A0 ||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=3D3 (one direction).
(In my presentation, I don't use the component "c x x =3D idpa= th (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. =C2=A0I would appreciate knowing
whether it's already known. =C2=A0It gives a criterion for factoring through the propositional truncation
when the target is of h-level 3.

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

You may find it in=C2=A0WellOrderedSets.v=C2=A0on one of my branches.
------=_Part_1579_893333320.1491220226510-- ------=_Part_1578_27393152.1491220226509--