open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Coend
open import Cat.Prelude

open import Data.Set.Coequaliser

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 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 we can naturally construct its Coend in This ends up assembling into a functor from the functor category into

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!