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 $F : C{^{{\mathrm{op}}}}\times C \to D$ generates a functor from the twisted arrow category of $\mathcal{C}{^{{\mathrm{op}}}}$:

${\mathrm{Tw}}(\mathcal{C}{^{{\mathrm{op}}}}){^{{\mathrm{op}}}}{\xrightarrow{\pi_t}} C{^{{\mathrm{op}}}}\times C {\xrightarrow{F}} D$

This is the fundamental part of our theorem: The twisted arrow category, in a sense, βclassifies cowedgesβ, in that cocones under $F\pi_t$ (the composite above) are the same thing as cowedges from $F$. 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: $\mathcal{D}$ has a coend for $F$ if it has a colimit for $F\pi_t$.

  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