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 and a wide subcategory The localisation if it exists, should satisfy the following universal property:

• There is a functor which inverts every morphism in , in the sense that, if then is an isomorphism in and

• If weβre given a category and a functor which also inverts every morphism in (i.e., if then is an isomorphism in then there is a unique functor which satisfies

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 We can picture a general zigzag as follows:

The diagram represents a zigzag from to But pay attention to the orientation of the pink edges: theyβre backwards! This zigzag represents a morphism that did not necessarily exist in composing the inverse of and the inverse of If and 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 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β standing for the composition of 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)

Warning

The localisation of a locally small category at a class 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 was small, then all of its localisations will be, as well.

It follows from uniqueness of isomorphisms that the inclusion of into is also functorial. The calculations are not particularly terrifying, but they are standard, so weβll skip over them for time.
  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) (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.

  _++_ : β {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 sends a morphism to the singleton zigzag consisting of pointing forwards. Finally, if then weβre also allowed to draw it backards; and this inverts 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 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π

  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 which inverts , together with the data of the category 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 Composing backwards uses the proof that sends to an isomorphism, so we have a choice of inverse 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

Finally, a straightforward inductive proof establishes that this procedure preserves composition of zigzags. It preserves the identity definitionally.
    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 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 was already invertible, then we can map from the localisation back to

  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 1
Total .Wide-subcat.P-id     = _
Total .Wide-subcat.P-β      = _


An important special case of localisation is the total localisation which computes the free groupoid on a category: the universal solution to inverting every morphism in 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++ []

We then have a battery of lemmas connecting these two operations with the standard composition, all shown by straightforward induction.
  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 onto 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

    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,1 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 into a groupoid Since any functor sends everything to an isomorphism, including the class weβre always allowed to extend to map from 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)


1. Technically speaking, the inclusion of into is a pseudofunctor, and so this should be a biadjoint cylinder. However, biadjunctions are very complicated objects, so itβs fine β though slightly inaccurate β to work intuitively at the level of 1-categories.β©οΈ