module Homotopy.Connectedness where

Connectedness🔗

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

While being $n$ -truncated expresses that all homotopy groups above $n$ are trivial, being $n$ -connected means that all homotopy groups below $n$ are trivial. A type that is both $n$ -truncated and $n$ -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 $n$ -connected 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 $0$ -connected, and simply connected if it is $1$ -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 (λ _ → 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 $P$ that holds on the base point holds everywhere.

In particular, since being a proposition is a proposition, we only need to check that $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 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, $n$ -connectedness enjoys closure properties very similar to those of $n$ -truncatedness; and we establish them in much the same way, by proving that $n$ -connectedness 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 $n$ is arbitrary: that’s the trade-off for it being easy to work with when $n$ 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 $n$ -truncation 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 $n$ -connected type is again $n$ -connected. Intuitively this is because any retraction $f : A \to B$ can be extended to a retraction $\| A \|_n \to \| B \|_n$ , 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 $\| - \|_n$ also preserves products, a remarkably similar argument shows that if $A$ and $B$ are $n$ -connected, then so is $A \times B$ 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 $ 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 $A$ is $(1+n)$ -connected, then each path space $x \equiv_A y$ is $n$ -connected; And if $A$ is $(2+n)$ -connected, then it is also $(1+n$ ) 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 $n = -1$ (a type is $(-1)$ -connected if and only if it is inhabited) and $n = 0$ (a type is $0$ -connected if and only if it is inhabited and all points are merely equal), we can prove that a type is $n$ -connected if and only if it is inhabited and all its path spaces are $(n-1)$ -connected.

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 $(n-2)$ -connected:

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 $n$ -truncation 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
  (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 $n$ -connectedness of a type $A$ by how it can map into the $n$ -truncated types. We then expand this idea to cover the $n$ -connected maps, too. At the level of types, the “relative” characterisation of $n$ -connectedness says that, if $A$ is $n$ -connected and $B$ is $n$ -truncated, then the function $\mathrm{const} : B \to (A \to B)$ is an equivalence.

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

The proof is a direct application of the definition of $n$ -connectedness and the universal property of truncations: $A \to B$ is equivalent to $\| A \|_n \to B$ , but this is equivalent to $B$ since $\| A \|_n$ 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 $\| A \|_n$ is $n$ -truncated by definition, we suppose that $\mathrm{const} : \| A \|_n \to (A \to \| A \|_n)$ is an equivalence. From the constructor $\operatorname{inc} : A \to \| A \|_n$ we obtain a point $p : \| A \|_n$ , and, for all $a$ , we have

$p = \operatorname{const}(p)(a) = \operatorname{inc}(a)\text{.}$

But by induction on truncation, this says precisely that any $a : \| A \|_n$ is equal to $p$ ; so $p$ is a centre of contraction, and $A$ is $n$ -connected.

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 $n$ -connected map $f : A \to B$ and a family $P$ of $n$ -types over $B$ : in this setting, precomposition with $f$ is an equivalence

$(\Pi_{a : A} P(fa)) \to (\Pi_{b : B} P(b))\text{.}$

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 $b : B$ to functions $A \to B$ , but no dependency was possible. With the extra generality, we think of $f$ as including a space of “constructors”, and the equivalence says that exhibiting $P$ 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 $P$ is a family of $n$ -types over an $(1+n)$ -connected pointed type $(A, a_0)$ , then $P$ holds everywhere if $P(a_0)$ 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 $(A,a_0)$ is $(1+n)$ -connected if and only if the inclusion of $a_0$ is $n$ -connected when considered as a map $\top \to A$ .

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