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