@ [Anindya](https://forum.azimuthproject.org/discussion/comment/19702/#Comment_19702)

> Michael's diagram suggests that \\( \textrm{Lan}_{G} (H) \circ G = H \\) which turns out to be the case. Is it true for left Kan extensions in general?

I believe the answer, in general, is "No".

Let \\(I\_\mathcal{C}\\) be the identity functor. We have the following:

\[ F \dashv \mathrm{Lan}\_{F}\, I\_\mathcal{C} \tag{A}\]

(see [Bartosz Milewski's notes (2017)](https://bartoszmilewski.com/2017/04/17/kan-extensions/) for more info on this)

In a [Cartesian Closed Category](https://en.wikipedia.org/wiki/Cartesian_closed_category#Definition), we have the following adjunction:

\[ A \times (-) \dashv (-)^A \tag{B} \]

By (A) and (B), we have

\[ \mathrm{Lan}\_{A \times (-)}\, I\_\mathcal{C} \cong (-)^A \]

This is because adjoints are unique up to isomorphism.

The composition \\( (-)^A \circ A \times (-) \\) is a monad. In Haskell, it is commonly referred to as the [State Monad](https://wiki.haskell.org/State_Monad) - you can find details regarding this on [nLab](https://ncatlab.org/nlab/show/function+monad#relation_to_the_writer_comonad_and_state_monad).

While the identity functor is a monad too, it is distinct from the state monad.

So we have:

\[ (\mathrm{Lan}\_{A \times (-)}\, I\_\mathcal{C}) \circ (A \times (-)) \not\cong I_\mathcal{C}\]

This does lead me to another curiosity...

**Puzzle MD1**. If \\(M\\) is a monad and \\(\mathrm{Lan}\_{M}\, I\_\mathcal{C}\\) exists, then is it the case that \\((\mathrm{Lan}\_{M}\, I\_\mathcal{C}) \circ M \cong M\\)?

> Michael's diagram suggests that \\( \textrm{Lan}_{G} (H) \circ G = H \\) which turns out to be the case. Is it true for left Kan extensions in general?

I believe the answer, in general, is "No".

Let \\(I\_\mathcal{C}\\) be the identity functor. We have the following:

\[ F \dashv \mathrm{Lan}\_{F}\, I\_\mathcal{C} \tag{A}\]

(see [Bartosz Milewski's notes (2017)](https://bartoszmilewski.com/2017/04/17/kan-extensions/) for more info on this)

In a [Cartesian Closed Category](https://en.wikipedia.org/wiki/Cartesian_closed_category#Definition), we have the following adjunction:

\[ A \times (-) \dashv (-)^A \tag{B} \]

By (A) and (B), we have

\[ \mathrm{Lan}\_{A \times (-)}\, I\_\mathcal{C} \cong (-)^A \]

This is because adjoints are unique up to isomorphism.

The composition \\( (-)^A \circ A \times (-) \\) is a monad. In Haskell, it is commonly referred to as the [State Monad](https://wiki.haskell.org/State_Monad) - you can find details regarding this on [nLab](https://ncatlab.org/nlab/show/function+monad#relation_to_the_writer_comonad_and_state_monad).

While the identity functor is a monad too, it is distinct from the state monad.

So we have:

\[ (\mathrm{Lan}\_{A \times (-)}\, I\_\mathcal{C}) \circ (A \times (-)) \not\cong I_\mathcal{C}\]

This does lead me to another curiosity...

**Puzzle MD1**. If \\(M\\) is a monad and \\(\mathrm{Lan}\_{M}\, I\_\mathcal{C}\\) exists, then is it the case that \\((\mathrm{Lan}\_{M}\, I\_\mathcal{C}) \circ M \cong M\\)?