Connected 1-Types

Connected 1-Types

[Валерий Исаев]

[-- Attachment #1.1: Type: text/plain, Size: 719 bytes --]

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 = Σ (A : 
1-Type) (a₀ : A) (isConnected A), where isConnected A = (a a' : A) → ∥ a ≡ 
a' ∥.
This type is equivalent to the type of groups (this construction uses 
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 = C1T = Σ (A : 
1-Type) (isConnected A)) or merely inhabited connected 1-types (IC1T = Σ (A 
: 1-Type ) (∥ A ∥ × isConnected A))?
Are there analogous theorems for n-types with n > 1?

Regards,
Valery Isaev


[-- Attachment #1.2: Type: text/html, Size: 884 bytes --]

Re: Connected 1-Types

[Ulrik Buchholtz]

[-- Attachment #1.1: Type: text/plain, Size: 1143 bytes --]

On Monday, October 31, 2016 at 3:42:05 PM UTC+1, Валерий Исаев wrote:
>
> Let's consider the type of pointed connected 1-types, that is PC1T = Σ (A 
> : 1-Type) (a₀ : A) (isConnected A), where isConnected A = (a a' : A) → ∥ a 
> ≡ a' ∥.
> This type is equivalent to the type of groups (this construction uses 
> 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 = BH) is a 0-type. 
This type is a sub-type of the hom-type hom(B,H) = (BG →* BH), which is 
easily seen to be a set: see Section 4 of this handout: 
http://www.mathematik.tu-darmstadt.de/~buchholtz/higher-groups.pdf
 

> Also, is it true for the type of connected 1-types (C1T = C1T = Σ (A : 
> 1-Type) (isConnected A)) or merely inhabited connected 1-types (IC1T = Σ (A 
> : 1-Type ) (∥ A ∥ × isConnected A))?
>

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

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

See the handout :)

Cheers,
Ulrik


[-- Attachment #1.2: Type: text/html, Size: 1669 bytes --]

RE: [HoTT] Connected 1-Types

[Joyal, André]

[-- Attachment #1: Type: text/plain, Size: 1685 bytes --]

Dear Valery,

Just a remark:
The presence (or the absence) of a base point is affecting the group of self-equivalences of a type.
The group of self-equivalences of a pointed connected 1-type (X,pt)=BG
is the group of automorphisms of G. The group of self-equivalences of the unbased space
X=BG is the 2-group of automorphisms of the groupoid G.

Best,
André

________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Валерий Исаев [valery...@gmail.com]
Sent: Monday, October 31, 2016 10:42 AM
To: Homotopy Type Theory
Subject: [HoTT] Connected 1-Types

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 = Σ (A : 1-Type) (a₀ : A) (isConnected A), where isConnected A = (a a' : A) → ∥ a ≡ a' ∥.
This type is equivalent to the type of groups (this construction uses 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 = C1T = Σ (A : 1-Type) (isConnected A)) or merely inhabited connected 1-types (IC1T = Σ (A : 1-Type ) (∥ A ∥ × isConnected A))?
Are there analogous theorems for n-types with n > 1?

Regards,
Valery Isaev


--
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<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 2683 bytes --]