module Cat.Diagram.Coend.Formula {o β o' β'} {C : Precategory o β} {D : Precategory o' β'} where
Computing coendsπ
Using the twisted arrow category as a mediating notion, we show how to compute coends as ordinary colimits. The calculation is actually a bit more straightforward than it might seem at first. The first thing we note is that any functor generates a functor from the twisted arrow category of
This is the fundamental part of our theorem: The twisted arrow category, in a sense, βclassifies cowedgesβ, in that cocones under (the composite above) are the same thing as cowedges from The proof is entirely shuffling some data around, but the commutativity/extranaturality conditions need to be massaged a bit. Check it out, itβs not too long:
module _ (F : Functor (C ^op ΓαΆ C) D) where private module C = Cat C module D = Cat D module F = F-r F open _=>_ open Twist open Bifunctor coconeβcowedge : β {x} β twistα΅α΅ F => Const x β Cowedge F coconeβcowedge eta .nadir = _ coconeβcowedge eta .Ο c = eta .Ξ· ((c , c) , C.id) coconeβcowedge eta .extranatural f = eta .is-natural _ _ (twist _ _ (C.eliml (C.idl _))) β (sym $ eta .is-natural _ _ (twist _ _ (C.cancelr (C.idl _)))) cowedgeβcocone : (W : Cowedge F) β twistα΅α΅ F => Const (W .nadir) cowedgeβcocone W .Ξ· ((c , c') , f) = W .Ο c D.β second F f cowedgeβcocone W .is-natural ((a , b) , f) ((x , y) , g) h = (W .Ο x D.β F.Fβ (C.id , g)) D.β F.Fβ (_ , _) β‘β¨ W .extranatural g D.β©ββ¨refl β©β‘ (W .Ο y D.β F.Fβ (g , C.id)) D.β F.Fβ (h .before , h .after) β‘β¨ D.pullr (F.weave (C.introl refl ,β refl)) β©β‘ W .Ο y D.β ((F.Fβ (h .before C.β g , C.id)) D.β F.Fβ (C.id , h .after)) β‘β¨ D.extendl (sym (W .extranatural _)) β©β‘ (W .Ο a D.β (F.Fβ (C.id , h .before C.β g) D.β F.Fβ (C.id , h .after))) β‘β¨ D.reflβ©ββ¨ sym (Bifunctor.secondβsecond F) β ap (Bifunctor.second F) (h .commutes) β©β‘ W .Ο a D.β F.Fβ (C.id , f) β‘β¨ sym (D.idl _) β©β‘ D.id D.β W .Ο a D.β F.Fβ (C.id , f) β
We can now extend that correspondence to calculating coends as certain colimits: has a coend for if it has a colimit for
colimitβcoend : Colimit (twistα΅α΅ F) β Coend F colimitβcoend colim = coend where open Coend module W = Colimit colim coend : Coend F coend .cowedge = coconeβcowedge W.cocone coend .factor W' = W.universal (cowedgeβcocone W' .Ξ·) (Ξ» f β cowedgeβcocone W' .is-natural _ _ f β D.idl _) coend .commutes {W = W'} = W.factors _ _ β D.elimr (Bifunctor.second-id F) coend .unique {W = W'} comm = W.unique _ _ _ $ Ξ» j β sym $ W' .extranatural _ Β·Β· D.pushl (sym comm) Β·Β· (D.reflβ©ββ¨ (W.commutes (twist _ _ (C.cancelr (C.idl _))))) cocompleteβcoend : is-cocomplete (o β β) β D β Coend F cocompleteβcoend colim = colimitβcoend (colim _) module cocompleteββ« (cocomp : is-cocomplete (o β β) β D) where open Coend (cocompleteβcoend cocomp) public