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
    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: 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 = 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