module Cat.Connected where

Connected categories🔗

A precategory is connected 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.

record is-connected-cat {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
  no-eta-equality
  field
    point : ∥ Ob C ∥
    zigzag : ∀ x y → ∥ Meander C x y ∥

Notice the similarity with the notion of connectedness in homotopy type theory, particularly its formulation in terms of propositional truncations: this definition is essentially saying that the category has a connected homotopy type. In particular, the propositional truncations are important: without them, we could not prove that the delooping of the group of integers, seen as a univalent category,¹ is connected, for the same reason that there is no function of type $(x\,y : S^1) \to x \equiv y$ in the circle.

As a simple example, a category is connected if it has an initial or terminal object. In particular, the terminal category is connected.²

⊤Cat-is-connected : is-connected-cat ⊤Cat
⊤Cat-is-connected .point      = inc tt
⊤Cat-is-connected .zigzag _ _ = inc []

module _ {o ℓ} {C : Precategory o ℓ} where
  open Precategory C

  initial→connected : Initial C → is-connected-cat C
  initial→connected init = conn where
    open Initial init
    conn : is-connected-cat C
    conn .point = inc bot
    conn .zigzag x y = inc (zig ¡ (zag ¡ tt []))

  terminal→connected : Terminal C → is-connected-cat C
  terminal→connected term = conn where
    open Terminal term
    conn : is-connected-cat C
    conn .point = inc top
    conn .zigzag x y = inc (zag ! tt (zig ! []))

We now show that this definition 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 = ∥-∥-rec!
    (λ x → contr (inc x)
      (Coeq-elim-prop (λ _ → hlevel 1)
        λ y → ∥-∥-rec! (Meander-rec-≡ (π₀ C) inc quot)
          (conn .zigzag x y)))
    (conn .point)

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}$ : 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})$ , 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 (Ob 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 squash inc λ (x , y , fs) →
      ∥-∥-rec (squash _ _) (Meander-rec-≡ (π₀ C) inc quot) fs
    is .snd .is-iso.inv = Coeq-rec squash inc λ (x , y , f) →
      quot (inc (zig f []))
    is .snd .is-iso.rinv = Coeq-elim-prop (λ _ → squash _ _) λ _ → refl
    is .snd .is-iso.linv = Coeq-elim-prop (λ _ → squash _ _) λ _ → refl

    conn : is-connected-cat C
    conn .point = Coeq-elim-prop (λ _ → squash) inc (π₀-contr .centre)
    conn .zigzag x y = effective R
      (is-contr→is-prop (Iso→is-hlevel 0 is π₀-contr) (inc x) (inc y))

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

Either via the Rezk completion, or directly, as the discrete category on the groupoid $S^1$ .↩︎
But the initial category isn’t: even though any of its points would be connected by a zigzag, there are no such points.↩︎
In a general category, it may fail to be symmetric (we call those where it is pregroupoids), and it may fail to be valued in propositions (those are the thin categories).↩︎
Thinking of Zigzag, vaguely, as the reflexive, transitive and symmetric closure of Hom.↩︎