From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 31 Oct 2016 07:42:05 -0700 (PDT)
From: =?UTF-8?B?0JLQsNC70LXRgNC40Lkg0JjRgdCw0LXQsg==?=
 <valery...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <a5f9acf7-e01e-48be-92b1-720d1bb316a9@googlegroups.com>
Subject: Connected 1-Types
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1321_939309554.1477924925246"

------=_Part_1321_939309554.1477924925246
Content-Type: multipart/alternative; 
	boundary="----=_Part_1322_515750419.1477924925246"

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

Hello, everybody,

The following questions have bothered me for some time now.
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 =E2=89=A1=20
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?
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))?
Are there analogous theorems for n-types with n > 1?

Regards,
Valery Isaev


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

<div dir=3D"ltr">Hello, everybody,<br><div><br></div><div>The following que=
stions have bothered me for some time now.</div><div>Let&#39;s consider 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><div>This type=
 is equivalent to the type of groups (this construction uses HITs). This im=
plies 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>Also, is it true for t=
he type of connected 1-types (C1T =3D C1T =3D =CE=A3 (A : 1-Type) (isConnec=
ted 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>Are there analog=
ous theorems for n-types with n &gt; 1?</div><div><br></div><div><div><div>=
Regards,</div><div>Valery Isaev</div></div></div><div><br></div></div>
------=_Part_1322_515750419.1477924925246--

------=_Part_1321_939309554.1477924925246--