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

[Ulrik Buchholtz]

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

[Joyal, André]

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

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