open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Monad
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 Monad
open _=>_

Codensity monads🔗

Let $F:\mathcal{A}\to \mathcal{B}$ be a functor with a left adjoint $G:\mathcal{B}\to \mathcal{A}\text{.}$ Some pretty standard abstract nonsense tells us that the composite $GF$ is a monad in $\mathcal{B}\text{,}$ with the unit and multiplication inherited from the adjunction $G⊣F\text{.}$ The easiest cases to picture are when $\mathcal{B}$ is ${\mathbf{Sets}}_{\kappa }\text{,}$ 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\text{,}$ and it exists whenever $\mathcal{B}$ admits limits indexed by categories the size of $\mathcal{A}\text{.}$ 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, ${\mathrm{Ran}}_{F}F\text{.}$

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 ${\mathrm{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\text{),}$ then this extends to a (unique) natural transformation $G\Rightarrow {\mathrm{Ran}}_{F}F\text{.}$

For example, the unit map $\eta$ is obtained by extending the identity natural transformation $\mathrm{id}:\mathrm{Id}F\Rightarrow F\text{,}$ which is implicit witnessing commutativity of the $F$ – $\mathrm{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

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

    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 : Monad B
  Codensity .M = Ext
  Codensity .unit = σ unit-nt
  Codensity .mult = σ mult-nt

  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
        (ext λ x → sym
          ( B.pulll (σ-comm ηₚ x)
          ∙ Ext.cancelr (σ-comm ηₚ x)))
        (ext λ _ → 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
        (ext λ x → sym $
            B.pulll (σ-comm ηₚ x)
          ·· B.pullr (sym (σ unit-nt .is-natural _ _ _))
          ·· B.cancell (σ-comm ηₚ x))
        (ext λ _ → 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'
        (ext λ x → sym $
            B.pulll (σ-comm ηₚ x)
          ∙ Ext.pullr (σ-comm ηₚ x))
        (ext λ 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.