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

Tw(Cop)op→πtCop×C→FD {\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Ο€tF\pi_t (the composite above) are the same thing as cowedges from FF. 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: D\mathcal{D} has a coend for FF if it has a colimit for FΟ€tF\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