Re: Connected 1-Types

[Ulrik Buchholtz <ulrikbu...@gmail.com>]

[-- 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 --]