module Cat.Diagram.Coend.Formula
  {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}

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
    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) ,
  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₁ ( , g)) D.∘ F.F₁ (_ , _)                           β‰‘βŸ¨ W .extranatural g D.⟩∘⟨refl βŸ©β‰‘
    (W .ψ y D.∘ F.F₁ (g , D.∘ F.F₁ (h .before , h .after)            β‰‘βŸ¨ D.pullr (F.weave (C.introl refl ,β‚š refl)) βŸ©β‰‘
    W .ψ y D.∘ ((F.F₁ (h .before C.∘ g , D.∘ F.F₁ ( , h .after)) β‰‘βŸ¨ D.extendl (sym (W .extranatural _)) βŸ©β‰‘
    (W .ψ a D.∘ (F.F₁ ( , h .before C.∘ g) D.∘ F.F₁ ( , h .after))) β‰‘βŸ¨ D.refl⟩∘⟨ sym (Bifunctor.second∘second F) βˆ™ ap (Bifunctor.second F) (h .commutes) βŸ©β‰‘
    W .ψ a D.∘ F.F₁ ( , f)                                              β‰‘βŸ¨ sym (D.idl _) βŸ©β‰‘ D.∘ W .ψ a D.∘ F.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 = Colimit colim
    coend : Coend F
    coend .cowedge = cocone→cowedge W.cocone
    coend .factor W' =
        (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