<!--
```agda
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
```
-->

```agda
module Cat.Connected where
```

# Connected categories {defines="connected-category"}

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.

```agda
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|connectedness-via-propositional-truncation]]: 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|delooping category]] of the group of [[integers]], seen as a
[[univalent category]],^[Either via the [[Rezk completion]], or
directly, as the [[discrete category]] on the groupoid $S^1$.] is
connected, for the same reason that there is no function of type $(x\,y
: S^1) \to x \equiv y$ in the [[circle]].

<!--
```agda
open is-connected-cat

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

unquoteDecl hl-is-connected-cat = declare-record-hlevel 1 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.^[But the [[initial category]] isn't: even though any of its
points *would* be connected by a zigzag, there are no such points.]

```agda
⊤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(\cC)$ to be [[contractible]].  The
forward implication easily follows from the elimination principle of
zigzags into sets:

```agda
  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(\cC)$ to zigzags, we would like to use the
[[effectivity]] of quotients, but the $\hom$ relation is not a
[[congruence]]!^[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]]).]

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^[Thinking of `Zigzag`{.Agda}, vaguely, as the reflexive,
transitive and symmetric closure of `Hom`{.Agda}.]. We can then show
that the [[quotient]] of this congruence is equivalent to $\pi_0(\cC)$,
so we can conclude that it is contractible and apply effectivity to get
a zigzag.

```agda
  π₀-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
```
