open import Cat.Functor.Kan.Right
open import Cat.Instances.Functor
open import Cat.Diagram.Monad
open import Cat.Functor.Base
open import Cat.Prelude

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

module Cat.Diagram.Monad.Codensity where

Codensity monadsπŸ”—

Let F:Aβ†’BF : \mathcal{A} \to \mathcal{B} be a functor with a left adjoint G:Bβ†’AG : \mathcal{B} \to \mathcal{A}. Some pretty standard abstract nonsense tells us that the composite GFGF is a monad in B\mathcal{B}, with the unit and multiplication inherited from the adjunction G⊣FG \dashv F. The easiest cases to picture are when B\mathcal{B} is SetsΞΊ{{\mathbf{Sets}}}_\kappa, and FF 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 FF, and it exists whenever B\mathcal{B} admits limits indexed by categories the size of A\mathcal{A}. When FF 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 FF is the right Kan extension of FF along itself, Ran⁑FF\operatorname{Ran}_F F.

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

For example, the unit map Ξ·\eta is obtained by extending the identity natural transformation id:IdFβ‡’F{{\mathrm{id}}_{}}: {\mathrm{Id}}F {\Rightarrow}F, which is implicit witnessing commutativity of the FF – Id{\mathrm{Id}} – FF 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

(Lan⁑F(F))2Fxβ†’Lan⁑F(F)Fxβ†’Fx, (\operatorname{Lan}_F(F))^2Fx \to \operatorname{Lan}_F(F)Fx \to Fx\text{,}

using the canonical natural transformation Ξ΅:Lan⁑F(F)Fβ‡’F{\varepsilon}: \operatorname{Lan}_F(F)F {\Rightarrow}F. Extending this map, then, gives us a natural transformation (Lan⁑F(F))2β‡’Lan⁑F(F)(\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 : Monad B
  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 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 Kan extensions are for.