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
    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,1 is connected, for the same reason that there is no function of type 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.2

⊀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 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 to zigzags, we would like to use the effectivity of quotients, but the relation is not a congruence!3

Luckily, we can define the free congruence generated by two objects are related by this congruence if there merely exists a zigzag between them4. We can then show that the quotient of this congruence is equivalent to 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

  1. Either via the Rezk completion, or directly, as the discrete category on the groupoid β†©οΈŽ

  2. But the initial category isn’t: even though any of its points would be connected by a zigzag, there are no such points.β†©οΈŽ

  3. 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).β†©οΈŽ

  4. Thinking of Zigzag, vaguely, as the reflexive, transitive and symmetric closure of Hom.β†©οΈŽ