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 be a functor, which, by the general yoga of bifunctors we think of as combining a contravariant action and a covariant action of on 1. As a concrete example, we could take the 1-object associated to a ring β then the functors and would be left- and right- respectively. In fact, let us focus on this case and consider two modules and incarnated as a pair of functors and

In this situation, we may study the tensor product (of modules!) as being an βuniversal object where the actions of and 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 stands for the tensor product of abelian groups, and the two maps are given by the of and More explicitly, letting stand for a tensor, the equation holds in and the tensor product is the universal object where this is forced to hold.

Going back to the absurd generality of a bifunctor 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 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 and denote it by (or 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 is given by an object (which we refer to as the nadir, because weβre pretentious), together with a family of maps

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

  field
Ο     : β 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 is a coend for such that, given any other wedge under we can factor through by a unique map Furthermore, the map must commute with the maps meaning explicitly that

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 we require that, given any other map s.t. for all objects then 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β©οΈ