module Cat.Diagram.Coend.Sets where

# Coends in Setsπ

We can give an explicit construction of coends in the category of sets by
taking a coequaliser.
Intuitively, the coend should be the βsum of the diagonalβ of a functor
$C_{op}ΓCβSets,$
which translates directly to the sigma type
`Ξ£[ X β Ob ] β£ Fβ (X , X) β£`

. However, trying to use this
without some sort of quotient is going to be immediately problematic.
For starters, this isnβt even a set! More importantly, we run into an
immediate issue when we try to prove that this is extranatural; we need
to show that `Fβ (f , id) Fyx β‘ Fβ (id , f) Fyx`

for all
`f : Hom Y X`

and `β£ Fyx : Fβ (X , Y) β£`

.

However, if we take a coequaliser of
`Ξ£[ X β Ob ] β£ Fβ (X , X) β£`

both of these problems
immediately disappear. In particular, we want to take the coequaliser of
the following pair of functions:

This allows us to prove the troublesome extranaturality condition
directly with `glue`

. With that
motivation out of the way, letβs continue with the construction!

module _ {o β} {C : Precategory o β} (F : Functor (C ^op ΓαΆ C) (Sets (o β β))) where open Precategory C open Functor F open Coend open Cowedge

We start by defining the two maps we will coequalise along. Quite a bit of bundling is required to make things well typed, but this is exactly the same pair of maps in the diagram above.

dimapl : Ξ£[ X β C ] Ξ£[ Y β C ] Ξ£[ f β Hom Y X ] F Κ» (X , Y) β Ξ£[ X β C ] F Κ» (X , X) dimapl (X , Y , f , Fxy) = X , Fβ (id , f) Fxy dimapr : Ξ£[ X β C ] Ξ£[ Y β C ] Ξ£[ f β Hom Y X ] F Κ» (X , Y) β Ξ£[ X β C ] F Κ» (X , X) dimapr (X , Y , f , Fxy) = Y , Fβ (f , id) Fxy

Constructing the universal `Cowedge`

is easy now that weβve
taken the right coequaliser.

Set-coend : Coend F Set-coend = coend where universal-cowedge : Cowedge F universal-cowedge .nadir = el! (Coeq dimapl dimapr) universal-cowedge .Ο X Fxx = inc (X , Fxx) universal-cowedge .extranatural {X} {Y} f = funext Ξ» Fyx β glue (Y , X , f , Fyx)

To show that the `Cowedge`

is universal, we can
essentially just project out the bundled up object from the coend and
feed that to the family associated to the cowedge `W`

.

factoring : (W : Cowedge F) β Coeq dimapl dimapr β β W .nadir β factoring W (inc (o , x)) = W .Ο o x factoring W (glue (X , Y , f , Fxy) i) = W .extranatural f i Fxy factoring W (squash x y p q i j) = W .nadir .is-tr (factoring W x) (factoring W y) (Ξ» i β factoring W (p i)) (Ξ» i β factoring W (q i)) i j coend : Coend F coend .cowedge = universal-cowedge coend .factor W = factoring W coend .commutes = refl coend .unique {W = W} p = ext Ξ» X x β p #β x

This construction is actually functorial! Given any functor $C_{op}ΓCβSets,$ we can naturally construct its Coend in $Sets.$ This ends up assembling into a functor from the functor category $[C_{op}ΓC,Sets]$ into $Sets.$

module _ {o β} {π : Precategory o β} where open Precategory π open Functor open _=>_ Coends : Functor Cat[ π ^op ΓαΆ π , Sets (o β β) ] (Sets (o β β)) Coends .Fβ F = el! (Coeq (dimapl F) (dimapr F)) Coends .Fβ Ξ± = Coeq-rec (Ξ» β«F β inc ((β«F .fst) , Ξ± .Ξ· _ (β«F .snd))) Ξ» where (X , Y , f , Fxy) β (ap (Ξ» Ο β inc (X , Ο)) $ happly (Ξ± .is-natural (X , Y) (X , X) (id , f)) Fxy) Β·Β· glue (X , Y , f , Ξ± .Ξ· (X , Y) Fxy) Β·Β· (sym $ ap (Ξ» Ο β inc (Y , Ο)) $ happly (Ξ± .is-natural (X , Y) (Y , Y) (f , id)) Fxy) Coends .F-id = trivial! Coends .F-β f g = trivial!