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

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 is a left Kan extension of along

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 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 (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 (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 β‘Λ
Corep.to has-corep (Corep.from has-corep Ξ± βnt idnt)
Corep.to has-corep (Corep.from has-corep Ξ±)              β‘
Ξ± β)
(Ξ» M β funext Ξ» Ξ± β
Corep.from has-corep ((Ξ± β p) βnt Corep.to has-corep idnt)
Ξ± βnt Corep.from has-corep (Corep.to has-corep idnt)
Ξ± β)