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,^{1} is connected, for the same reason
that there is no function of type
$(xy:S_{1})βxβ‘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 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.^{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 $Ο_{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!^{3}

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^{4}. 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`

.β©οΈ