module Cat.Connected whereConnected 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 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 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→connectedEither via the Rezk completion, or directly, as the discrete category on the groupoid ↩︎
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 ofHom.↩︎