open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

module Cat.Diagram.Monad.Codensity where

private variable
o β : Level
A B : Precategory o β
open _=>_


Let $F : \mathcal{A} \to \mathcal{B}$ be a functor with a left adjoint $G : \mathcal{B} \to \mathcal{A}$. Some pretty standard abstract nonsense tells us that the composite $GF$ is a monad in $\mathcal{B}$, with the unit and multiplication inherited from the adjunction $G \dashv F$. The easiest cases to picture are when $\mathcal{B}$ is $\mathbf{Sets}_\kappa$, and $F$ is the βunderlying setβ functor from an algebraic category (like monoids or groups). Whatβs slightly more interesting is that functors without left adjoints may also induce monads!

This is called the codensity monad of the functor $F$, and it exists whenever $\mathcal{B}$ admits limits indexed by categories the size of $\mathcal{A}$. When $F$ does have a left adjoint, its codensity monad coincides with the ordinary monad-from-an-adjunction construction. Rather than unfolding the necessary limits here, though, we defer to general categorical machinery: right Kan extensions.

The really, really short of it is that the codensity monad of $F$ is the right Kan extension of $F$ along itself, $\operatorname{Ran}_F F$.

module _ (F : Functor A B) (R : Ran F F) where
open Ran R
private
module A = Cat A
module B = Cat B
module F = Func F


Constructing the monad structure on the $\operatorname{Ran}_F F$ functor is a bit involved, but it does serve as a very illustrative application of the universal property of right Kan extensions. Recall that, by definition, if we have a natural transformation $GF \Rightarrow F$ (for our choice of functor $G$), then this extends to a (unique) natural transformation $G \Rightarrow \operatorname{Ran}_F F$.

For example, the unit map $\eta$ is obtained by extending the identity natural transformation $\operatorname{id}_{} : \operatorname{Id}_{} F \Rightarrow F$, which is implicit witnessing commutativity of the $F$ β $\operatorname{Id}_{}$ β $F$ triangle below.

    unit-nt : Id Fβ F => F
unit-nt .Ξ· x = B.id
unit-nt .is-natural x y f = B.id-comm-sym


For the multiplication map, observe that we can piece together a natural transformation

$(\operatorname{Lan}_F(F))^2Fx \to \operatorname{Lan}_F(F)Fx \to Fx\text{,}$

using the canonical natural transformation $\varepsilon : \operatorname{Lan}_F(F)F \Rightarrow F$. Extending this map, then, gives us a natural transformation $(\operatorname{Lan}_F(F))^2 \Rightarrow \operatorname{Lan}_F(F)$.

    mult-nt : (Ext Fβ Ext) Fβ F => F
mult-nt .Ξ· x = eps .Ξ· x B.β Ext.β (eps .Ξ· x)
mult-nt .is-natural x y f =
(eps .Ξ· y B.β Ext.β (eps .Ξ· y)) B.β Ext.β (Ext.β (F.β f)) β‘β¨ Ext.extendr (eps .is-natural _ _ _) β©β‘
(eps .Ξ· y B.β Ext.Fβ (F.β f)) B.β Ext.β (eps .Ξ· x)        β‘β¨ B.pushl (eps .is-natural _ _ _) β©β‘
F.β f B.β eps .Ξ· x B.β Ext.β (eps .Ξ· x)                   β

Codensity .M = Ext
Codensity .unit = Ο unit-nt
Codensity .mult = Ο mult-nt

Proving that these two extended natural transformations really do comprise a monad structure is a routine application of the uniqueness properties of right Kan extensions. The real noise comes from having to construct auxiliary natural transformations representing each pair of maps we want to compute with.
  Codensity .left-ident {x = x} = path Ξ·β x where
natβ : Ext => Ext
natβ .Ξ· x = Ο mult-nt .Ξ· x B.β Ext.β (Ο unit-nt .Ξ· x)
natβ .is-natural x y f = Ext.extendr (Ο unit-nt .is-natural x y f)
β B.pushl (Ο mult-nt .is-natural _ _ _)

abstract
path : natβ β‘ idnt
path = Ο-uniqβ eps
(Nat-path Ξ» x β
sym (B.pulll (Ο-comm Ξ·β x)
β Ext.cancelr (Ο-comm Ξ·β x)))
(Nat-path Ξ» _ β B.intror refl)

Codensity .right-ident {x = x} = path Ξ·β x where
natβ : Ext => Ext
natβ .Ξ· x = Ο mult-nt .Ξ· x B.β Ο unit-nt .Ξ· (Ext.β x)
natβ .is-natural x y f = B.extendr (Ο unit-nt .is-natural _ _ _)
β B.pushl (Ο mult-nt .is-natural _ _ _)

abstract
path : natβ β‘ idnt
path = Ο-uniqβ eps
(Nat-path Ξ» x β sym \$ B.pulll (Ο-comm Ξ·β x)
β B.pullr (sym (Ο unit-nt .is-natural _ _ _))
β B.cancell (Ο-comm Ξ·β x))
(Nat-path Ξ» _ β B.intror refl)

Codensity .mult-assoc {x = x} = path Ξ·β x where
multβ² : (Ext Fβ Ext Fβ Ext) Fβ F => F
multβ² .Ξ· x = eps .Ξ· x B.β Ext.β (mult-nt .Ξ· x)
multβ² .is-natural x y f = Ext.extendr (mult-nt .is-natural _ _ _)
β B.pushl (eps .is-natural _ _ _)

sigβ : Ext Fβ Ext Fβ Ext => Ext
sigβ .Ξ· x = Ο mult-nt .Ξ· x B.β Ext.β (Ο mult-nt .Ξ· x)
sigβ .is-natural x y f = Ext.extendr (Ο mult-nt .is-natural _ _ _)
β B.pushl (Ο mult-nt .is-natural _ _ _)

sigβ : Ext Fβ Ext Fβ Ext => Ext
sigβ .Ξ· x = Ο mult-nt .Ξ· x B.β Ο mult-nt .Ξ· (Ext.β x)
sigβ .is-natural x y f = B.extendr (Ο mult-nt .is-natural _ _ _)
β B.pushl (Ο mult-nt .is-natural _ _ _)

abstract
path : sigβ β‘ sigβ
path = Ο-uniqβ {M = Ext Fβ Ext Fβ Ext} multβ²
(Nat-path Ξ» x β sym (B.pulll (Ο-comm Ξ·β x)
β Ext.pullr (Ο-comm Ξ·β x)))
(Nat-path Ξ» x β sym (B.pulll (Ο-comm Ξ·β x)
Β·Β· B.pullr (sym (Ο mult-nt .is-natural _ _ _))
Β·Β· B.pulll (Ο-comm Ξ·β x)
β Ext.pullr refl))


To understand what the codensity monad represents, recall that adjoints can be understood as efficient solutions to βoptimisation problemsβ. But when a functor does not admit a left adjoint, we conclude that there is no most efficient solution; This doesnβt mean that we canβt approximate a solution, though! And indeed, this kind of approximation is exactly what right Kan extensions are for.