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

open Cowedge


# 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 .Ο 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