module Cat.Functor.Kan.Representable where

Representability of Kan extensionsπŸ”—

Like most constructions with a universal property, we can phrase the definition of Kan extensions in terms of an equivalence of functors. This rephrasing lets us construct extensions in terms of chains of natural isomorphisms, which can be very handy!

Let and and be a candidate for a left extension, as in the following diagram.

Any such pair induces a natural transformation

    : F => G F∘ p
    β†’ Hom-from Cat[ C' , D ] G => Hom-from Cat[ C , D ] F F∘ precompose p
  Hom-from-precompose eta .Ξ· H Ξ± = (Ξ± β—‚ p) ∘nt eta
  Hom-from-precompose eta .is-natural H K Ξ± = funext Ξ» Ξ² β†’ [C,D].pushl β—‚-distribl

If this natural transformation is an isomorphism, then is a left Kan extension of along

    : (eta : F => G F∘ p)
    β†’ is-invertibleⁿ (Hom-from-precompose eta)
    β†’ is-lan p F G eta
  represents→is-lan eta nat-inv = lan where

This may seem somewhat difficult to prove at first glance, but it ends up being an exercise in shuffling data around. We can use the inverse to Hom-from-precompose eta to obtain the universal map of the extension, and factorisation/uniqueness follow directly from the fact that we have a natural isomorphism.

    module nat-inv = is-invertibleⁿ nat-inv

    lan : is-lan p F G eta
    lan .Οƒ {M} Ξ± = nat-inv.inv .Ξ· M Ξ±
    lan .Οƒ-comm {M} {Ξ±} = nat-inv.invl Ξ·β‚š M $β‚š Ξ±
    lan .Οƒ-uniq {M} {Ξ±} {Οƒ'} q = ap (nat-inv.inv .Ξ· M) q βˆ™ nat-inv.invr Ξ·β‚š M $β‚š Οƒ'

Furthermore, if is a left extension, then we can show that Hom-from-precompose eta is a natural isomorphism. The proof is yet another exercise in moving data around.

    : {eta : F => G F∘ p}
    β†’ is-lan p F G eta
    β†’ is-invertibleⁿ (Hom-from-precompose eta)
  is-lan→represents {eta} lan =
    to-is-invertibleⁿ inv
      (Ξ» M β†’ funext Ξ» Ξ± β†’ lan .Οƒ-comm)
      (Ξ» M β†’ funext Ξ» Ξ± β†’ lan .Οƒ-uniq refl)
      inv : Hom-from Cat[ C , D ] F F∘ precompose p => Hom-from Cat[ C' , D ] G
      inv .Ξ· M Ξ± = lan .Οƒ Ξ±
      inv .is-natural M N Ξ± = funext Ξ» Ξ² β†’
        lan .Οƒ-uniq (ext Ξ» _ β†’ D.pushr (sym $ lan .Οƒ-comm Ξ·β‚š _))
  lanβ†’represents : Lan p F β†’ Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p)
  lan→represents lan .corep = lan .Ext
  lan→represents lan .corepresents =
    (is-invertibleⁿ→isoⁿ (is-lanβ†’represents (lan .has-lan))) ni⁻¹

  representsβ†’lan : Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p) β†’ Lan p F
  represents→lan has-corep .Ext = has-corep .corep
  represents→lan has-corep .eta = has-corep .corepresents .from .η _ idnt
  represents→lan has-corep .has-lan =
    represents→is-lan ( has-corep idnt) $
    to-is-invertibleⁿ (has-corep .corepresents .to)
      (Ξ» M β†’ funext Ξ» Ξ± β†’
        (Corep.from has-corep Ξ± β—‚ p) ∘nt has-corep idnt β‰‘Λ˜βŸ¨ has-corep .corepresents .from .is-natural _ _ _ $β‚š idnt βŸ©β‰‘Λ˜ has-corep (Corep.from has-corep Ξ± ∘nt idnt)     β‰‘βŸ¨ ap ( has-corep) ([C',D].idr _) βŸ©β‰‘ has-corep (Corep.from has-corep Ξ±)              β‰‘βŸ¨ Corep.Ξ΅ has-corep Ξ± βŸ©β‰‘
        α ∎)
      (Ξ» M β†’ funext Ξ» Ξ± β†’
        Corep.from has-corep ((Ξ± β—‚ p) ∘nt has-corep idnt) β‰‘βŸ¨ has-corep .corepresents .to .is-natural _ _ _ $β‚š _ βŸ©β‰‘
        Ξ± ∘nt Corep.from has-corep ( has-corep idnt)       β‰‘βŸ¨ [C',D].elimr (Corep.Ξ· has-corep idnt) βŸ©β‰‘
        α ∎)