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}$1. As a concrete example, we could take $\mathcal{C} = \mathbf{B}R$, the 1-object $\mathbf{Ab}$-category associated to a ring $R$ β then the functors $F(-,x)$ and $F(x,-)$ would be left- and right- $R$-modules, respectively. In fact, let us focus on this case and consider two modules $A$ and $B$, incarnated as a pair of functors $A : \mathbf{B}R^{\mathrm{op}} \to \mathbf{Ab}$ and $B : \mathbf{B}R \to \mathbf{Ab}$.

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

$A \otimes R \otimes B \rightrightarrows A \otimes B \twoheadrightarrow A \otimes_R B\text{,}$

where the undecorated $A \otimes B$ stands for the tensor product of abelian groups, and the two maps are given by the $R$-actions of $A$ and $B$. More explicitly, letting $a \otimes b$ stand for a tensor, the equation $a\otimes rb = ar\otimes b$ holds in $A \otimes_R B$, 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}$, 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$, 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$.

  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',\psi)$ under $F$, we can factor $w$ through $w'$ by a unique map $e : w \to w'$. Furthermore, the map $e$ must commute with the maps $\psi$, meaning explicitly that $e\psi_a = \psi'_a$.

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$, we require that, given any other map $f : w \to w'$ s.t. $f\psi_a = \psi'_a$ for all objects $a$, then $e = f$. 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


1. βActionβ here is meant evoke the idea of e.g.Β group actions, and does not refer to a specific conceptβ©οΈ