open import Cat.Diagram.Colimit.Base open import Cat.Instances.Product open import Cat.Instances.Twisted open import Cat.Diagram.Initial open import Cat.Diagram.Coend open import Cat.Prelude import Cat.Functor.Bifunctor as Bifunctor import Cat.Functor.Reasoning as F-r import Cat.Reasoning as Cat 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 coconeβcowedge : Cocone (twistα΅α΅ F) β Cowedge F coconeβcowedge x .nadir = x .coapex coconeβcowedge x .Ο c = x .Ο ((c , c) , C.id) coconeβcowedge x .extranatural f = x .Ο (_ , C.id) D.β Bifunctor.second F f β‘β¨ x .commutes (record { commutes = C.eliml (C.idl C.id) }) β©β‘ x .Ο (_ , f) β‘Λβ¨ x .commutes (record { commutes = C.cancelr (C.idl C.id) }) β©β‘Λ x .Ο (_ , C.id) D.β Bifunctor.first F f β cowedgeβcocone : Cowedge F β Cocone (twistα΅α΅ F) cowedgeβcocone W .coapex = W .nadir cowedgeβcocone W .Ο ((c , cβ²) , f) = W .Ο c D.β Bifunctor.second F f cowedgeβcocone W .commutes {(a , b) , f} {(x , y) , g} h = (W .Ο x D.β Bifunctor.second F g) D.β F.β (_ , _) β‘β¨ W .extranatural g D.β©ββ¨refl β©β‘ (W .Ο y D.β Bifunctor.first F g) D.β F.β (_ , _) β‘β¨ D.pullr (F.weave (Ξ£-pathp (C.introl refl) refl)) β©β‘ W .Ο y D.β Bifunctor.first F (Twist.before h C.β g) D.β Bifunctor.second F (Twist.after h) β‘β¨ D.extendl (sym (W .extranatural _)) β©β‘ W .Ο a D.β Bifunctor.second F (Twist.before h C.β g) D.β Bifunctor.second F (Twist.after h) β‘β¨ D.reflβ©ββ¨ sym (Bifunctor.secondβsecond F) β ap (Bifunctor.second F) (h .Twist.commutes) β©β‘ W .Ο a D.β Bifunctor.second F 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 = Initial colim coend : Coend F coend .Coend.cowedge = coconeβcowedge (colim .Initial.bot) coend .Coend.factor Wβ² = W.Β‘ {x = cowedgeβcocone Wβ²} .hom coend .Coend.commutes = W.Β‘ .commutes _ β D.elimr F.F-id coend .Coend.unique {W = W} {g = g} comm = ap hom β sym $ W.Β‘-unique $ cocone-hom _ Ξ» o β sym $ square (o .snd) where square : β {a b} (f : C.Hom b a) β _ square {a} {b} f = W .Ο a D.β Bifunctor.second F f β‘β¨ W .extranatural f β©β‘ W .Ο b D.β Bifunctor.first F f β‘β¨ D.pushl (sym comm) β©β‘ g D.β W.bot .Ο (_ , C.id) D.β Bifunctor.first F f β‘β¨ D.reflβ©ββ¨ W.bot .commutes (record { before = f ; after = C.id ; commutes = C.cancelr (C.idl _) }) β©β‘ g D.β W.bot .Ο (_ , f) β 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