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