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.Prelude

open Precategory
open Congruence
open Functor

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 $(xy:S^1)\to x\equiv y$ in the circle.

open is-connected-cat

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

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

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 = 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 ${\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.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  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