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 $π_{0} (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 .zigzag x y))

Showing the converse implication is not as straightforward: in order to go from paths in $π_{0} (C)$ to zigzags, we would like to use the effectivity of quotients, but the $Hom$ relation is not a congruence!³

Luckily, we can define the free congruence generated by $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 $π_{0} (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 ⌞ 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.inv = 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 = rec! 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.↩︎