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

module Cat.Instances.Localisation where

Localisations🔗

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 to the problem of inverting a given class of morphisms. More precisely, suppose that we have a category $\mathcal{C}$ and a wide subcategory $W\subseteq \mathcal{C}\text{.}$ The localisation $\mathcal{C}[W^{-1}]\text{,}$ if it exists, should satisfy the following universal property:

• There is a functor $\mathcal{L}:\mathcal{C}\to \mathcal{C}[W^{-1}]$ which inverts every morphism in $W$, in the sense that, if $f\in W\text{,}$ then $\mathcal{L}f$ is an isomorphism in $\mathcal{C}\text{;}$ and

• If we’re given a category $\mathcal{D}\text{,}$ and a functor $F:\mathcal{C}\to \mathcal{D}$ which also inverts every morphism in $W$ (i.e., if $f\in W\text{,}$ then $F(f)$ is an isomorphism in $\mathcal{D}\text{),}$ then there is a unique functor $\tilde{F}:\mathcal{C}[W^{-1}]\to \mathcal{D}$ which satisfies $\tilde{F}\mathcal{L}\cong F\text{.}$

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

  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 $\mathcal{L}\text{,}$ 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.

    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

then we can get rid of the extra “roof” $a\stackrel{f}{\leftarrow }b\stackrel{f}{\to }a\text{,}$ 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.

    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.

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

  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)                                              ∎

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) ( + n)
    H-Level-Zigzag = basic-instance  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)  ⦄
      → (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 ))
        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.

  _++_ : ∀ {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.

  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))

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 $\mathcal{L}:\mathcal{C}\to \mathcal{C}[W^{-1}]$ sends a morphism $f:a\to b$ to the singleton zigzag consisting of $f$ pointing forwards. Finally, if $f\in W\text{,}$ then we’re also allowed to draw it backards; and this inverts $\mathcal{L}f\text{.}$ Since we’re just writing down things we’ve already shown, there’s a bit of code with not much more we could say:

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

  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🔗

  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:\mathcal{C}\to \mathcal{D}$ which inverts $W$, together with the data of the category $\mathcal{D}\text{,}$ gives us exactly what we need to handle each of the constructors:

    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\text{;}$ 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^{-1}:b\to a\text{.}$ The relations need a bit of re-arranging, to deal with associativity, but they are also very pleasant:

    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

    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)

Since Zigzag-univ 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 $\mathcal{L}\tilde{F}\cong F\text{,}$ it’s actually an identity, even if the categories involved are not univalent categories.

    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.

  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 $\mathcal{C}\text{:}$

  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🔗

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 
  Total .Wide-subcat.P-id     = _
  Total .Wide-subcat.P-∘      = _

An important special case of localisation is the total localisation $\mathcal{C}[{\mathcal{C}}^{-1}]\text{,}$ which computes the free groupoid on a category: the universal solution to inverting every morphism in $\mathcal{C}\text{.}$ 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.

  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 by appending onto the empty zigzag.

  _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++ []

  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

Finally, we can show that inverse-appending $f$ onto $f$ gives the identity. With the lemmas proved in the <details> block above, we can conclude that the reverse of a zigzag is actually its categorical inverse in the total localisation $\mathcal{C}[{\mathcal{C}}^{-1}]\text{.}$

    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, we should note the following rephrasing of its universal property: it is the left adjoint to the inclusion of groupoids into categories,¹ which fits into an adjoint triple

with the right adjoint being the core functor — the cofree groupoid on a category.

  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 $\mathcal{C}[W^{-1}]$ into a groupoid $\mathcal{D}\text{.}$ Since any functor $F:\mathcal{C}\to \mathcal{D}$ sends everything to an isomorphism, including the class $W\text{,}$ we’re always allowed to extend $F$ to map from $\mathcal{C}[W^{-1}]\text{,}$ instead.

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 _

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

module _ {o ℓ} {C : Precategory o ℓ} where
  open Precategory C

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

  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)