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.