<!--
```agda
open import Cat.Functor.WideSubcategory
open import Cat.Instances.Congruence
open import Cat.Functor.Base
open import Cat.Groupoid
open import Cat.Prelude

import Cat.Reasoning
```
-->

```agda
module Cat.Instances.Localisation where
```

# Localisations {defines=localisation}

<!--
```agda
module _ {o ℓ w} (C : Precategory o ℓ) (W : Wide-subcat C w) where
  open Precategory C
  open Wide-subcat W

  private variable
    a b c d : Ob
    f g h : Hom a b
```
-->

A problem in category theory which sounds simple but turns out to be
surprisingly tricky is **localisation**: constructing [[universal
solutions|free object]] to the problem of *inverting a given class of
morphisms.* More precisely, suppose that we have a category $\cC$ and a
[[wide subcategory]] $W \sube \cC$. The localisation $\cC\loc{W}$, if it
exists, should satisfy the following universal property:

- There is a functor $\cL : \cC \to \cC\loc{W}$ which *inverts every
  morphism in $W$*, in the sense that, if $f \in W$, then $\cL f$ is an
  isomorphism in $\cC$; and

- If we're given a category $\cD$, and a functor $F : \cC \to \cD$ which
  *also* inverts every morphism in $W$ (i.e., if $f \in W$, then $F(f)$
  is an [[isomorphism]] in $\cD$), then there is a *unique* functor
  $\tilde{F} : \cC\loc{W} \to \cD$ which satisfies $\tilde{F} \cL \cong
  F$.

::: {.definition #zigzag}
The construction we present here is similar to that of the [[free
category]] on a graph. However, instead of *paths*, we will use
structures called *zigzags*. The idea is simple: in a path, all edges
must be oriented the same way; but in a zigzag, we have edges going
forward, and edges going backward! The backwards edges are *formal
inverses* for the morphisms from $W$. We can picture a general zigzag
as follows:
:::

~~~{.quiver}
\[\begin{tikzcd}[ampersand replacement=\&]
  \& b \&\& d \\
  a \&\& c
  \arrow["f"', color={rgb,255:red,214;green,92;blue,214}, from=1-2, to=2-1]
  \arrow["g"', from=1-2, to=2-3]
  \arrow["h", color={rgb,255:red,214;green,92;blue,214}, from=1-4, to=2-3]
\end{tikzcd}\]
~~~

The diagram represents a zigzag from $a$ to $d$. But pay attention to
the orientation of the pink edges: they're backwards! This zigzag
represents a morphism that did not necessarily exist in $\cC$: composing
the *inverse* of $f$, $g$, and the *inverse* of $h$. If $f$ and $h$ were
not isomorphisms before, we would have nothing to fill the pink edges
with!

```agda
  data Zigzag : Ob → Ob → Type (o ⊔ ℓ ⊔ w) where
    []  : Zigzag a a
    zig : Hom b c → Zigzag a b → Zigzag a c
    zag : (f : Hom c b) → f ∈ W → Zigzag a b → Zigzag a c
```

However, if we treat zigzags as plain *data*, things go wrong. We must
also impose relations, corresponding to functoriality of $\cL$, and to
make the formal inverses into... inverses. Using a higher inductive type
makes this extremely natural: we can add these relations as higher
constructors, which saves us from defining the least congruence
generated by the relations we want.

First, we have functoriality: these are straightforward. Note that we
only need functoriality in the _forwards_ direction; functoriality of
the inverses will follow by uniqueness.

```agda
    zig-id : (h : Zigzag a b) → zig id h ≡ h
    zig-∘  : (f : Hom c d) (g : Hom b c) (h : Zigzag a b)
           → zig f (zig g h) ≡ zig (f ∘ g) h
```

Next, we need laws that allow us to collapse zigzags. These say that if
we have a zigzag starting with

~~~{.quiver}
\[\begin{tikzcd}[ampersand replacement=\&]
  \& b \&\& \dots \\
  a \&\& a
  \arrow["f"', color={rgb,255:red,214;green,92;blue,214}, from=1-2, to=2-1]
  \arrow["f", from=1-2, to=2-3]
  \arrow["g", from=2-3, to=1-4]
\end{tikzcd}\]
~~~

then we can get rid of the extra "roof" $a \xot{f} b \xto{f} a$,
standing for the composition of $f$ and its inverse; We have the
symmetric rule in case the inverse comes second, too. Note that since
these are generators for the *identity type* in zigzags, we can apply
them anywhere, not just at the start: any context in which a zig-zag or
zag-zig could appear will respect this identity.

```agda
    zig-zag
      : (f : Hom c b) (w : f ∈ W) (h : Zigzag a b)
      → zig f (zag f w h) ≡ h
    zag-zig
      : (f : Hom b c) (w : f ∈ W) (h : Zigzag a b)
      → zag f w (zig f h) ≡ h
```

Finally, we must ensure that the type of zigzags is a [[set]], by
truncating it. This is unlike the case with the category of paths in a
graph, which *worked out* to be a set due to the careful setup: there
are no relations imposed, and the vertices in a graph must be drawn from
a set, unlike the objects in a general [[precategory]].

```agda
    squash : ∀ {a b} → is-set (Zigzag a b)
```

::: warning
The localisation of a *locally small* category $\cC$ at a class $W$ is
not necessarily locally small! This is because the data of a zigzag
technically includes the names of the objects in the intermediate steps,
and objects may live at a higher universe level than morphisms. However,
if $\cC$ was *small*, then all of its localisations will be, as well.
:::

<details>
<summary>It follows from uniqueness of isomorphisms that the inclusion
of $W$ into $\cC\loc{W}$ is also functorial. The calculations
are not particularly terrifying, but they are standard, so we'll skip
over them for time.
</summary>

```agda
  abstract
    zag-id : ∀ {a b} (fs : Zigzag a b) → zag id P-id fs ≡ fs
    zag-id fs =
      zag id P-id ⌜ fs ⌝       ≡˘⟨ ap¡ (zig-id fs) ⟩
      zag id P-id (zig id fs)  ≡⟨ zag-zig id _ fs ⟩
      fs                       ∎

    zag-∘
      : ∀ {a b c d} {f : Hom c d} {g : Hom b c} (hs : Zigzag a d)
      → (hf : f ∈ W) (hg : g ∈ W)
      → zag (f ∘ g) (P-∘ hf hg) hs ≡ zag g hg (zag f hf hs)
    zag-∘ {f = f} {g} hs hf hg =
      zag (f ∘ g) (P-∘ hf hg) ⌜ hs ⌝                                      ≡˘⟨ ap¡ (ap (zig f) (zig-zag _ _ _) ∙ zig-zag _ _ _) ⟩
      zag (f ∘ g) (P-∘ hf hg) ⌜ zig f (zig g (zag g hg (zag f hf hs))) ⌝  ≡⟨ ap! (zig-∘ f g _) ⟩
      zag (f ∘ g) (P-∘ hf hg) (zig (f ∘ g) (zag g hg (zag f hf hs)))      ≡⟨ zag-zig (f ∘ g) _ _ ⟩
      zag g hg (zag f hf hs)                                              ∎
```

</details>

<!--
```agda
module _ {o ℓ w} {C : Precategory o ℓ} {W : Wide-subcat C w} where
  open Wide-subcat W
  instance
    H-Level-Zigzag : ∀ {a b n} → H-Level (Zigzag C W a b) (2 + n)
    H-Level-Zigzag = basic-instance 2 squash

  open Precategory C

  Zigzag-elim
    : ∀ {ℓ'} (P : ∀ {a b} → Zigzag C W a b → Type ℓ')
    → (∀ {a b} (h : Zigzag C W a b) → is-set (P h))
    → (hnil : ∀ {a} → P {a} [])
    → (hzig : ∀ {a b c} (f : Hom b c) (h : Zigzag C W a b) → P h → P (zig f h))
    → (hzag : ∀ {a b c} (f : Hom c b) (hf : f ∈ W) (h : Zigzag C W a b) → P h → P (zag f hf h))
    → (∀ {a b} {h : Zigzag C W a b} (ph : P h) → PathP (λ i → P (zig-id h i)) (hzig id h ph) ph)
    → (∀ {a b c d} {f : Hom c d} {g : Hom b c} {h : Zigzag C W a b} (ph : P h)
      → PathP (λ i → P (zig-∘ f g h i)) (hzig f (zig g h) (hzig g h ph)) (hzig (f ∘ g) h ph))
    → (∀ {a b c} {f : Hom c b} {w : f ∈ W} {h : Zigzag C W a b} (ph : P h)
      → PathP (λ i → P (zig-zag f w h i)) (hzig f (zag f w h) (hzag f w h ph)) ph)
    → (∀ {a b c} {f : Hom b c} {w : f ∈ W} {h : Zigzag C W a b} (ph : P h)
      → PathP (λ i → P (zag-zig f w h i)) (hzag f w (zig f h) (hzig f h ph)) ph)
    → ∀ {a b} (h : Zigzag C W a b) → P h
  Zigzag-elim P pset pnil pzig pzag pzid pzo pia pai = go where
    go : ∀ {a b} (h : Zigzag C W a b) → P h
    go [] = pnil
    go (zig f h) = pzig f h (go h)
    go (zag f hf w) = pzag f hf w (go w)
    go (zig-id x i) = pzid (go x) i
    go (zig-∘ f g x i) = pzo (go x) i
    go (zig-zag f w x i) = pia (go x) i
    go (zag-zig f w x i) = pai (go x) i
    go (squash x y p q i j) = is-set→squarep (λ i j → pset (squash x y p q i j)) (λ i → go x) (λ i → go (p i)) (λ i → go (q i)) (λ i → go y) i j

  abstract
    Zigzag-elim-prop
      : ∀ {ℓ'} (P : ∀ {a b} → Zigzag C W a b → Type ℓ')
      → ⦃ ∀ {a b} {h : Zigzag C W a b} → H-Level (P h) 1 ⦄
      → (hnil : ∀ {a} → P {a} [])
      → (hzig : ∀ {a b c} (f : Hom b c) (h : Zigzag C W a b) → P h → P (zig f h))
      → (hzag : ∀ {a b c} (f : Hom c b) (hf : f ∈ W) (h : Zigzag C W a b) → P h → P (zag f hf h))
      → ∀ {a b} (h : Zigzag C W a b) → P h
    Zigzag-elim-prop P hnil hzig hzag =
      Zigzag-elim P (λ h → is-prop→is-set (hlevel 1))
        hnil hzig hzag
        (λ _ → prop!) (λ _ → prop!) (λ _ → prop!) (λ _ → prop!)
```
-->

Composition of zigzags is perfectly straightforward. On the data, it's
exactly concatenation of lists, or composition of paths. Since
composition _sinks to the right_ when presented with explicit
constructors, respect for the imposed relations also very nicely mirrors
the definition of concatenation itself.

```agda
  _++_ : ∀ {a b c} → Zigzag C W b c → Zigzag C W a b → Zigzag C W a c
  []                 ++ f = f
  zig g h            ++ f = zig g (h ++ f)
  zag g hg h         ++ f = zag g hg (h ++ f)
  zig-id g i         ++ f = zig-id (g ++ f) i
  zig-∘ g g' h i     ++ f = zig-∘ g g' (h ++ f) i
  zig-zag g hg h i   ++ f = zig-zag g hg (h ++ f) i
  zag-zig g hg h i   ++ f = zag-zig g hg (h ++ f) i
  squash x y p q i j ++ f = squash
    (x ++ f) (y ++ f) (λ i → p i ++ f) (λ i → q i ++ f) i j
```

The definition above is definitionally unital on the left; We must show
that this is also the case on the right. Since we're showing identity of
zigzags, which is a [[proposition]], it suffices to cover the data; the
relations are automatically respected. While the proofs are slightly
obfuscated due to the higher-order nature of eliminators, they once
again mirror precisely the proofs for lists, or simple paths.

```agda
  abstract
    ++-nil : ∀ {a b} (fs : Zigzag C W a b) → fs ++ [] ≡ fs
    ++-nil = Zigzag-elim-prop (λ h → h ++ [] ≡ h)
      refl (λ f h p → ap (zig f) p) (λ f hf h p → ap (zag f hf) p)

    ++-assoc
      : ∀ {a b c d} (fs : Zigzag C W c d) (gs : Zigzag C W b c) (hs : Zigzag C W a b)
       → (fs ++ gs) ++ hs ≡ fs ++ (gs ++ hs)
    ++-assoc = Zigzag-elim-prop (λ fs → ∀ gs hs → (fs ++ gs) ++ hs ≡ fs ++ (gs ++ hs))
      (λ gs hs → refl)
      (λ f h p gs hs → ap (zig f) (p gs hs))
      (λ f hf h p gs hs → ap (zag f hf) (p gs hs))
```

<!--
```agda
module _ {o ℓ w} (C : Precategory o ℓ) (W : Wide-subcat C w) where
  private module C = Cat.Reasoning C
  open Wide-subcat W
  open Precategory
  open Functor
```
-->

We thus have the localisation as a [[precategory]]. The localisation
functor $\cL : \cC \to \cC\loc{W}$ sends a morphism $f : a \to b$ to the
singleton zigzag consisting of $f$ pointing forwards. Finally, if $f \in
W$, then we're also allowed to draw it backards; and this inverts $\cL
f$. Since we're just writing down things we've already shown, there's a
bit of code with not much more we could say:

```agda
  Localisation : Precategory o (ℓ ⊔ o ⊔ w)
  Localisation .Ob          = C.Ob
  Localisation .Hom         = Zigzag C W
  Localisation .Hom-set _ _ = hlevel 2

  Localisation .id  = []
  Localisation ._∘_ = _++_

  Localisation .idr f       = ++-nil f
  Localisation .idl f       = refl
  Localisation .assoc f g h = sym (++-assoc f g h)

  module Localisation = Cat.Reasoning Localisation

  Localise : Functor C Localisation
  Localise .F₀ X    = X
  Localise .F₁ f    = zig f []
  Localise .F-id    = zig-id []
  Localise .F-∘ f g = sym (zig-∘ f g [])

  inverted : ∀ {a b} (f : C.Hom a b) → f ∈ W → Localisation.is-invertible (zig f [])
  inverted f hf = record
    { inv      = zag f hf []
    ; inverses = record
      { invl = zig-zag f hf [] ; invr = zag-zig f hf [] } }
```

## The universal property

<!--
```agda
  module
    _ {o' ℓ'} {D : Precategory o' ℓ'} (F : Functor C D)
      (let module D = Cat.Reasoning D)
      (let module F = Functor F)
      (f-invs : ∀ {a b} (f : C.Hom a b) → f ∈ W → D.is-invertible (F.₁ f))
    where
```
-->

Having constructed the localisation as a higher-inductive type, proving
the proper universal property becomes a straightforward exercise in
rearranging data. That's because the data of *a functor $F : \cC \to
\cD$ which inverts $W$*, together with the data of the category $\cD$,
gives us exactly what we need to handle each of the constructors:

```agda
    private
      F⁻¹ : ∀ {a b} (f : C.Hom a b) (hf : f ∈ W) → D.Hom (F.₀ b) (F.₀ a)
      F⁻¹ f hf = D.is-invertible.inv (f-invs f hf)

    Zigzag-univ : ∀ {a b} → Zigzag C W a b → D.Hom (F.₀ a) (F.₀ b)
    Zigzag-univ []           = D.id
    Zigzag-univ (zig f h)    = F.₁ f D.∘ Zigzag-univ h
    Zigzag-univ (zag f hf h) = F⁻¹ f hf D.∘ Zigzag-univ h
```

Composing in the forwards direction uses the normal action of the
functor $F$; Composing _backwards_ uses the proof that $F$ sends $f : a
\to b \in W$ to an isomorphism, so we have a choice of inverse $f\inv :
b \to a$. The relations need a bit of re-arranging, to deal with
associativity, but they are also very pleasant:

```agda
    Zigzag-univ (zig-id h i)      = D.eliml F.F-id {f = Zigzag-univ h} i
    Zigzag-univ (zig-∘ f g h i)   = D.pushl (F.F-∘ f g) {f = Zigzag-univ h} (~ i)
    Zigzag-univ (zig-zag f w h i) = D.cancell (D.is-invertible.invl (f-invs f w)) {f = Zigzag-univ h} i
    Zigzag-univ (zag-zig f w h i) = D.cancell (D.is-invertible.invr (f-invs f w)) {f = Zigzag-univ h} i
    Zigzag-univ (squash x y p q i j) = D.Hom-set _ _
      (Zigzag-univ x) (Zigzag-univ y) (λ i → Zigzag-univ (p i)) (λ i → Zigzag-univ (q i)) i j
```

<details>
<summary>Finally, a straightforward inductive proof establishes that
this procedure preserves composition of zigzags. It preserves the
identity definitionally.</summary>

```agda
    abstract
      Zigzag-univ-++
        : ∀ {a b c} (f : Zigzag C W b c) (g : Zigzag C W a b)
        → Zigzag-univ (f ++ g) ≡ Zigzag-univ f D.∘ Zigzag-univ g
      Zigzag-univ-++ = Zigzag-elim-prop
        (λ f → ∀ g → Zigzag-univ (f ++ g) ≡ Zigzag-univ f D.∘ Zigzag-univ g)
        (λ g → D.introl refl)
        (λ f h p g → ap (F.₁ f D.∘_) (p g) ∙ D.pulll refl)
        (λ f hf h p g → ap (F⁻¹ f hf D.∘_) (p g) ∙ D.pulll refl)
```

</details>

Since `Zigzag-univ`{.Agda} computes so nicely, the proof of the
universal property is incredibly straightforward, and we actually get a
stronger result than we bargained for: not only do we have a natural
isomorphism $\cL \tilde{F} \cong F$, it's actually an identity, *even
if* the categories involved are not [[univalent categories]].

```agda
    Localisation-univ : Functor Localisation D
    Localisation-univ .F₀   = F.₀
    Localisation-univ .F₁   = Zigzag-univ
    Localisation-univ .F-id = refl
    Localisation-univ .F-∘  = Zigzag-univ-++

    Localisation-univ-β : F ≡ Localisation-univ F∘ Localise
    Localisation-univ-β = Functor-path (λ _ → refl) (λ _ → D.intror refl)
```

We can also show a uniqueness principle, saying that extending the
localisation functor results in the identity.

```agda
  Localisation-univ-η : Localisation-univ Localise inverted ≡ Id
  Localisation-univ-η = Functor-path (λ _ → refl) $ Zigzag-elim-prop
    (λ h → Zigzag-univ Localise inverted h ≡ h)
    refl (λ f h p → ap (zig f) p) (λ f hf h p → ap (zag f hf) p)
```

To conclude this section, we make note of a slight triviality: if every
morphism in $W$ was *already* invertible, then we can map from the
localisation back to $\cC$:

```agda
  Localisation-fold
    : (∀ {a b} (f : C.Hom a b) → f ∈ W → C.is-invertible f)
    → Functor Localisation C
  Localisation-fold invs = Localisation-univ Id invs
```

## Total localisations {defines="free-groupoid"}

<!--
```agda
module _ {o ℓ} (C : Precategory o ℓ) where
  open Precategory C

  Total : Wide-subcat C lzero
  Total .Wide-subcat.P      _ = ⊤
  Total .Wide-subcat.P-prop f = hlevel 1
  Total .Wide-subcat.P-id     = _
  Total .Wide-subcat.P-∘      = _
```
-->

An important special case of localisation is the **total localisation**
$\cC\loc{\cC}$, which computes the free groupoid on a category: the
universal solution to inverting _every_ morphism in $\cC$. To make it
clear what we're talking about, we'll refer to zigzags in the total
localisation as _meanders_. The setup is the same: we're just allowing
ourselves to draw _every_ morphism backwards.

```agda
  Meander : Ob → Ob → Type _
  Meander = Zigzag C Total
```

To show that the total localisation is a [[pregroupoid]], we'll have to
compute the inverse of an arbitrary meander. Following standard
functional programming practice, we first define a _reverse append_
operation, which composes against the *inverse* of its first argument,
and then define `reverse`{.Agda} by appending onto the empty zigzag.

```agda
  _r++_ : ∀ {a b c} → Meander c b → Meander a b → Meander a c
  []                 r++ f = f
  zig g h            r++ f = h r++ zag g tt f
  zag g hg h         r++ f = h r++ zig g f
  zig-id g i         r++ f = g r++ zag-id _ _ f i
  zig-∘ g g' h i     r++ f = h r++ zag-∘ C Total {f = g} {g'} f tt tt (~ i)
  zig-zag g hg h i   r++ f = h r++ zig-zag g tt f i
  zag-zig g hg h i   r++ f = h r++ zag-zig g tt f i
  squash x y p q i j r++ f = squash (x r++ f) (y r++ f) (λ i → p i r++ f) (λ i → q i r++ f) i j

  reverse : ∀ {a b} → Meander a b → Meander b a
  reverse fs = fs r++ []
```

<details>
<summary>We then have a battery of lemmas connecting these two
operations with the standard composition, all shown by straightforward
induction.</summary>

```agda
  abstract
    r++-assoc
      : ∀ {a b c d} (fs : Meander d c) (gs : Meander b c) (hs : Meander a b)
      → (fs r++ gs) ++ hs ≡ fs r++ (gs ++ hs)
    r++-assoc = Zigzag-elim-prop (λ fs → ∀ gs hs → (fs r++ gs) ++ hs ≡ fs r++ (gs ++ hs))
      (λ _ _ → refl)
      (λ f fs rec gs hs → rec _ _)
      (λ f hf fs rec gs hs → rec _ _)

    r++-assoc'
      : ∀ {a b c d} (fs : Meander b c) (gs : Meander d c) (hs : Meander a b)
      → (fs r++ gs) r++ hs ≡ gs r++ (fs ++ hs)
    r++-assoc' = Zigzag-elim-prop (λ f → ∀ g h → (f r++ g) r++ h ≡ g r++ (f ++ h))
      (λ _ _ → refl)
      (λ f fs rec gs hs → rec _ _)
      (λ f h fs rec gs hs → rec _ _)

    r++-reverse
      : ∀ {a b c} (fs : Meander c b) (gs : Meander a b)
      → reverse fs ++ gs ≡ fs r++ gs
    r++-reverse fs gs = r++-assoc fs [] gs
```

</details>

Finally, we can show that inverse-appending $f$ onto $f$ gives the
identity. With the lemmas proved in the `<details>`{.html} block above,
we can conclude that the `reverse`{.Agda} of a zigzag is actually its
categorical *inverse* in the total localisation $\cC\loc{\cC}$.

```agda
    r++-cancel : ∀ {a b} (fs : Meander a b) → fs r++ fs ≡ []
    r++-cancel = Zigzag-elim-prop (λ fs → fs r++ fs ≡ [])
      refl
      (λ f    fs rec → ap (fs r++_) (zag-zig _ _ _) ∙ rec)
      (λ f tt fs rec → ap (fs r++_) (zig-zag _ _ _) ∙ rec)

    reverse-invo : ∀ {a b} (fs : Meander a b) → reverse (reverse fs) ≡ fs
    reverse-invo fs = r++-assoc' fs [] [] ∙ ++-nil fs

    reverse-invl : ∀ {a b} (fs : Meander a b) → reverse fs ++ fs ≡ []
    reverse-invl fs = r++-reverse fs fs ∙ r++-cancel fs

    reverse-invr : ∀ {a b} (fs : Meander a b) → fs ++ reverse fs ≡ []
    reverse-invr fs = ap (_++ reverse fs) (sym (reverse-invo fs))
                    ∙ reverse-invl (reverse fs)
```

As we put together the construction of the `Free-groupoid`{.Agda}, we
should note the following rephrasing of its universal property: it is
the [[left adjoint]] to the inclusion of groupoids into
categories,[^biadjunction] which fits into an adjoint *triple*

$$
\operatorname{Free} \dashv U \dashv \operatorname{Core}
$$

with the right adjoint being the [[*core*]] functor --- the *co*free
groupoid on a category.

[^biadjunction]:
  Technically speaking, the inclusion of $\Grpd$ into $\Cat$ is a
  [[pseudofunctor]], and so this should be a *bi*adjoint cylinder.
  However, biadjunctions are very complicated objects, so it's fine ---
  though slightly inaccurate --- to work intuitively at the level of
  1-categories.

```agda
  Free-groupoid : Precategory o (o ⊔ ℓ)
  Free-groupoid = Localisation C Total

  Free-groupoid-is-groupoid : is-pregroupoid Free-groupoid
  Free-groupoid-is-groupoid f = record
    { inv = reverse f
    ; inverses = record
      { invl = reverse-invr f
      ; invr = reverse-invl f
      }
    }
```

Finally, we'll show the universal property of the free groupoid as a
special case of mapping *any* localisation $\cC\loc{W}$ into a groupoid
$\cD$. Since any functor $F : \cC \to \cD$ sends *everything* to an
isomorphism, including the class $W$, we're always allowed to extend $F$
to map from $\cC\loc{W}$, instead.

```agda
Localisation-univ-groupoid
  : ∀ {o ℓ w o' ℓ'} {C : Precategory o ℓ} {W : Wide-subcat C w}
  → {D : Precategory o' ℓ'} (d-grpd : is-pregroupoid D)
  → Functor C D
  → Functor (Localisation C W) D
Localisation-univ-groupoid dg F = Localisation-univ _ _ F λ f _ → dg _
```

<!--
```agda
Free-groupoid-map
  : ∀ {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
  → Functor C D → Functor (Free-groupoid C) (Free-groupoid D)
Free-groupoid-map F = Localisation-univ-groupoid
  (Free-groupoid-is-groupoid _)
  (Localise _ _ F∘ F)

Free-groupoid-counit
  : ∀ {o ℓ} {C : Precategory o ℓ}
  → is-pregroupoid C
  → Functor (Free-groupoid C) C
Free-groupoid-counit C-grpd = Localisation-fold _ _ λ f _ → C-grpd f
```
-->

<!--
```agda
module _ {o ℓ} {C : Precategory o ℓ} where
  open Precategory C
```
-->

Specialising the universal property to [[thin|thin category]] groupoids
(i.e. [[congruences|congruences as groupoids]]), we obtain useful
recursion principles for showing that objects connected by zigzags are
related.

```agda
  Meander-rec-congruence
    : ∀ {ℓ'} (R : Congruence Ob ℓ') (open Congruence R)
    → (∀ {a b} → Hom a b → a ∼ b)
    → ∀ {x y} → Meander C x y → x ∼ y
  Meander-rec-congruence R h = Localisation-univ-groupoid (congruence→groupoid R)
    (congruence-functor R (λ x → x) h) .Functor.F₁

  Meander-rec-≡
    : ∀ {ℓ'} (D : Set ℓ')
    → (f : Ob → ∣ D ∣)
    → (∀ {x y} → Hom x y → f x ≡ f y)
    → ∀ {x y} → Meander C x y → f x ≡ f y
  Meander-rec-≡ D f = Meander-rec-congruence (Kernel-pair (D .is-tr) f)
```
