open import Cat.Instances.Functor open import Cat.Instances.Product open import Cat.Instances.Sets 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:
[coequaliser] Data.Set.Coequaliser.html
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 β Ob ] Ξ£[ Y β Ob ] Ξ£[ f β Hom Y X ] β£ Fβ (X , Y) β£ β Ξ£[ X β Ob ] β£ Fβ (X , X) β£ dimapl (X , Y , f , Fxy) = X , (Fβ (id , f) Fxy) dimapr : Ξ£[ X β Ob ] Ξ£[ Y β Ob ] Ξ£[ f β Hom Y X ] β£ Fβ (X , Y) β£ β Ξ£[ X β Ob ] β£ 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
.
coend : Coend F coend .cowedge = universal-cowedge coend .factor W = Coeq-rec hlevel! (Ξ» β«F β W .Ο (β«F .fst) (β«F .snd)) Ξ» where (X , Y , f , Fxy) β happly (W .extranatural f) Fxy coend .commutes = refl coend .unique {W = W} p = funext $ Coeq-elim hlevel! (Ξ» β«F β happly p (β«F .snd)) Ξ» where (X , Y , f , Fxy) β is-setβsquarep (Ξ» _ _ β is-tr (W .nadir)) _ _ _ _
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 squash (Ξ» β«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 = funext $ Coeq-elim (Ξ» _ β hlevel!) (Ξ» _ β refl) (Ξ» _ β is-setβsquarep (Ξ» _ _ β squash) _ _ _ _) Coends .F-β f g = funext $ Coeq-elim (Ξ» _ β hlevel!) (Ξ» _ β refl) (Ξ» _ β is-setβsquarep (Ξ» _ _ β squash) _ _ _ _)