module Homotopy.Connectedness where

Connectedness🔗

We say that a type is if its truncation is contractible.

While being truncated expresses that all homotopy groups above are trivial, being means that all homotopy groups below are trivial. A type that is both and 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 is a proposition:

is-n-connected-is-prop : (n : Nat) → is-prop (is-n-connected A n)
is-n-connected-is-prop 0 _ _ = refl
is-n-connected-is-prop 1     = is-prop-∥-∥
is-n-connected-is-prop 2     = 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 and simply connected if it is

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

Furthermore, we say that a map is if all of its fibres are

is-n-connected-map : (A → B) → Nat → Type _
is-n-connected-map f n = ∀ x → is-n-connected (fibre f x) n

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 (λ _ → is-hlevel-suc 2 squash (inc pt) _) λ x →
      ∥-∥-rec! {pprop = squash _ _} (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 that holds on the base point holds everywhere.

In particular, since being a proposition is a proposition, we only need to check that 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 propx (λ e → subst P (sym e) pb) (conn x)
  where abstract
    propx : is-prop (P x)
    propx = ∥-∥-rec is-prop-is-prop (λ e → subst (is-prop ∘ P) (sym e) prop) (conn x)

We can similarly define an elimination principle into sets.

module connected∙-elim-set
  {ℓ ℓ'} {X : Type∙ ℓ} {P : ⌞ X ⌟ → Type ℓ'}
  (conn : is-connected∙ X)
  (set : is-set (P (X .snd)))
  (pb : P (X .snd))
  (loops : ∀ (p : X .snd ≡ X .snd) → PathP (λ i → P (p i)) pb pb)
  where opaque

  elim : ∀ x → P x
  elim x = work (conn x)
    module elim where
      setx : is-set (P x)
      setx = ∥-∥-rec (is-hlevel-is-prop 2) (λ e → subst (is-set ∘ P) (sym e) set) (conn x)

      work : ∥ x ≡ X .snd ∥ → P x
      work = ∥-∥-rec-set setx
        (λ p → subst P (sym p) pb)
        (λ p q i → subst P (sym (∙-filler'' (sym p) q i)) (loops (sym p ∙ q) i))

  elim-β-point : elim (X .snd) ≡ pb
  elim-β-point = subst (λ c → elim.work (X .snd) c ≡ pb)
    (squash (inc refl) (conn (X .snd)))
    (transport-refl pb)

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

Closure properties🔗

As a property of types, enjoys closure properties very similar to those of and we establish them in much the same way, by proving that is preserved by retractions.

However, the definition of is-n-connected, which uses the explicit constructions of truncations for the base cases, is slightly annoying to work when is arbitrary: that’s the trade-off for it being easy to work with when is a known, and usually small, number. Therefore, we prove the following lemma by the recursion, establishing that the notion of connectedness could very well have been defined using the general uniformly.

is-n-connected-Tr : ∀ {ℓ} {A : Type ℓ} n → is-n-connected A (suc n) → is-contr (n-Tr A (suc n))
is-n-connected-Tr zero a-conn = ∥-∥-proj! do
  pt ← a-conn
  pure $ contr (inc pt) (λ x → n-Tr-is-hlevel 0 _ _)
is-n-connected-Tr (suc zero) a-conn =
  retract→is-hlevel 0
    (∥-∥₀-rec (n-Tr-is-hlevel 1) inc)
    (n-Tr-rec squash inc)
    (n-Tr-elim _ (λ _ → is-prop→is-set (n-Tr-is-hlevel 1 _ _)) λ _ → refl)
    a-conn
is-n-connected-Tr (suc (suc n)) a-conn = a-conn

The first closure property we’ll prove is very applicable: it says that any retract of an type is again Intuitively this is because any retraction can be extended to a retraction and contractible types are closed under retractions.

retract→is-n-connected
  : (n : Nat) (f : A → B) (g : B → A)
  → is-left-inverse f g → is-n-connected A n → is-n-connected B n
retract→is-n-connected 0 = _
retract→is-n-connected 1 f g h a-conn = f <$> a-conn
retract→is-n-connected (suc (suc n)) f g h a-conn =
  n-connected.from (suc n) $ retract→is-contr
    (n-Tr-rec! (inc ∘ f))
    (n-Tr-rec! (inc ∘ g))
    (n-Tr-elim! _ λ x → ap n-Tr.inc (h x))
    (is-n-connected-Tr (suc n) a-conn)

Since the truncation operator also preserves products, a remarkably similar argument shows that if and are then so is is.

×-is-n-connected
  : ∀ n → is-n-connected A n → is-n-connected B n → is-n-connected (A × B) n
×-is-n-connected 0 = _
×-is-n-connected (suc n) a-conn b-conn = n-connected.from n $ Equiv→is-hlevel 0
  n-Tr-product (×-is-hlevel 0 (n-connected.to n a-conn) (n-connected.to n b-conn))

Finally, we show the dual of two properties of truncations: if is then each path space is And if is then it is also connected. This latter property lets us count down in precisely the same way that is-hlevel-suc lets us count up.

Path-is-connected : ∀ n → is-n-connected A (suc n) → is-n-connected (Path A x y) n
Path-is-connected 0 = _
Path-is-connected {x = x} (suc n) conn = n-connected.from n (contr (ps _ _) $
  n-Tr-elim _ (λ _ → hlevel!)
    (J (λ y p → ps x y ≡ inc p) (Equiv.injective (Equiv.inverse n-Tr-path-equiv)
      (is-contr→is-set (is-n-connected-Tr _ conn) _ _ _ _))))
  where
    ps : ∀ x y → n-Tr (x ≡ y) (suc n)
    ps x y = Equiv.to n-Tr-path-equiv (is-contr→is-prop (is-n-connected-Tr _ conn) _ _)

is-connected-suc
  : ∀ {ℓ} {A : Type ℓ} n
  → is-n-connected A (suc n) → is-n-connected A n
is-connected-suc {A = A} zero _ = _
is-connected-suc {A = A} (suc n) w = n-connected.from n $ n-Tr-elim! _
    (λ x → contr (inc x) (n-Tr-elim _ (λ _ → hlevel!) (rem₁ n w x)))
    (is-n-connected-Tr (suc n) w .centre)
  where
    rem₁ : ∀ n → is-n-connected A (2 + n) → ∀ x y → Path (n-Tr A (suc n)) (inc x) (inc y)
    rem₁ zero a-conn x y = n-Tr-is-hlevel 0 _ _
    rem₁ (suc n) a-conn x y = Equiv.from n-Tr-path-equiv
      (n-Tr-rec (is-hlevel-suc _ (n-Tr-is-hlevel n)) inc
        (is-n-connected-Tr _ (Path-is-connected (2 + n) a-conn) .centre))

is-connected-+
  : ∀ {ℓ} {A : Type ℓ} (n k : Nat)
  → is-n-connected A (k + n) → is-n-connected A n
is-connected-+ n zero w = w
is-connected-+ n (suc k) w = is-connected-+ n k (is-connected-suc _ w)

In terms of propositional truncations🔗

There is an alternative definition of connectedness that avoids talking about arbitrary truncations, and is thus sometimes easier to work with. Generalising the special cases for (a type is if and only if it is inhabited) and (a type is if and only if it is inhabited and all points are merely equal), we can prove that a type is if and only if it is inhabited and all its path spaces are

We can use this to give a definition of connectedness that only makes use of propositional truncations, with the base case being that all types are

is-n-connected-∥-∥ : ∀ {ℓ} → Type ℓ → Nat → Type ℓ
is-n-connected-∥-∥ A zero = Lift _ ⊤
is-n-connected-∥-∥ A (suc n) =
  ∥ A ∥ × ∀ (a b : A) → is-n-connected-∥-∥ (a ≡ b) n

is-n-connected-∥-∥-is-prop : ∀ n → is-prop (is-n-connected-∥-∥ A n)
is-n-connected-∥-∥-is-prop zero = hlevel 1
is-n-connected-∥-∥-is-prop (suc n) = ×-is-hlevel 1 (hlevel 1)
  (Π-is-hlevel² 1 λ _ _ → is-n-connected-∥-∥-is-prop n)

We show that this is equivalent to the of a type being contractible, hence in turn to our first definition.

is-contr-n-Tr→∥-∥
  : ∀ n → is-contr (n-Tr A (suc n)) → is-n-connected-∥-∥ A (suc n)
is-contr-n-Tr→∥-∥ zero h .fst = n-Tr-rec! inc (h .centre)
is-contr-n-Tr→∥-∥ zero h .snd = _
is-contr-n-Tr→∥-∥ (suc n) h .fst = n-Tr-rec! inc (h .centre)
is-contr-n-Tr→∥-∥ (suc n) h .snd a b = is-contr-n-Tr→∥-∥ n
  (Equiv→is-hlevel 0 (n-Tr-path-equiv e⁻¹) (Path-is-hlevel 0 h))

∥-∥→is-contr-n-Tr
  : ∀ n → is-n-connected-∥-∥ A (suc n) → is-contr (n-Tr A (suc n))
∥-∥→is-contr-n-Tr zero (a , _) = is-prop∙→is-contr hlevel! (∥-∥-rec! inc a)
∥-∥→is-contr-n-Tr (suc n) (a , h) = ∥-∥-rec! (λ a → is-prop∙→is-contr
  (n-Tr-elim! _ λ a → n-Tr-elim! _ λ b →
    Equiv.from n-Tr-path-equiv (∥-∥→is-contr-n-Tr n (h a b) .centre))
  (inc a)) a

is-n-connected→∥-∥
  : ∀ n → is-n-connected A n → is-n-connected-∥-∥ A n
is-n-connected→∥-∥ zero _ = _
is-n-connected→∥-∥ (suc n) h = is-contr-n-Tr→∥-∥ n (n-connected.to n h)

∥-∥→is-n-connected
  : ∀ n → is-n-connected-∥-∥ A n → is-n-connected A n
∥-∥→is-n-connected zero _ = _
∥-∥→is-n-connected (suc n) h = n-connected.from n (∥-∥→is-contr-n-Tr n h)

is-n-connected≃∥-∥
  : ∀ n → is-n-connected A n ≃ is-n-connected-∥-∥ A n
is-n-connected≃∥-∥ {A = A} n = prop-ext
  (is-n-connected-is-prop {A = A} n) (is-n-connected-∥-∥-is-prop n)
  (is-n-connected→∥-∥ n) (∥-∥→is-n-connected n)

module n-connected-∥-∥ {ℓ} {A : Type ℓ} (n : Nat) =
  Equiv (is-n-connected≃∥-∥ {A = A} n)

In relation to truncatedness🔗

The following lemmas define of a type by how it can map into the truncated types. We then expand this idea to cover the maps, too. At the level of types, the “relative” characterisation of says that, if is and is then the function is an equivalence.

The intuitive idea behind this theorem is as follows: we have assumed that has no interesting information below dimension and that has no interesting information in the dimensions and above. Therefore, the functions can’t be interesting, since they’re mapping boring data into boring data.

The proof is a direct application of the definition of and the universal property of truncations: is equivalent to but this is equivalent to since is contractible.

is-n-connected→n-type-const
  : ∀ n → is-hlevel B (suc n) → is-n-connected A (suc n)
  → is-equiv {B = A → B} (λ b a → b)
is-n-connected→n-type-const {B = B} {A = A} n B-hl A-conn =
  subst is-equiv (λ i x z → transp (λ i → B) i x) $ snd $
  B                      ≃⟨ Π-contr-eqv (is-n-connected-Tr n A-conn) e⁻¹ ⟩≃
  (n-Tr A (suc n) → B)   ≃⟨ n-Tr-univ n B-hl ⟩≃
  (A → B)                ≃∎

This direction of the theorem is actually half of an equivalence. In the other direction, since is by definition, we suppose that is an equivalence. From the constructor we obtain a point and, for all we have

But by induction on truncation, this says precisely that any is equal to so is a centre of contraction, and is

n-type-const→is-n-connected
  : ∀ {ℓ} {A : Type ℓ} n
  → (∀ {B : Type ℓ} → is-hlevel B (suc n) → is-equiv {B = A → B} (λ b a → b))
  → is-n-connected A (suc n)
n-type-const→is-n-connected {A = A} n eqv =
  n-connected.from n $ contr (rem.from inc) $ n-Tr-elim _
    (λ h → Path-is-hlevel (suc n) (n-Tr-is-hlevel n)) (rem.ε inc $ₚ_)
  where module rem = Equiv (_ , eqv {n-Tr A (suc n)} hlevel!)

We can now generalise this to work with an map and a family of over in this setting, precomposition with is an equivalence

This is somewhat analogous to generalising from a recursion principle to an elimination principle. When we were limited to talking about types, we could extend points to functions but no dependency was possible. With the extra generality, we think of as including a space of “constructors”, and the equivalence says that exhibiting at these constructors is equivalent to exhibiting it for the whole type.

relative-n-type-const
  : (P : B → Type ℓ'') (f : A → B)
  → ∀ n → is-n-connected-map f n
  → (∀ x → is-hlevel (P x) n)
  → is-equiv {A = (∀ b → P b)} {B = (∀ a → P (f a))} (_∘ f)

Despite the generality, the proof is just a calculation: observing that we have the following chain of equivalences suffices.

  rem₁ =
    ((b : B) → P b)                             ≃⟨ Π-cod≃ (λ x → Π-contr-eqv {B = λ _ → P x} (is-n-connected-Tr _ (n-conn x)) e⁻¹) ⟩≃
    ((b : B) → n-Tr (fibre f b) (suc n) → P b)  ≃⟨ Π-cod≃ (λ x → n-Tr-univ n (phl _)) ⟩≃
    ((b : B) → fibre f b → P b)                 ≃⟨ shuffle ⟩≃
    ((a : A) → P (f a))                         ≃∎
There’s also the shuffle isomorphism that eliminates the fibre argument using path induction, but its construction is mechanical.
  shuffle = Iso→Equiv λ where
    .fst      g a         → g (f a) (a , refl)
    .snd .inv g b (a , p) → subst P p (g a)
    .snd .rinv g → funext λ a → transport-refl _
    .snd .linv g → funext λ b → funext λ { (a , p) →
      J (λ b p → subst P p (g (f a) (a , refl)) ≡ g b (a , p))
        (transport-refl _) p }

We can specialise this to get a literal elimination principle: If is a family of over an pointed type then holds everywhere if holds. Moreover, this has the expected computation rule.

module _ n (P : A → Type ℓ) (tr : ∀ x → is-hlevel (P x) n)
           {a₀ : A} (pa₀ : P a₀)
           (a-conn : is-n-connected A (suc n))
  where

  connected-elimination-principle : fibre (λ z x → z a₀) (λ _ → pa₀)
  connected-elimination-principle = relative-n-type-const {A = ⊤} P (λ _ → a₀) n
    (λ x → retract→is-n-connected n (λ p → tt , p) snd (λ _ → refl)
      (Path-is-connected n a-conn))
    tr .is-eqv (λ _ → pa₀) .centre

  opaque
    connected-elim : ∀ x → P x
    connected-elim = connected-elimination-principle .fst

    connected-elim-β : connected-elim a₀ ≡ pa₀
    connected-elim-β = connected-elimination-principle .snd $ₚ tt

Using these elimination principles, we can prove that a pointed type is if and only if the inclusion of is when considered as a map

is-n-connected-point
  : ∀ {ℓ} {A : Type ℓ} (a₀ : A) n
  → is-n-connected-map {A = ⊤} (λ _ → a₀) n
  → is-n-connected A (suc n)
is-n-connected-point {A = A} a₀ n pt-conn = done where
  rem : ∀ {B : Type ℓ} → is-hlevel B (suc n) → ∀ (f : A → B) a → f a₀ ≡ f a
  rem b-hl f = equiv→inverse
    (relative-n-type-const (λ a → f a₀ ≡ f a) _ n pt-conn λ x → Path-is-hlevel' n b-hl _ _)
    (λ _ → refl)

  done : is-n-connected A (suc n)
  done = n-type-const→is-n-connected n λ hl → is-iso→is-equiv $
    iso (λ f → f a₀) (λ f → funext λ a → rem hl f a) λ _ → refl

point-is-n-connected
  : ∀ {ℓ} {A : Type ℓ} (a₀ : A) n
  → is-n-connected A (2 + n)
  → is-n-connected-map {A = ⊤} (λ _ → a₀) (suc n)
point-is-n-connected a₀ n a-conn =
  connected-elim (suc n) (λ x → is-n-connected (⊤ × (a₀ ≡ x)) (suc n))
    (λ x → is-prop→is-hlevel-suc (is-n-connected-is-prop (suc n)))
    (retract→is-n-connected (suc n) (tt ,_) snd (λ _ → refl)
      (Path-is-connected {y = a₀} (suc n) a-conn))
    a-conn
relative-n-type-const-plus
  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} (P : B → Type ℓ'')
  → (f : A → B)
  → ∀ n k
  → is-n-connected-map f n
  → (∀ x → is-hlevel (P x) (k + n))
  → ∀ it → is-hlevel (fibre {A = ((b : B) → P b)} {B = (a : A) → P (f a)} (_∘ f) it) k

relative-n-type-const-plus P f n zero f-conn P-hl it = relative-n-type-const P f n f-conn P-hl .is-eqv it
relative-n-type-const-plus {A = A} {B = B} P f n (suc k) f-conn P-hl it = done where
  T = fibre {A = ((b : B) → P b)} {B = (a : A) → P (f a)} (_∘ f) it

  module _ (gp@(g , p) hq@(h , q) : T) where
    Q : B → Type _
    Q b = g b ≡ h b

    S = fibre {A = (∀ b → Q b)} {B = (∀ a → Q (f a))} (_∘ f) λ a → happly (p ∙ sym q) a

    rem₃ : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ y) → (p ≡ q) ≡ (refl ≡ p ∙ sym q)
    rem₃ {x = x} p q = J (λ y q → (p : x ≡ y) → (p ≡ q) ≡ (refl ≡ p ∙ sym q))
      (λ p → sym (ap (refl ≡_) (∙-idr p) ∙ Iso→Path (sym , iso sym (λ _ → refl) (λ _ → refl)))) q p

    abstract
      remark
        : ∀ {h} (α : g ≡ h) {q : h ∘ f ≡ it}
        → (PathP (λ i → α i ∘ f ≡ it) p q)
        ≃ (happly α ∘ f ≡ happly (p ∙ sym q))
      remark α = J
        (λ h α → {q : h ∘ f ≡ it} → PathP (λ i →  α i ∘ f ≡ it) p q ≃ (happly α ∘ f ≡ happly (p ∙ sym q)))
        (path→equiv (rem₃ _ _) ∙e (_ , embedding→cancellable {f = happly} λ x →
          is-contr→is-prop (is-iso→is-equiv
            (iso funext (λ _ → refl) (λ _ → refl)) .is-eqv x)))
        α

    to : Path T gp hq → S
    to α = happly (ap fst α) , remark (ap fst α) .fst (ap snd α)

    from : S → Path T gp hq
    from (a , b) = ap₂ _,_ (funext a) (Equiv.from (remark (funext a)) b)

    linv : is-left-inverse from to
    linv x = ap₂ (ap₂ _,_) refl (Equiv.η (remark _) _)

  done = Path-is-hlevel→is-hlevel k $ λ x y →
    retract→is-hlevel k (from _ _) (to _ _) (linv _ _) $
      relative-n-type-const-plus (Q x y) f n k f-conn
        (λ x → Path-is-hlevel' (k + n) (P-hl x) _ _) _