open import Cat.Functor.Hom.Representable
open import Cat.Functor.Naturality
open import Cat.Functor.Kan.Base
open import Cat.Functor.Compose
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Reasoning

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 $\mathbf{Hom}$ functors. This rephrasing lets us construct extensions in terms of chains of natural isomorphisms, which can be very handy!

module _
{o β oβ² ββ²}
{C : Precategory o β} {C' : Precategory o β} {D : Precategory oβ² ββ²}
{p : Functor C C'} {F : Functor C D} {G : Functor C' D}
where
private
module C = Cat.Reasoning C
module C' = Cat.Reasoning C'
module D = Cat.Reasoning D
module [C',D] = Cat.Reasoning Cat[ C' , D ]
module [C,D] = Cat.Reasoning Cat[ C , D ]
open Functor
open _=>_
open is-lan
open Corepresentation
open IsoβΏ


Let $p : \mathcal{C} \to \mathcal{C}'$, and $F : \mathcal{C} \to \mathcal{D}$, and $(G, \eta)$ be a candidate for a left extension, as in the following diagram.

Any such pair $(G, \eta)$ induces a natural transformation $D^{C'}(G, -) \to D^{C}(F, - \circ p)$.

  Hom-from-precompose
: 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 $(G, \eta)$ is a left Kan extension of $F$ along $p$.

  representsβis-lan
: (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 $(G, \eta)$ 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.

  is-lanβrepresents
: {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)
where
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 (Nat-path Ξ» _ β D.pushr (sym $lan .Ο-comm Ξ·β _))  module _ {o β oβ² ββ²} {C : Precategory o β} {C' : Precategory o β} {D : Precategory oβ² ββ²} {p : Functor C C'} {F : Functor C D} where private module C = Cat.Reasoning C module C' = Cat.Reasoning C' module D = Cat.Reasoning D module [C',D] = Cat.Reasoning Cat[ C' , D ] module [C,D] = Cat.Reasoning Cat[ C , D ] open Functor open _=>_ open Lan open is-lan open Corepresentation open IsoβΏ   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 (Corep.to has-corep idnt)$
to-is-invertibleβΏ (has-corep .corepresents .to)
(Ξ» M β funext Ξ» Ξ± β
(Corep.from has-corep Ξ± β p) βnt Corep.to has-corep idnt β‘Λβ¨ has-corep .corepresents .from .is-natural _ _ _ $β idnt β©β‘Λ Corep.to has-corep (Corep.from has-corep Ξ± βnt idnt) β‘β¨ ap (Corep.to has-corep) ([C',D].idr _) β©β‘ Corep.to has-corep (Corep.from has-corep Ξ±) β‘β¨ Corep.Ξ΅ has-corep Ξ± β©β‘ Ξ± β) (Ξ» M β funext Ξ» Ξ± β Corep.from has-corep ((Ξ± β p) βnt Corep.to has-corep idnt) β‘β¨ has-corep .corepresents .to .is-natural _ _ _$β _ β©β‘
Ξ± βnt Corep.from has-corep (Corep.to has-corep idnt)       β‘β¨ [C',D].elimr (Corep.Ξ· has-corep idnt) β©β‘
Ξ± β)