open import Cat.Instances.Product
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor
import Cat.Reasoning as Cat

module Cat.Diagram.Coend where

private
  variable
    o ℓ o' ℓ' : Level
    C D : Precategory o' ℓ'
  coend-level
    : {C : Precategory o ℓ} {D : Precategory o' ℓ'}
    → Functor (C ^op ×ᶜ C) D
    → Level
  coend-level {o = o} {ℓ} {o'} {ℓ'} _ = o ⊔ o' ⊔ ℓ ⊔ ℓ'

Coends🔗

Let $F:{\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}\to \mathcal{D}$ be a functor, which, by the general yoga of bifunctors we think of as combining a contravariant action $F(-,x):{\mathcal{C}}^{\mathrm{op}}\to \mathcal{D}$ and a covariant action $F(x,-):\mathcal{C}\to \mathcal{D}$ of $\mathcal{C}$ on $\mathcal{D}$¹. As a concrete example, we could take $\mathcal{C}=\mathbf{B}R\text{,}$ the 1-object $\mathbf{Ab}\text{-category}$ associated to a ring $R$ — then the functors $F(-,x)$ and $F(x,-)$ would be left- and right- $R\text{-modules,}$ respectively. In fact, let us focus on this case and consider two modules $A$ and $B\text{,}$ incarnated as a pair of functors $A:\mathbf{B}{R}^{\mathrm{op}}\to \mathbf{Ab}$ and $B:\mathbf{B}R\to \mathbf{Ab}\text{.}$

In this situation, we may study the tensor product (of modules!) $A{\otimes }_{R}B$ as being an “universal object where the actions of $A$ and $B$ agree”. In particular, it’s known that we can compute the tensor product of modules as being (the object in) a coequaliser diagram like

where the undecorated $A\otimes B$ stands for the tensor product of abelian groups, and the two maps are given by the $R\text{-actions}$ of $A$ and $B\text{.}$ More explicitly, letting $a\otimes b$ stand for a tensor, the equation $a\otimes rb=ar\otimes b$ holds in $A{\otimes }_{R}B\text{,}$ and the tensor product is the universal object where this is forced to hold.

Going back to the absurd generality of a bifunctor $F:{\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}\to \mathcal{D}\text{,}$ we may still wish to consider these sorts of “universal quotients where a pair of actions are forced to agree”, even if our codomain category $\mathcal{D}$ does not have a well-behaved calculus of tensor products. As a motivating example, the computation of left Kan extensions as certain colimits has this form!

We call such an object a coend of the functor $F\text{,}$ and denote it by ${\int }^{c}F(c,c)$ (or $\int F$ for short). Being a type of colimit, coends are initial objects in a particular category, but we will unpack the definition here and talk about cowedges instead.

Formalisation🔗

record Cowedge (F : Functor (C ^op ×ᶜ C) D) : Type (coend-level F) where
  no-eta-equality

A cowedge under a functor $F$ is given by an object $w:\mathcal{D}$ (which we refer to as the nadir, because we’re pretentious), together with a family of maps ${\psi }_c:F(c,c)\to w\text{.}$

  private
    module C = Cat C
    module D = Cat D
    module F = Bifunctor F

  field
    nadir : D.Ob
    ψ     : ∀ c → D.Hom (F.₀ (c , c)) nadir

This family of maps must satisfy a condition called extranaturality, expressing that the diagram below commutes. As the name implies, this is like the naturality condition for a natural transformation, but extra! In particular, it copes with the functor being covariant in one argument and contravariant in the other.

    extranatural
      : ∀ {c c'} (f : C.Hom c c')
      → ψ c' D.∘ F.second f ≡ ψ c D.∘ F.first f

A coend, then, is a universal cowedge. In particular, we say that $(w,\psi )$ is a coend for $F$ such that, given any other wedge $(w^{\prime },\psi )$ under $F\text{,}$ we can factor $w$ through $w^{\prime }$ by a unique map $e:w\to w^{\prime }\text{.}$ Furthermore, the map $e$ must commute with the maps $\psi \text{,}$ meaning explicitly that $e{\psi }_a={\psi }_a^{\prime }\text{.}$

record Coend (F : Functor (C ^op ×ᶜ C) D) : Type (coend-level F) where

  private
    module C = Cat C
    module D = Cat D
    module F = Bifunctor F

  field
    cowedge : Cowedge F

  module cowedge = Cowedge cowedge
  open cowedge public
  open Cowedge

Unfolding the requirement of uniqueness for $e\text{,}$ we require that, given any other map $f:w\to w^{\prime }$ s.t. $f{\psi }_a={\psi }_a^{\prime }$ for all objects $a\text{,}$ then $e=f\text{.}$ This is exactly analogous to the uniqueness properties of colimiting maps for every other colimit.

  field
    factor   : ∀ (W : Cowedge F) → D.Hom cowedge.nadir (W .nadir)
    commutes : ∀ {W : Cowedge F} {a} → factor W D.∘ cowedge.ψ a ≡ W .ψ a
    unique
      : ∀ {W : Cowedge F} {g : D.Hom cowedge.nadir (W .nadir)}
      → (∀ {a} → g D.∘ cowedge.ψ a ≡ W .ψ a)
      → g ≡ factor W