module Homotopy.Connectedness where

Connectedness🔗

We say that a type is nn-connected if its nn-truncation is contractible.

While being nn-truncated expresses that all homotopy groups above nn are trivial, being nn-connected means that all homotopy groups below nn are trivial. A type that is both nn-truncated and nn-connected is contractible.

We give definitions in terms of the propositional truncation and set truncation for the lower levels, and then defer to the general “hubs and spokes” truncation. Note that our indices are offset by 2, just like h-levels.

is-n-connected :  {}  Type   Nat  Type _
is-n-connected A zero = Lift _ 
is-n-connected A (suc zero) =  A 
is-n-connected A (suc (suc zero)) = is-contr  A ∥₀
is-n-connected A n@(suc (suc (suc _))) = is-contr (n-Tr A n)

Being nn-connected is a proposition:

is-n-connected-is-prop :  {} {A : Type } (n : Nat)  is-prop (is-n-connected A n)
is-n-connected-is-prop zero _ _ = refl
is-n-connected-is-prop (suc zero) = is-prop-∥-∥
is-n-connected-is-prop (suc (suc zero)) = is-contr-is-prop
is-n-connected-is-prop (suc (suc (suc n))) = is-contr-is-prop

For short, we say that a type is connected if it is 00-connected, and simply connected if it is 11-connected:

is-connected :  {}  Type   Type _
is-connected A = is-n-connected A 2

is-simply-connected :  {}  Type   Type _
is-simply-connected A = is-n-connected A 3

Pointed connected types🔗

In the case of pointed types, there is an equivalent definition of being connected that is sometimes easier to work with: a pointed type is connected if every point is merely equal to the base point.

is-connected∙ :  {}  Type∙   Type _
is-connected∙ (X , pt) = (x : X)   x  pt 

module _ {} {X@(_ , pt) : Type∙ } where
  is-connected∙→is-connected : is-connected∙ X  is-connected  X 
  is-connected∙→is-connected c .centre = inc pt
  is-connected∙→is-connected c .paths =
    ∥-∥₀-elim hlevel! λ x  ∥-∥-rec! (ap inc  sym) (c x)

  is-connected→is-connected∙ : is-connected  X   is-connected∙ X
  is-connected→is-connected∙ c x =
    ∥-∥₀-path.to (is-contr→is-prop c (inc x) (inc pt))

This alternative definition lets us formulate a nice elimination principle for pointed connected types: any family of propositions PP that holds on the base point holds everywhere. In particular, since being a proposition is a proposition, we only need to check that P()P(\bullet_{}) is a proposition.

connected∙-elim-prop
  :  { ℓ′} {X : Type∙ } {P :  X   Type ℓ′}
   is-connected∙ X
   is-prop (P (X .snd))
   P (X .snd)
    x  P x
connected∙-elim-prop {X = X} {P} conn prop pb x =
  ∥-∥-rec (P-is-prop x)  e  subst P (sym e) pb) (conn x)
  where abstract
    P-is-prop :  x  is-prop (P x)
    P-is-prop x = ∥-∥-rec is-prop-is-prop  e  subst (is-prop  P) (sym e) prop) (conn x)

Examples of pointed connected types include the circle and the delooping of a group.

S¹-is-connected : is-connected∙ ( , base)
S¹-is-connected = S¹-elim (inc refl) prop!

Deloop-is-connected :  {} {G : Group }  is-connected∙ (Deloop G , base)
Deloop-is-connected = Deloop-elim-prop _ _ hlevel! (inc refl)