🔍

Equations Inline Footnotes

open import Cat.Instances.StrictCat.Cohesive
open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Localisation
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Groupoid
open import Cat.Prelude

import Cat.Morphism

open Congruence
open Functor

module Cat.Connected where

Connected categories🔗

We can straightforwardly adapt the definition of connectedness via propositional truncations from types ($\infty \text{-groupoids)}$ to $1\text{-}$pregroupoids:

record is-connected-groupoid {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
  no-eta-equality
  open Precategory C
  field
    point : ∥ Ob ∥
    path : ∀ x y → ∥ Hom x y ∥

{-# INLINE is-connected-groupoid.constructor #-}
open is-connected-groupoid

private unquoteDecl eqv = declare-record-iso eqv (quote is-connected-groupoid)

unquoteDecl hl-is-connected-groupoid = declare-record-hlevel  hl-is-connected-groupoid (quote is-connected-groupoid)

Note that this definition can be stated without requiring $\mathcal{C}$ to be a groupoid; however, for general categories, it is too strong: for example, we would like the walking arrow to be connected, but there is no morphism from $1$ to $0\text{.}$

Instead, we say that a precategory is connected if its total localisation is a connected groupoid; in other words, if it has exactly one connected component. Explicitly, this means that it has at least one object, and that every two objects can be connected by a finite zigzag of morphisms.

is-connected-cat : ∀ {o ℓ} (C : Precategory o ℓ) → Type (o ⊔ ℓ)
is-connected-cat C = is-connected-groupoid (Localisation C (Total C))

We define some helpers for proving that a concrete category $\mathcal{C}$ is connected: it suffices to exhibit an object $c:\mathcal{C}$ such that any other object $d$ is connected to $c$ by a zigzag (compare this with pointed connected types!).

module _ {o ℓ} {C : Precategory o ℓ} (gpd : is-pregroupoid C) where
  open Cat.Morphism C

  mk-connected-groupoid
    : (c : Ob) → (∀ x → Hom c x)
    → is-connected-groupoid C
  {-# INLINE mk-connected-groupoid #-}
  mk-connected-groupoid c paths = record where
    point = inc c
    path x y = inc (paths y ∘ gpd (paths x) .is-invertible.inv)

mk-connected-cat
  : ∀ {o ℓ} {C : Precategory o ℓ} (open Precategory C)
  → (c : Ob) → (∀ x → Meander C c x)
  → is-connected-cat C
{-# INLINE mk-connected-cat #-}
mk-connected-cat {C = C} = mk-connected-groupoid (Free-groupoid-is-groupoid C)

As a simple example, any category with an initial or terminal object is connected. In particular, the terminal category is connected.¹

⊤Cat-is-connected : is-connected-cat ⊤Cat
⊤Cat-is-connected = mk-connected-cat _ λ _ → []

module _ {o ℓ} {C : Precategory o ℓ} where
  private module C = Precategory C

  initial→connected : Initial C → is-connected-cat C
  initial→connected init = mk-connected-cat bot λ _ → zig ¡ []
    where open Initial init

  terminal→connected : Terminal C → is-connected-cat C
  terminal→connected term = mk-connected-cat top λ _ → zag ! _ []
    where open Terminal term

The opposite of a connected category is again connected.

  ^op-connected : is-connected-cat C → is-connected-cat (C ^op)
  ^op-connected conn .point = conn .point
  ^op-connected conn .path x y =
    Free-groupoid^op C .F₁ <$> conn .path y x

We now show that this definition of connectedness is equivalent to asking for the set of connected components ${\pi }_0(\mathcal{C})$ to be contractible. The forward implication easily follows from the elimination principle of zigzags into sets:

  connected→π₀-is-contr : is-connected-cat C → is-contr (π₀ ʻ C)
  connected→π₀-is-contr conn = case conn .point of λ x → contr (inc x)
    (elim! λ y → rec! (Meander-rec-≡ (π₀ C) inc quot) (conn .path x y))

Showing the converse implication is not as straightforward: in order to go from paths in ${\pi }_0(\mathcal{C})$ to zigzags, we would like to use the effectivity of quotients, but the $\mathbf{Hom}$ relation is not a congruence!²

Luckily, we can define the free congruence generated by $\mathbf{Hom}\text{:}$ two objects are related by this congruence if there merely exists a zigzag between them³. We can then show that the quotient of this congruence is equivalent to ${\pi }_0(\mathcal{C})\text{,}$ so we can conclude that it is contractible and apply effectivity to get a zigzag.

  π₀-is-contr→connected : is-contr (π₀ ʻ C) → is-connected-cat C
  π₀-is-contr→connected π₀-contr = conn where
    R : Congruence ⌞ C ⌟ (o ⊔ ℓ)
    R ._∼_ x y         = ∥ Meander C x y ∥
    R .has-is-prop _ _ = squash
    R .reflᶜ    = inc []
    R ._∙ᶜ_ p q = ∥-∥-map₂ _++_ q p
    R .symᶜ     = ∥-∥-map (reverse C)

    is : Iso (quotient R) (π₀ ʻ C)
    is .fst = Coeq-rec inc (elim! λ x y → Meander-rec-≡ (π₀ C) inc quot)
    is .snd .is-iso.from = Coeq-rec inc λ (x , y , f) →
      quot (inc (zig f []))
    is .snd .is-iso.rinv = elim! λ _ → refl
    is .snd .is-iso.linv = elim! λ _ → refl

    conn : is-connected-cat C
    conn .point = case π₀-contr .centre of λ { .inc* → inc }
    conn .path x y = effective R
      (is-contr→is-prop (Iso→is-hlevel  is π₀-contr) (inc x) (inc y))

  connected≃π₀-is-contr : is-connected-cat C ≃ is-contr (π₀ ʻ C)
  connected≃π₀-is-contr = prop-ext (hlevel ) (hlevel )
    connected→π₀-is-contr π₀-is-contr→connected

Connected categories enjoy the following recursion principle: to define a map $\Vert \mathcal{C}\Vert \to X\text{,}$ where $\mathcal{C}$ is a connected category and $X$ is a set, it suffices to give a map $r:|\mathcal{C}|\to X$ from the objects of $\mathcal{C}$ that gives the same result for any two objects connected by a morphism.

  connected-∥-∥-rec!
    : is-connected-cat C
    → ∀ {ℓ'} {X : Type ℓ'} ⦃ _ : H-Level X  ⦄
    → (r : C.Ob → X)
    → (∀ {x y} (f : C.Hom x y) → r x ≡ r y)
    → ∥ C.Ob ∥ → X
  connected-∥-∥-rec! conn r r-const = ∥-∥-rec-set! r λ x y →
    case conn .path x y of
      Meander-rec-≡ (el! _) r r-const