defn: Localisations and final functors (#348)

# Description

Closes #335 in the maximally annoying way, by using the 
fully correct definition of final functors.

---

Co-authored-by: Amélia Liao <me@amelia.how>

src/1Lab/Path.lagda.md

@@ -476,6 +476,14 @@ subst : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} (P : A → Type ℓ₂) {x y : A}
 subst P p x = transp (λ i → P (p i)) i0 x
 ```
 
+<!--
+```agda
+subst₂ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} (P : A → B → Type ℓ₃) {a a' : A} {b b' : B}
+       → a ≡ a' → b ≡ b' → P a b → P a' b'
+subst₂ P p q x = transp (λ i → P (p i) (q i)) i0 x
+```
+-->
+
 ### Computation
 
 In “Book HoTT”, `transport`{.Agda} is defined using path induction, and

src/Cat/Connected.lagda.md

@@ -0,0 +1,145 @@
+<!--
+```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)
+
+instance
+  H-Level-is-connected-cat
+    : ∀ {k o ℓ} {C : Precategory o ℓ}
+    → H-Level (is-connected-cat C) (1 + k)
+  H-Level-is-connected-cat = basic-instance 1 (Iso→is-hlevel 1 eqv (hlevel 1))
+```
+-->
+
+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 = ∥-∥-rec!
+    (λ x → contr (inc x)
+      (Coeq-elim-prop (λ _ → hlevel 1)
+        λ y → ∥-∥-rec! (Meander-rec-≡ (π₀ C) inc quot)
+          (conn .zigzag x y)))
+    (conn .point)
+```
+
+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 (Ob 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 squash inc λ (x , y , fs) →
+      ∥-∥-rec (squash _ _) (Meander-rec-≡ (π₀ C) inc quot) fs
+    is .snd .is-iso.inv = Coeq-rec squash inc λ (x , y , f) →
+      quot (inc (zig f []))
+    is .snd .is-iso.rinv = Coeq-elim-prop (λ _ → squash _ _) λ _ → refl
+    is .snd .is-iso.linv = Coeq-elim-prop (λ _ → squash _ _) λ _ → refl
+
+    conn : is-connected-cat C
+    conn .point = Coeq-elim-prop (λ _ → squash) 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
+```

src/Cat/Diagram/Terminal.lagda.md

@@ -1,5 +1,8 @@
 <!--
 ```agda
+open import Cat.Instances.Shape.Terminal
+open import Cat.Functor.Adjoint.Hom
+open import Cat.Functor.Adjoint
 open import Cat.Prelude
 ```
 -->
@@ -83,3 +86,25 @@ is-terminal-iso isom term x = contr (isom .to ∘ term x .centre) λ h →
   isom .to ∘ isom .from ∘ h ≡⟨ cancell (isom .invl) ⟩
   h                         ∎
 ```
+
+## In terms of right adjoints
+
+We prove that the inclusion functor of an object $x$ of $\cC$ is right adjoint
+to the unique functor $\cC \to \top$ if and only if $x$ is terminal.
+
+```agda
+module _ (x : Ob) (term : is-terminal x) where
+  terminal→inclusion-is-right-adjoint : !F ⊣ const! {A = C} x
+  terminal→inclusion-is-right-adjoint =
+    hom-iso→adjoints (e _ .fst) (e _ .snd)
+      λ _ _ _ → term _ .paths _
+    where
+      e : ∀ y → ⊤ ≃ Hom y x
+      e y = is-contr→≃ (hlevel 0) (term y)
+
+module _ (x : Ob) (adj : !F ⊣ const! {A = C} x) where
+  inclusion-is-right-adjoint→terminal : is-terminal x
+  inclusion-is-right-adjoint→terminal y = is-hlevel≃ 0
+    (Σ-contract (λ _ → hlevel 0) e⁻¹)
+    (R-adjunct-is-equiv adj .is-eqv _)
+```