From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 31 Oct 2016 08:00:54 -0700 (PDT)
From: Ulrik Buchholtz <ulrikbu...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <bbdb58df-4192-4e2d-88bf-402bc52d710a@googlegroups.com>
In-Reply-To: <a5f9acf7-e01e-48be-92b1-720d1bb316a9@googlegroups.com>
References: <a5f9acf7-e01e-48be-92b1-720d1bb316a9@googlegroups.com>
Subject: Re: Connected 1-Types
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1926_1001699536.1477926054802"

------=_Part_1926_1001699536.1477926054802
Content-Type: multipart/alternative; 
	boundary="----=_Part_1927_1161827967.1477926054802"

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

On Monday, October 31, 2016 at 3:42:05 PM UTC+1, =D0=92=D0=B0=D0=BB=D0=B5=
=D1=80=D0=B8=D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote:
>
> Let's consider the type of pointed connected 1-types, that is PC1T =3D =
=CE=A3 (A=20
> : 1-Type) (a=E2=82=80 : A) (isConnected A), where isConnected A =3D (a a'=
 : A) =E2=86=92 =E2=88=A5 a=20
> =E2=89=A1 a' =E2=88=A5.
> This type is equivalent to the type of groups (this construction uses=20
> HITs). This implies that it is a 1-type.
> Is there a way to prove directly (without HITs) that PC1T is a 1-type?
>

Sure, it suffices to show that any identity type (BG =3D BH) is a 0-type.=
=20
This type is a sub-type of the hom-type hom(B,H) =3D (BG =E2=86=92* BH), wh=
ich is=20
easily seen to be a set: see Section 4 of this handout:=20
http://www.mathematik.tu-darmstadt.de/~buchholtz/higher-groups.pdf
=20

> Also, is it true for the type of connected 1-types (C1T =3D C1T =3D =CE=
=A3 (A :=20
> 1-Type) (isConnected A)) or merely inhabited connected 1-types (IC1T =3D =
=CE=A3 (A=20
> : 1-Type ) (=E2=88=A5 A =E2=88=A5 =C3=97 isConnected A))?
>

No, connected 1-types, i.e., connected groupoids, are no simpler than=20
general groupoids.

Are there analogous theorems for n-types with n > 1?
>

See the handout :)

Cheers,
Ulrik


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

<div dir=3D"ltr">On Monday, October 31, 2016 at 3:42:05 PM UTC+1, =D0=92=D0=
=B0=D0=BB=D0=B5=D1=80=D0=B8=D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote:<blo=
ckquote class=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;border-=
left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr">Let&#39;s conside=
r the type of=C2=A0pointed=C2=A0connected 1-types, that is PC1T =3D =CE=A3 =
(A : 1-Type) (a=E2=82=80 : A) (isConnected A), where isConnected A =3D (a a=
&#39; : A) =E2=86=92 =E2=88=A5 a =E2=89=A1 a&#39; =E2=88=A5.<div>This type =
is equivalent to the type of groups (this construction uses HITs). This imp=
lies that it is a 1-type.</div><div>Is there a way to prove directly=C2=A0(=
without HITs)=C2=A0that PC1T is a 1-type?</div></div></blockquote><div><br>=
Sure, it suffices to show that any identity type (BG =3D BH) is a 0-type. T=
his type is a sub-type of the hom-type hom(B,H) =3D (BG =E2=86=92* BH), whi=
ch is easily seen to be a set: see Section 4 of this handout: http://www.ma=
thematik.tu-darmstadt.de/~buchholtz/higher-groups.pdf<br>=C2=A0</div><block=
quote class=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;border-le=
ft: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"><div>Also, is it tr=
ue for the type of connected 1-types (C1T =3D C1T =3D =CE=A3 (A : 1-Type) (=
isConnected A)) or merely inhabited connected 1-types (IC1T =3D =CE=A3 (A :=
 1-Type ) (=E2=88=A5 A =E2=88=A5 =C3=97 isConnected A))?</div></div></block=
quote><div><br>No, connected 1-types, i.e., connected groupoids, are no sim=
pler than general groupoids.<br><br></div><blockquote class=3D"gmail_quote"=
 style=3D"margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-=
left: 1ex;"><div dir=3D"ltr"><div>Are there analogous theorems for n-types =
with n &gt; 1?</div></div></blockquote><div><br>See the handout :)<br><br>C=
heers,<br>Ulrik<br><br></div></div>
------=_Part_1927_1161827967.1477926054802--

------=_Part_1926_1001699536.1477926054802--