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?