<p>I think I found a better proof.</p>
<h2>Simplify <span class="math-container">$(\forall a. a \to M\, a) \cong  M\, \mathbb 1$</span></h2>
<p>This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:</p>
<p><em>Yoneda lemma</em>: For any fixed object <span class="math-container">$X$</span> of a category <span class="math-container">$C$</span>, define the hom-functor <span class="math-container">$\textrm{Hom}(X, \_)$</span> as a functor from <span class="math-container">$C$</span> to the category of sets; it maps an object <span class="math-container">$A$</span> to the set <span class="math-container">$\textrm{Hom}(X, A)$</span> of all morphisms between <span class="math-container">$X$</span> and <span class="math-container">$A$</span>. So, <span class="math-container">$\textrm{Hom}(X, \_)$</span> is a set-valued functor. For any other set-valued functor <span class="math-container">$M$</span> from <code>CT</code> to the category of sets, the set of all natural transformations of type <span class="math-container">$\textrm{Hom}(X, \_) \to M$</span> is equivalent to the set <span class="math-container">$M(X)$</span>.</p>
<p>If we use the Yoneda lemma for the category <code>CT</code>, we interpret a covariant type constructor <span class="math-container">$M$</span> as a set-valued functor from <code>CT</code> to the category of sets (since all types are sets). The hom functor for a type <span class="math-container">$X$</span> is the type constructor <span class="math-container">$H\,A = X\to A$</span>. The set of natural transformations  from <span class="math-container">$H$</span> to <span class="math-container">$M$</span> is the type <span class="math-container">$\forall a.\,H\,a\to M\, a$</span> under assumptions of full parametricity.</p>
<p>Then the Yoneda lemma gives the following type equivalence:</p>
<p><span class="math-container">$$ \forall a. (x \to a) \to M\,a \cong M\,x $$</span></p>
<p>To obtain <span class="math-container">$\forall a. a \to M\, a \cong  M\, \mathbb 1$</span>, we use the Yoneda lemma with <span class="math-container">$x = \mathbb 1$</span>.</p>
<p>So, it remains to prove that <span class="math-container">$\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$</span>.</p>
<h1>Use a theorem by Jaskelioff and O'Connor</h1>
<p>The paper <a href="https://arxiv.org/pdf/1402.1699.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1402.1699.pdf</a> proves the following identity:</p>
<p>(Equation 6.1 in section 6)</p>
<p><span class="math-container">$$\forall (M: \mathrm{Monad}). \forall (a, b, x: \mathrm{Type}). (a \to M\, b) \to M\, x \cong \mathrm{Free} \,(R \,a\, b) \,x $$</span></p>
<p>where <span class="math-container">$R \, a \, b$</span> is defined by <span class="math-container">$R \, a \, b \, x = a \times (b \to x)$</span> (it is a covariant endofunctor in <span class="math-container">$x$</span>) and &quot;Free F&quot; is the free monad on a covariant endofunctor <span class="math-container">$F$</span>. The free monad construction is a covariant endofunctor <span class="math-container">$\mathrm{Free}\, F$</span> defined as a recursive type by:</p>
<p><span class="math-container">$$ \mathrm{Free}\, F\, a = a + F\, (\mathrm{Free}\, F\, a) $$</span></p>
<p>or using the <span class="math-container">$\mu$</span> (least fixpoint) notation:</p>
<p><span class="math-container">$$ \mathrm{Free}\, F\, a = \mu \,r.\, (a + F\, r) $$</span></p>
<p>So, we can rewrite the identity as:</p>
<p><span class="math-container">$$\forall (a, b, x: \mathrm{Type}). \forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \mu\,r.\, (x + a \times (b\to r)) $$</span></p>
<p>Now we will substitute some suitable types for <span class="math-container">$a$</span>, <span class="math-container">$b$</span>, <span class="math-container">$x$</span> so that the left-hand side of the identity gives what we want: <span class="math-container">$\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$</span>.</p>
<p>We set <span class="math-container">$a = \mathbb0$</span>, <span class="math-container">$x = \mathbb1$</span> and we find:</p>
<p><span class="math-container">$$ (a \to M\, b) \to M\, x \cong (\mathbb0 \to M\, b) \to M\, \mathbb1 \cong \mathbb1 \to M\, \mathbb1 \cong M\,\mathbb1 $$</span></p>
<p>so:</p>
<p><span class="math-container">$$\forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \forall (M: \mathrm{Monad}). M\, \mathbb1  $$</span></p>
<p>Then we substitute <span class="math-container">$a = \mathbb0$</span>, <span class="math-container">$x = \mathbb1$</span>  into the right-hand side of the identity and get:</p>
<p><span class="math-container">$$ \mu\,r.\, (x + a \times (b\to r)) = \mu\,r.\, (\mathbb1 + \mathbb0 \times (b\to r)) = \mu\,r.\,\mathbb1=\mathbb1 $$</span></p>
<p>This completes the proof.</p>

CC BY-SA 4.0
2024-02-02T10:15:17.450Z
2024-02-02T10:15:17.450Z
winitzki
<p>I have a partial solution. But I got stuck.</p>
<pre><code>//Define a quotient inductive type:
data FreeMonad :  →  where
  Map : (a → b) → FreeMonad a → FreeMonad b
  Pure : a → FreeMonad a
  Join : FreeMonad² a → FreeMonad a
  //Define Bind
  Bind : FreeMonad a → (a → FreeMonad b) → FreeMonad b
  Bind t f = Join (Map f t)

  //Functor laws
  (t : FreeMonad a) ⊦ Map id t = t : FreeMonad a
  (t : FreeMonad a) ⊦ Map (g ∘ f) t = Map g (Map f t) : FreeMonad a

  //Define
  Map² f = Map (Map f)

  //naturality laws
  Map f (Pure x) = Pure (f x) : FreeMonad a
  (t : FreeMonad² a) ⊦ Map f (Join t) = Join (Map² f t) : FreeMonad a

  //Monoid laws
  (t : FreeMonad a) ⊦ Join (Pure t) = t : FreeMonad a
  (t : FreeMonad a) ⊦ Join (Map Pure t) = t : FreeMonad a
  (t : FreeMonad³ a) ⊦ Join (Map Join t) = Join (Join t) : FreeMonad a


//Let's prove that
(t : FreeMonad a) ⊦ Bind t Pure = t : FreeMonad a
                    Join (Map Pure t) = t ✔

//Let's prove that
(x : a) ⊦ Bind (Pure x) f = f x : FreeMonad b
          Join (Map f (Pure x)) = f x
          Join (Pure (f x)) = f x
          f x = f x ✔

//Let's prove that
(t : FreeMonad a) ⊦ (do y ← (do x ← t; f); g) = (do x ← t; y ← f; g) : FreeMonad a
                    Join (Map (y ↦ g) (do x ← t; f)) = Join (Map (x ↦ do y ← f; g) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (x ↦ Join (Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (Join . (x ↦ Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Join (Map² (y ↦ g) (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g) . (x ↦ f)) t
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g)) (Map (x ↦ f) t)
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map² (y ↦ g) (Map (x ↦ f) t) ✔


//FreeMonad satisfies functor laws and monad laws. 

//define
interp : ∀(M : Monad). FreeMonad a → M a 
interp M (Pure x) = pure x
interp M (Map f t) = M f (interp M t)
interp M (Join t) = join (M (interp M) (interp M t))

interp M (Map id t) = interp M t 
M id (interp M t) = interp M t
interp M t = interp M t ✔

interp M (Map (g ∘ f) t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = M g (interp M (Map f t)) 
M (g ∘ f) (interp M t) = M g (M f (interp M t)) 
M g (M f (interp M t)) = M g (M f (interp M t)) ✔ 

interp M (Map f (Pure x)) = interp M (Pure (f x))
M f (interp M (Pure x)) = pure (f x)
M f (pure x) = pure (f x)
pure (f x) = pure (f x) ✔

interp M (Map f (Join t)) = interp M (Join (Map² f t))
M f (join (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
join (M² f (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map² f t))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map (Map f) t))
M² f (M (interp M) (interp M t)) = M (interp M) (M (Map f) (interp M t))
M² f (M (interp M) (interp M t)) = M (interp M . Map f) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f . interp M) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f) (M (interp M) (interp M t))
M² f (M (interp M) (interp M t)) = M² f (M (interp M) (interp M t)) ✔

(t : FreeMonad a) ⊦ interp (Join (Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Pure t))) = interp M t
                    join (M (interp M) (pure t)) = interp M t
                    join (pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad a) ⊦ interp M (Join (Map Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Map Pure t))) = interp M t
                    join (M (interp M) (M Pure (interp M t))) = interp M t
                    join (M (interp M . Pure) (interp M t)) = interp M t
                    join (M pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad³ a) ⊦ interp (Join (Map Join t)) = interp (Join (Join t)) : M a
                     join (M (interp M) (interp M (Map Join t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M) (M Join (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M . Join) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M (join . M (interp M) . interp M) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (join (M (interp M) (interp M t))))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (join (M² (interp M) (M (interp M) (interp M t))))
                     M (M (interp M) . interp M) (interp M t) = M² (interp M) (M (interp M) (interp M t))
                     M (M (interp M) . interp M) (interp M t) = M (M (interp M)) (M (interp M) (interp M t))
                     M (M (interp M)) (M (interp M) (interp M t)) = M (M (interp M)) (M (interp M) (interp M t)) ✔


//Note that interp is automatically a natural transformation (preserves map) and
//a monad morphism (moreover preserves pure and join).

//Let's show that interp is a unique monad morphism 
(M : Monad) (μ : FreeMonad ⇝ M) ⊦ μ = interp M : ∀a. FreeMonad a → M a  
//By function extensionality
(M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) ⊦ μ t = interp M t : M a  
//By induction on t
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ μ (Pure x) = interp M (Pure x)  
  //by definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ μ (Pure x) = pure x
  //by properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ pure x = pure x ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = interp M (Map f t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = Map f (interp M t)
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ M f (μ t) = M f (interp M t)
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ t = interp M t 
  //By induction hypothesis
  ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ μ (Join t) = interp M (Join t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ μ (Join t) = join (M (interp M) (interp M t))
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ join (M μ (μ t)) = join (M (interp M) (interp M t))
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ M μ (μ t) = M (interp M) (interp M t)
  //By induction hypothesis
  ✔

//Hence FreeMonad is the initial object in the category of monads.

//Let's show that FreeMonad and Id are isomorphic objects of the category of monads.

//There is a monad morphism:
pure : ∀a. Id a → FreeMonad a

//interp gives us a morphism in other direction:
interp Id : ∀a. FreeMonad a → Id a

interp Id . pure = pure = id //follows immediately from definition of interp

pure . interp Id = id
//By function extensionality
(t : FreeMonad a) ⊦ pure (interp Id t) = t
//By induction on t
* (x : a) ⊦ pure (interp Id (Pure x)) = Pure x
            pure (pure x) = Pure x
            pure (id x) = Pure x
            pure x = Pure x
            Pure x = Pure x ✔
* (t : FreeMonad a) (f : a → b) ⊦ pure (interp Id (Map f t)) = Map f t
                                  pure (Id f (interp Id t)) = Map f t
                                  //pure is a natural transformation
                                  Map f (pure (interp Id t)) = Map f t
                                  //By induction hypothesis
                                  Map f t = Map f t ✔
* (t : FreeMonad² a) ⊦ Pure (interp Id (Join t)) = Join t
                       Pure (join (Id (interp Id) (interp Id t))) = Join t
                       //pure preserves join
                       Join (pure (Id pure (Id (interp Id) (interp Id t)))) = Join t
                       Join (pure (Id pure (interp Id (interp Id t)))) = Join t
                       Join (interp Id (interp Id t)) = Join t
                       Join (interp Id t) = Join t
                       Join t = Join t ✔

//Hence Id and FreeMonad are isomorphic objects of the monad category.

∀M. ((∀a. a → M a) ≅ )
≅
∀M. ((∀a. Id a → M a) ≅ )
≅
∀M. ((∀a. FreeMonad a → M a) ≅ )
//I am stuck
//We know that the set of monad morphisms (Free ⇝ M) is isomorphic to singleton set but we can't say the same about
//merely functions (∀a. FreeMonad a → M a)

<span class="math-container">```</span>
</code></pre>

CC BY-SA 4.0
2023-10-04T12:11:09.840Z
Your goal seems to be to avoid proving directly (via monad laws) that `Id` is an initial object in the category of monads.  But I don't see how your proof is different. You defined `FreeMonad` and then you need to prove that there is a unique monad morphism from `FreeMonad` to `M`. You showed one such monad morphism. How are you going to prove that it is unique; that any other monad morphism `FreeMonad -> M` is equal to that one? If you have a proof of that, you can just as easily prove that there is a unique monad morphism `Id -> M`.
winitzki
CC BY-SA 4.0
2023-10-04T12:16:10.817Z
One reference about parametricity for type constructors and type classes is this paper http://users.eecs.northwestern.edu/~clk800/rand-test-study/_ftitcc/ftitcc-2009-10-8-12-02-00.pdf  and there is also this tutorial https://www.well-typed.com/blog/2015/08/parametricity-part2/  Although I can't really say that those methods are clearly explained and easy to use. But I am not aware of any other papers or tutorials that explain how to do reasoning with parametricity at the level of type classes ("for all monads m", "For all applicative functor f" etc.).
winitzki
CC BY-SA 4.0
2023-10-04T16:57:45.727Z
Uniqueness follows from the induction principle / universal property of `FreeMonad`. That's the difference between `Id a` and `FreeMonad a`. The latter is an inductive construction, hence we get an induction principle. Uniqueness follows from induction.
Russoul
CC BY-SA 4.0
2023-10-04T17:23:02.440Z
I do not know enough about the theory that proves how your `FreeMonad` code is actually constructing an initial object. Your `FreeMonad` is not the same as the usual free monad construction (which takes an arbitrary given functor `F` and wraps it into some structure in order to obtain a free monad on `F`). Could you give a reference? Also, it's not clear to me how you prove that `pure . interp = id`. (The other direction is easy, `interp . pure = id`.)
winitzki
CC BY-SA 4.0
2023-10-04T17:32:58.583Z
I updated my "answer" to include induction and uniqueness principle of `FreeMonad`. I have a critical hole in my reasoning though. For some reason I assumed that the quotient type I defined makes every function `FreeMonad a -> M a` an actual monad morphism. But that's not true. Hence indeed I can't prove uniqueness of `interp`... My idea was parallel to that of quotient types: every function out of a quotient type is actually a setoid homomorhism (it automatically preserves equations of the quotient type).
Russoul
CC BY-SA 4.0
2023-10-04T17:33:52.680Z
I somehow wishfully thought that my construction would similarly make every function `FreeMonad a -> M a` a monad morphism... I wonder if something like that is possible in type theory...
Russoul
CC BY-SA 4.0
2023-10-04T17:38:08.863Z
Regarding `pure . interp = id`, I'd use function extensionality to get:
`(x : FreeMonad a) |- pure (interp x) = x` and prove this by induction on `x`
Russoul
CC BY-SA 4.0
2023-10-04T17:41:42.737Z
Actually, wait, I can't show that `interp` is a unique function `FreeMonad a -> M a`. But I might still be able to show that it's a unique monad morphism...
Russoul
CC BY-SA 4.0
2023-10-04T17:47:23.953Z
You only need to show that there is a unique monad morphism, not a unique arbitrary function.
winitzki
CC BY-SA 4.0
2023-10-04T19:41:45.973Z
I find `pure (interp x) = Pure(interp x)` but `x` is not necessarily of the form `Pure (...)`, as `x` could be a `Bind (...)`. So I don't see how to show that `pure (interp x) = x`.
winitzki
CC BY-SA 4.0
2023-10-05T14:13:53.180Z
I updated my answer with a proof of `pure . interp = id`. 
I'll try to compile a full proof of the target equation again this weekend.
Russoul
CC BY-SA 4.0
2023-10-05T18:07:54.407Z
I do not understand the definition of `FreeMonad`. How are `a` and `b` quantified? Please write explicitly for every variable appearing what it ranges over and where it's introduced (and how it's quantified). Furthermore, in order to have a monad there has to be an underlying functor. What is it?
Andrej Bauer
CC BY-SA 4.0
2023-10-06T09:06:52.203Z
@AndrejBauer The whole point of this `FreeMonad` is to have no underlying functor. It's perhaps a slight abuse of terminology to call this a `FreeMonad`. Equivalently it is a free monad on a void functor (F a = Void). Such a free monad is equivalent to the identity monad.
winitzki
CC BY-SA 4.0
2023-10-07T08:49:04.480Z
Slight abuse? If you want to be understood, you should change both the notation and the title. Or at the very least put up a very, very big warning that you're abusing accepted terminology.
Andrej Bauer
CC BY-SA 4.0
2023-10-07T09:10:26.323Z
Abusing terminology wasn’t my intention. I just lack proper knowledge to formulate my question in accepted terms. I thought every initial or terminal object is a free object. Or alternatively, that an inductive type like that one generates a monad “freely” without any extra knowledge. I guess I got that wrong. Anyway, I’ll write out my answer over this weekend.
Russoul
CC BY-SA 4.0
2023-10-08T08:01:29.453Z
I know of two uses of "monad", in category theory and in functional programming, both of which presume an underlying functor. Indeed, it is beginning to look like your question is misleading because of strange terminology.
Andrej Bauer
CC BY-SA 4.0
2023-10-08T09:06:59.063Z
@AndrejBauer I would say that the formulation `(∀(M : Monad). ∀a. a → M a) ≅ ` is perfectly ordinary from the programming language perspective. It is a direct translation from Haskell code. The proof, however, must reformulate that into the language of categories.
winitzki
CC BY-SA 4.0
2023-10-08T10:32:26.277Z
I am not saying the answer is all wrong, on the contrary, very likely parametricity can be used to prove so something of the kind. The problem is that both the question and the answer are of the "fast & loose" reasoning seen in Haskell community – and that's not math. So far we have neither a well-posed question nor a well-posed answer. The best way to get there is to stop avoiding obvious direct questions. Let me ask again: **What is `Monad`?**
Andrej Bauer
CC BY-SA 4.0
2023-10-11T16:41:03.933Z
As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).
Community
CC BY-SA 4.0
2023-10-15T11:02:09.257Z
I rewrote my answer.
Russoul
CC BY-SA 4.0
2023-10-15T14:58:09.333Z
I got stuck at the end. I managed to show that FreeMonad is isomorphic to Id as monad objects in the category of monads though.
Russoul
CC BY-SA 4.0
2023-10-03T11:49:53.990Z
2023-10-15T14:57:13.090Z
2023-10-15T14:57:13.090Z
Russoul
<h1>This proof is most likely incorrect and is left here only for reference!</h1>
<p>Here is a derivation of <span class="math-container">$\forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1$</span>  based on parametricity.</p>
<h2>Preliminaries</h2>
<p>The type <span class="math-container">$\forall (M:\textrm{Monad}). \forall a. a \to M\, a$</span> is a type of functions with type parameters <span class="math-container">$M$</span> and <span class="math-container">$a$</span>. In addition, there is a typeclass constraint on the type parameter <span class="math-container">$M$</span>: the type constructor <span class="math-container">$M$</span> must be a monad.</p>
<p>We require that the code of those functions must be purely functional and &quot;fully parametric&quot;: the type parameters <span class="math-container">$M$</span> and <span class="math-container">$a$</span> are used as opaque unknown arbitrary types about which no information may be used. (For example, the code may not try to discover the actual types of <span class="math-container">$a$</span> and <span class="math-container">$M$</span> using run-time type reflection that some programming languages support. We should imagine that all code is written purely in System F<span class="math-container">$\omega$</span> or something similar.) This means the code may use only the monad <span class="math-container">$M$</span>'s methods, without using any other information about the type <span class="math-container">$M$</span>. (There is no information at all about the type parameter <span class="math-container">$a$</span>.)</p>
<p>The assumptions of &quot;full parametricity&quot; about the code allow us to use the parametricity theorems. One consequence of the parametricity theorems is that any fully parametric code with type signature <span class="math-container">$\forall x.\, F\, x \to G\,x$</span> (where <span class="math-container">$F$</span> and <span class="math-container">$G$</span> are covariant type constructors) will automatically satisfy the law of a natural transformation. The natural transformation is between functors <span class="math-container">$F$</span> and <span class="math-container">$G$</span> that will arise when we translate that code into the language of category theory.</p>
<p>We will use two categories here:</p>
<ol>
<li><p>The category of types: objects are all System F<span class="math-container">$\omega$</span>'s ground types (i.e. types of kind <span class="math-container">$*$</span>) and morphisms are all functions implementable as terms in System F<span class="math-container">$\omega$</span>. We will denote this category by <code>CT</code>.</p>
</li>
<li><p>The category of endofunctors in the category of types. Endofunctors correspond to type constructors in the programming language (types of kind <span class="math-container">$*\to*$</span>). We will denote this category by <code>Endo(CT)</code>.</p>
</li>
</ol>
<p>So, the programming language notation <span class="math-container">$\forall a.\, F\, a \to G\,a$</span> under assumptions of full parametricity means the type of natural transformations between <span class="math-container">$F$</span> and <span class="math-container">$G$</span> where <span class="math-container">$F$</span> and <span class="math-container">$G$</span> are endofunctors in <code>CT</code>.</p>
<p>Similarly, the programming language notation <span class="math-container">$\forall (M:\textrm{Monad}). F\,M \to G\,M$</span> means the type of natural transformations between some functors <span class="math-container">$F$</span>, <span class="math-container">$G$</span>. For our usage, those functors will be between <code>Endo(CT)</code> and <code>CT</code>.</p>
<p>Finally, the programming language will have to implement all types as sets (actually, as countable sets because the byte size of any value in memory must be finite). So, the category of types <code>CT</code> is in some way embedded into the category of sets.</p>
<h2>Simplify <span class="math-container">$(\forall a. a \to M\, a) \cong  M\, \mathbb 1$</span></h2>
<p>This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:</p>
<p><em>Yoneda lemma</em>: For any fixed object <span class="math-container">$X$</span> of a category <span class="math-container">$C$</span>, define the hom-functor <span class="math-container">$\textrm{Hom}(X, \_)$</span> as a functor from <span class="math-container">$C$</span> to the category of sets; it maps an object <span class="math-container">$A$</span> to the set <span class="math-container">$\textrm{Hom}(X, A)$</span> of all morphisms between <span class="math-container">$X$</span> and <span class="math-container">$A$</span>. So, <span class="math-container">$\textrm{Hom}(X, \_)$</span> is a set-valued functor. For any other set-valued functor <span class="math-container">$M$</span> from <code>CT</code> to the category of sets, the set of all natural transformations of type <span class="math-container">$\textrm{Hom}(X, \_) \to M$</span> is equivalent to the set <span class="math-container">$M(X)$</span>.</p>
<p>If we use the Yoneda lemma for the category <code>CT</code>, we interpret a covariant type constructor <span class="math-container">$M$</span> as a set-valued functor from <code>CT</code> to the category of sets (since all types are sets). The hom functor for a type <span class="math-container">$X$</span> is the type constructor <span class="math-container">$H\,A = X\to A$</span>. The set of natural transformations  from <span class="math-container">$H$</span> to <span class="math-container">$M$</span> is the type <span class="math-container">$\forall a.\,H\,a\to M\, a$</span> under assumptions of full parametricity.</p>
<p>Then the Yoneda lemma gives the following type equivalence:</p>
<p><span class="math-container">$$ \forall a. (x \to a) \to M\,a \cong M\,x $$</span></p>
<p>To obtain <span class="math-container">$\forall a. a \to M\, a \cong  M\, \mathbb 1$</span>, we use the Yoneda lemma with <span class="math-container">$x = \mathbb 1$</span>.</p>
<p>So, it remains to prove that <span class="math-container">$\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$</span>.</p>
<h2>From monads to pointed endofunctors</h2>
<p>It is easier to prove a stronger statement: instead of the <code>Monad</code> typeclass, we require only a <code>Pointed</code> typeclass. An endofunctor <span class="math-container">$F$</span> is pointed if there exists a natural transformation of type <span class="math-container">$\textrm{Id} \to F$</span>. In a programming language, this means there exists a value of type <span class="math-container">$\forall a. a\to F\,a$</span>. This is equivalent to a value of type <span class="math-container">$F \, \mathbb 1$</span>. There are no laws required for this value.</p>
<p>So, the requirement of having a pointed endofunctor (<span class="math-container">$F:\textrm{Pointed}$</span>) is the same as assuming an existing value of type <span class="math-container">$F\,\mathbb 1$</span>.</p>
<p>Then we will obtain the statement</p>
<p><span class="math-container">$$ \forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1 $$</span></p>
<p>as a consequence of a stronger statement:</p>
<p><span class="math-container">$$ \forall (F:\textrm{Pointed}).\, F\, \mathbb 1 \cong \mathbb 1$$</span></p>
<p>or equivalently:</p>
<p><span class="math-container">$$ \forall (F:\textrm{Functor}). F\,\mathbb1\to F\,\mathbb1\cong\mathbb1$$</span></p>
<p>Now we have a simpler problem that can be solved by Yoneda lemma in the category <code>Endo(CT)</code>.</p>
<h2>The meaning of <span class="math-container">$\forall (F:\textrm{Functor})$</span></h2>
<p>In order to use the Yoneda lemma, we need to formulate the last statement more clearly in terms of category theory.</p>
<p>In the programming language notation, a function of type <span class="math-container">$\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$</span> is simply a function that is parameterized by a type constructor <span class="math-container">$F$</span> that is assumed to have a law-abiding <code>fmap</code> method (i.e., a covariant type constructor). Also, it is assumed that any function of type <span class="math-container">$\forall (F:\textrm{Functor}). (...)$</span> does not use any information about <span class="math-container">$F$</span> other than its <code>fmap</code> method.</p>
<p>The parametricity theorem says that such functions will satisfy a naturality law with respect to the type parameter <span class="math-container">$F$</span>. This corresponds in the language of category theory to a natural transformation between functors from <code>Endo(CT)</code> to <code>CT</code>.</p>
<p>So, the programming language notation <span class="math-container">$\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$</span>  means the type of natural transformations <span class="math-container">$S\, F\to S\, F$</span> where we defined a functor <span class="math-container">$S$</span>:<code>Endo(CT)</code><span class="math-container">$\to$</span><code>CT</code> by <span class="math-container">$S\,F = F\,\mathbb 1$</span>.</p>
<h2>Shortcut for the proof</h2>
<p>A shortcut is the following identity: for fixed types <span class="math-container">$b$</span> and <span class="math-container">$c$</span>:</p>
<p><span class="math-container">$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$</span></p>
<p>The paper <a href="https://arxiv.org/abs/1402.1699" rel="nofollow noreferrer">https://arxiv.org/abs/1402.1699</a> has a more general result that also covers what we need:</p>
<p><span class="math-container">$$ \forall (F:\textrm{Functor}). (a\to F\,b)\to F\,c \cong a\times(b\to c)$$</span></p>
<p>Setting <span class="math-container">$a=b=c=\mathbb1$</span>, we obtain <span class="math-container">$\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1) \cong\mathbb1 \to\mathbb1 \cong \mathbb1$</span>.</p>
<h2>Yoneda lemma for endofunctors</h2>
<p>Let's look at the identity:</p>
<p><span class="math-container">$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$</span></p>
<p>We can prove this using Yoneda lemma twice.</p>
<p>First, we want to reformulate this from the programming language notation into the category theory language. We want to rewrite the type of functions shown above as a type of some natural transformations like this:</p>
<p><span class="math-container">$$ \forall F. P\,F \to Q\,F $$</span></p>
<p>In the language of category theory, this is the set <span class="math-container">$P \to Q$</span> of natural transformations between functors <span class="math-container">$P$</span>, <span class="math-container">$Q$</span>.</p>
<p>Between which functors <span class="math-container">$P$</span>, <span class="math-container">$Q$</span> will those natural transformations work? In our case, we must have <span class="math-container">$P\,F = F\,b$</span> and <span class="math-container">$Q\,F = F\,c$</span>. Clearly <span class="math-container">$P$</span> maps <span class="math-container">$F$</span> to a type from <code>CT</code>. So, we need to work with <span class="math-container">$P$</span>, <span class="math-container">$Q$</span> that are functors from <code>Endo(CT)</code> to <code>CT</code>.</p>
<p>If we want to use the Yoneda lemma, we need a natural transformation between a hom-functor and some other functor. So, <span class="math-container">$P$</span> must be a hom-functor (but right now our <span class="math-container">$P$</span> is not of that form). The type <span class="math-container">$ \forall F. P\,F \to Q\,F $</span> must be of the form that Yoneda lemma requires, which looks like this:</p>
<p><span class="math-container">$$  \forall F.\, \textrm{Hom}(X, F) \to Q\,F  \cong Q\,X$$</span></p>
<p>Here <span class="math-container">$\textrm{Hom}(X, F)$</span> is the set of all morphisms between <span class="math-container">$X$</span> and <span class="math-container">$F$</span> in the category <code>Endo(CT)</code>. Those morphisms are natural transformations between <span class="math-container">$X$</span> and <span class="math-container">$F$</span>.</p>
<p>In the category theory notation, the Yoneda lemma in the category <code>Endo(CT)</code> is:</p>
<p><span class="math-container">$$ \textrm{Hom}(X, \_) \to Q \cong Q\,X$$</span></p>
<p>Here we interpret <span class="math-container">$Q$</span> as a set-valued functor from <code>Endo(CT)</code> to the category of sets.</p>
<p>How can we rewrite <span class="math-container">$P\,F$</span> as <span class="math-container">$\textrm{Hom}(X, F)$</span>? What is the endofunctor <span class="math-container">$X$</span> from <code>Endo(CT)</code> that fits here? To figure that out, write the types in the programming language notation:</p>
<p><span class="math-container">$$ P\,F = F\,b \quad \textrm{but}\quad \textrm{Hom}(X, F) = \forall a.\,X\,a\to F\,a $$</span></p>
<p>We need to find <span class="math-container">$X$</span> such that <span class="math-container">$\forall a.\,X\,a\to F\,a \cong F\,b$</span>.</p>
<p>We use the Yoneda lemma for the category <code>CT</code> to find:</p>
<p><span class="math-container">$$\forall a.\,(b\to a)\to F\,a \cong F\,b$$</span></p>
<p>So, a suitable <span class="math-container">$X$</span> is the functor defined by the code <span class="math-container">$X\,a = b \to a$</span>, or in the category theory notation, <span class="math-container">$X = \textrm{Hom}(b,\_)$</span>.</p>
<p>With this <span class="math-container">$X$</span>, we obtain <span class="math-container">$Q\,X =X\,c=\textrm{Hom}(b,c)$</span>. In the programming language notation, this is just the type <span class="math-container">$b\to c$</span>.</p>
<p>So, we have proved that the type of natural transformations <span class="math-container">$P\to Q$</span> is equivalent to the set <span class="math-container">$\textrm{Hom}(b,c)$</span> or, in the programming language notation, to the type <span class="math-container">$b\to c$</span>.</p>

CC BY-SA 4.0
2023-10-07T08:51:09.247Z
Please specify the category on which you're using the Yoneda lemma, explain what universal quantification over "functors" is supposed to be, etc.
Andrej Bauer
CC BY-SA 4.0
2023-10-07T19:38:00.943Z
@AndrejBauer I updated my answer.
winitzki
CC BY-SA 4.0
2023-10-08T08:04:46.763Z
In "Preliminaries" you state that $M$ is a type parameter, but by the end of the paragraph you call it a "monad". Which is it? And if $M$ is indeed a type parameter, then why "$M : \mathrm{Monad}$"? Is $\mathrm{Monad}$ a synonym for $\mathrm{Type}$?
Andrej Bauer
CC BY-SA 4.0
2023-10-08T08:07:35.787Z
In the category `CT`, do you mean only closed terms to be morphisms, and only closed types to be objects? What does it mean for two terms to be equal, precisely (whatever the answer, you must check that composition is associative)?
Andrej Bauer
CC BY-SA 4.0
2023-10-08T15:08:06.873Z
@AndrejBauer I edited the answer to clarify the "Monad" $M$.  As for the category `CT`, I do not know how to define everything completely rigorously down to axioms and first principles. I think both types and terms must be closed. But I don't know how to define equality and how to prove associativity. This probably needs some model and not just definitions about terms of System F$\omega$. This is a basic assumption underlying all reasoning in functional programming. Can you suggest papers or books where the category similar to `CT` is defined completely rigorously?
winitzki
CC BY-SA 4.0
2023-10-08T19:04:18.653Z
Unfortunately, all I can suggest is [a rant](https://math.andrej.com/2016/08/06/hask-is-not-a-category/). Honestly, I think a more promising direction would be to use all the category-theoretic stuff as inspiration, but to stick to just relational parametricity in the proof, and carry it out purely in the relevant calculus (something like $F^\omega$).
Andrej Bauer
CC BY-SA 4.0
2023-10-08T19:09:07.000Z
But then the trouble is, what sort of parametricity result do we need to handle quantification over all type constructors. I am not an expert on this particular topic, so I don't know if anyone's proved parametricity results for $F^\omega$ (where the argument could be carried out). The only work I am aware of that seems to be related is [On monadic parametricity of second-order functionals](https://www2.in.tum.de/bib/files/Bauer13Parametricity.pdf), but I think it doesn't quite cover enough ground to include this question.
Andrej Bauer
CC BY-SA 4.0
2023-10-09T08:40:19.327Z
@AndrejBauer I will try to do what you say but 1) I thought your "rant" was only about Haskell, with its `seq` etc. But I don't mean to work in Haskell, I want to work in a typed lambda-calculus of some sort. Do you also think that nobody has really constructed a rigorous category like `CT` for any kind of typed lambda-calculus like System F or System F$\omega$? 2) There is a paper http://users.eecs.northwestern.edu/~clk800/rand-test-study/_ftitcc/ftitcc-2009-10-8-12-02-00.pdf about parametricity for type classes. Do you think it's not rigorous? What about https://arxiv.org/abs/1402.1699 ?
winitzki
CC BY-SA 4.0
2023-10-09T09:41:08.813Z
The word "category" appears exactly once in Voigtländer's paper (according to my PDF viewer), and that's in combination with "hoops". So, no categories in that paper.
Andrej Bauer
CC BY-SA 4.0
2023-10-09T09:42:54.070Z
Jaskelioff and O’Connor's paper has plenty of categories, but it does **not** construct a syntactic category, as far as I can see. It uses more traditional semantic techniques, which are based on *interpreting* the calculi in suitable categories (that themselves are not specifically constructed as syntactic models). So, no categories made out of $F_\omega$ there either.
Andrej Bauer
CC BY-SA 4.0
2023-10-09T09:45:10.273Z
Rather than repeating myself in the comments here, it's probably better to just point to https://mathstodon.xyz/@andrejbauer/110773943434654514. If anyone knows of a precisely constructed "category $F_\omega$" or some such, I'd like to know about it.
Andrej Bauer
CC BY-SA 4.0
2023-10-09T09:47:44.100Z
Would it be acceptable to just replace "syntactic category"  by a "semantic category" in my answer?
winitzki
CC BY-SA 4.0
2023-10-09T10:47:37.047Z
You mean something in the style of the Jaskelioff and O’Connor's paper? Sure, I think that might work rather well (and is probably easier than finding a suitable parametricity statement).
Andrej Bauer
CC BY-SA 4.0
2023-10-09T12:26:27.923Z
Actually I think there is a crucial error in all my attempts to prove this. The error seems to be that from `∀
M: Pointed. something` it does not actually follow that `∀
M: Monad. something`. It could be that there is some combination of `M`'s `pure` and `bind` that creates a nontrivial value of type  . We need to prove that there can't be such a combination.
winitzki
CC BY-SA 4.0
2024-03-03T20:39:18.853Z
Here is a paper from ICFP 2010 that contains parametricity results for F_omega and all PTS
Max New
CC BY-SA 4.0
2024-03-04T10:06:14.653Z
@MaxNew Could you give a link to that paper please?
winitzki
CC BY-SA 4.0
2024-03-04T14:58:06.770Z
Sorry here it is: https://dl.acm.org/doi/10.1145/1863543.1863592 . And I'll point out that there's been tons of work in the intervening years on dependent type theories and external and internal parametricity.
Max New
CC BY-SA 4.0
2023-10-07T08:25:29.033Z
2024-03-03T16:01:47.103Z
2024-03-03T16:01:47.103Z
winitzki
<p>Just like the title says, how to prove that equation? The equation basically says that there is only one function <code>a -&gt; M a</code> parametric in both <code>M</code> and <code>a</code>. I am not very familiar with proofs involving parametricity. Only simple ones, like proving that there is only one parametric identity function. Or that church booleans are equivalent to inductively defined booleans. There is one catch though. We can't prove it using initiality of Id in the category of monads, because I want to prove initiality via the sought equation.</p>
<p><em><strong>Edit:</strong></em>
A more vigorous formulation of the goal statement I want to prove:</p>
<pre><code>//Fix the category of types and functions — Type

//Functor is an endofunctor on Type

//Given a functor F and a type a
//we write
F a : 
//to represent the functorial action of F on object a.

//Given a functor F and a function f : a → b
//we write
F f : F a → F b
//to represent the functorial action of F on morhism f.

//Notation:
M⁰ a = a
M¹⁺ⁿ a = M (Mⁿ a)

//Monad is a Functor M with additional two functions:
pure : ∀a. a → M a
join : ∀a. M² a → M a
//which satisfy the following laws:
(x : a) ⊦ M f (pure x) = pure (f x)            } naturality laws
(t : M² a) ⊦ M f (join t) = join (M² f t)      }

(t : M a) ⊦ join (pure t) = t                  }
(t : M a) ⊦ join (M pure t) = t                } monoid laws
(t : M³ a) ⊦ join (M join t) = join (join t)   }

//Define a category of Monads:
//Objects are monads
//Arrows are functions f : ∀a. M a → N a
//that additionally have the following properties:
(x : a) ⊦ f (pure x) = pure x : N a
(t : M² a) ⊦ f (join t) = join (f (M f t) : N² a) : N a
(α : a → b) (t : M a) ⊦ f (M α t) = N α (f t) : N b

//Isomorphism between types A and B is a pair of both-way functions between A and B that compose to identity in both ways.

//The goal is to prove:
(∀(M : Monad). ∀a. a → M a) ≅ 
//In english: the space of functions that for arbitrary monad M, arbitrary type a take an element of a to an element of M a is
//isomorphic to one element space ().

<span class="math-container">```</span>
</code></pre>

CC BY-SA 4.0
2023-10-07T08:52:29.637Z
Please provide a context in which this question makes sense. The statement in the title looks like something that one migth write in a polymorphic calculus of some sort, but you did not say which one. You should also define what `Monad` stands for, *precisely*, and what notion of isomorphism you are using.
Andrej Bauer
CC BY-SA 4.0
2023-10-15T10:47:08.580Z
You can assume that the statement is formulated against a constructive extensional dependent type theory with quotient types and an open universe. If we ever need to be more concrete, we can fix a theory.
Russoul
CC BY-SA 4.0
2023-10-15T10:54:45.230Z
Updated the question to reflect the statement more rigorously
Russoul
<type-theory><parametricity>
How to prove `(∀(M : Monad). ∀a. a → M a) ≅ `
Russoul
# How to prove `(∀(M : Monad). ∀a. a → M a) ≅ `

(Asked by: username_0 on 2023-10-03)

Just like the title says, how to prove that equation? The equation basically says that there is only one function a -> M a parametric in both M and a. I am not very familiar with proofs involving parametricity. Only simple ones, like proving that there is only one parametric identity function. Or that church booleans are equivalent to inductively defined booleans. There is one catch though. We can't prove it using initiality of Id in the category of monads, because I want to prove initiality via the sought equation.
Edit:
A more vigorous formulation of the goal statement I want to prove:
//Fix the category of types and functions — Type

//Functor is an endofunctor on Type

//Given a functor F and a type a
//we write
F a : 
//to represent the functorial action of F on object a.

//Given a functor F and a function f : a → b
//we write
F f : F a → F b
//to represent the functorial action of F on morhism f.

//Notation:
M⁰ a = a
M¹⁺ⁿ a = M (Mⁿ a)

//Monad is a Functor M with additional two functions:
pure : ∀a. a → M a
join : ∀a. M² a → M a
//which satisfy the following laws:
(x : a) ⊦ M f (pure x) = pure (f x)            } naturality laws
(t : M² a) ⊦ M f (join t) = join (M² f t)      }

(t : M a) ⊦ join (pure t) = t                  }
(t : M a) ⊦ join (M pure t) = t                } monoid laws
(t : M³ a) ⊦ join (M join t) = join (join t)   }

//Define a category of Monads:
//Objects are monads
//Arrows are functions f : ∀a. M a → N a
//that additionally have the following properties:
(x : a) ⊦ f (pure x) = pure x : N a
(t : M² a) ⊦ f (join t) = join (f (M f t) : N² a) : N a
(α : a → b) (t : M a) ⊦ f (M α t) = N α (f t) : N b

//Isomorphism between types A and B is a pair of both-way functions between A and B that compose to identity in both ways.

//The goal is to prove:
(∀(M : Monad). ∀a. a → M a) ≅ 
//In english: the space of functions that for arbitrary monad M, arbitrary type a take an element of a to an element of M a is
//isomorphic to one element space ().

```

**Tags:** type-theory, parametricity
> **Comments:**
> **username_1**: Please provide a context in which this question makes sense. The statement in the title looks like something that one migth write in a polymorphic calculus of some sort, but you did not say which one. You should also define what `Monad` stands for, *precisely*, and what notion of isomorphism you are using.  
> **username_0**: You can assume that the statement is formulated against a constructive extensional dependent type theory with quotient types and an open universe. If we ever need to be more concrete, we can fix a theory.  
> **username_0**: Updated the question to reflect the statement more rigorously  

---

## 3 answers

### Answer by username_2 on 2024-02-02. Score: 1

I think I found a better proof.

## Simplify $(\forall a. a \to M\, a) \cong M\, \mathbb 1$

This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:

*Yoneda lemma*: For any fixed object $X$ of a category $C$, define the hom-functor $\textrm{Hom}(X, \\_)$ as a functor from $C$ to the category of sets; it maps an object $A$ to the set $\textrm{Hom}(X, A)$ of all morphisms between $X$ and $A$. So, $\textrm{Hom}(X, \\_)$ is a set-valued functor. For any other set-valued functor $M$ from `CT` to the category of sets, the set of all natural transformations of type $\textrm{Hom}(X, \\_) \to M$ is equivalent to the set $M(X)$.

If we use the Yoneda lemma for the category `CT`, we interpret a covariant type constructor $M$ as a set-valued functor from `CT` to the category of sets (since all types are sets). The hom functor for a type $X$ is the type constructor $H\,A = X\to A$. The set of natural transformations from $H$ to $M$ is the type $\forall a.\,H\,a\to M\, a$ under assumptions of full parametricity.

Then the Yoneda lemma gives the following type equivalence:

$$ \forall a. (x \to a) \to M\,a \cong M\,x $$

To obtain $\forall a. a \to M\, a \cong M\, \mathbb 1$, we use the Yoneda lemma with $x = \mathbb 1$.

So, it remains to prove that $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

# Use a theorem by Jaskelioff and O'Connor

The paper <https://arxiv.org/pdf/1402.1699.pdf> proves the following identity:

(Equation 6.1 in section 6)

$$\forall (M: \mathrm{Monad}). \forall (a, b, x: \mathrm{Type}). (a \to M\, b) \to M\, x \cong \mathrm{Free} \,(R \,a\, b) \,x $$

where $R \, a \, b$ is defined by $R \, a \, b \, x = a \times (b \to x)$ (it is a covariant endofunctor in $x$) and "Free F" is the free monad on a covariant endofunctor $F$. The free monad construction is a covariant endofunctor $\mathrm{Free}\, F$ defined as a recursive type by:

$$ \mathrm{Free}\, F\, a = a + F\, (\mathrm{Free}\, F\, a) $$

or using the $\mu$ (least fixpoint) notation:

$$ \mathrm{Free}\, F\, a = \mu \,r.\, (a + F\, r) $$

So, we can rewrite the identity as:

$$\forall (a, b, x: \mathrm{Type}). \forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \mu\,r.\, (x + a \times (b\to r)) $$

Now we will substitute some suitable types for $a$, $b$, $x$ so that the left-hand side of the identity gives what we want: $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

We set $a = \mathbb0$, $x = \mathbb1$ and we find:

$$ (a \to M\, b) \to M\, x \cong (\mathbb0 \to M\, b) \to M\, \mathbb1 \cong \mathbb1 \to M\, \mathbb1 \cong M\,\mathbb1 $$

so:

$$\forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \forall (M: \mathrm{Monad}). M\, \mathbb1 $$

Then we substitute $a = \mathbb0$, $x = \mathbb1$ into the right-hand side of the identity and get:

$$ \mu\,r.\, (x + a \times (b\to r)) = \mu\,r.\, (\mathbb1 + \mathbb0 \times (b\to r)) = \mu\,r.\,\mathbb1=\mathbb1 $$

This completes the proof.


---

### Answer by username_0 on 2023-10-03. Score: 0

I have a partial solution. But I got stuck.
//Define a quotient inductive type:
data FreeMonad :  →  where
  Map : (a → b) → FreeMonad a → FreeMonad b
  Pure : a → FreeMonad a
  Join : FreeMonad² a → FreeMonad a
  //Define Bind
  Bind : FreeMonad a → (a → FreeMonad b) → FreeMonad b
  Bind t f = Join (Map f t)

  //Functor laws
  (t : FreeMonad a) ⊦ Map id t = t : FreeMonad a
  (t : FreeMonad a) ⊦ Map (g ∘ f) t = Map g (Map f t) : FreeMonad a

  //Define
  Map² f = Map (Map f)

  //naturality laws
  Map f (Pure x) = Pure (f x) : FreeMonad a
  (t : FreeMonad² a) ⊦ Map f (Join t) = Join (Map² f t) : FreeMonad a

  //Monoid laws
  (t : FreeMonad a) ⊦ Join (Pure t) = t : FreeMonad a
  (t : FreeMonad a) ⊦ Join (Map Pure t) = t : FreeMonad a
  (t : FreeMonad³ a) ⊦ Join (Map Join t) = Join (Join t) : FreeMonad a


//Let's prove that
(t : FreeMonad a) ⊦ Bind t Pure = t : FreeMonad a
                    Join (Map Pure t) = t ✔

//Let's prove that
(x : a) ⊦ Bind (Pure x) f = f x : FreeMonad b
          Join (Map f (Pure x)) = f x
          Join (Pure (f x)) = f x
          f x = f x ✔

//Let's prove that
(t : FreeMonad a) ⊦ (do y ← (do x ← t; f); g) = (do x ← t; y ← f; g) : FreeMonad a
                    Join (Map (y ↦ g) (do x ← t; f)) = Join (Map (x ↦ do y ← f; g) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (x ↦ Join (Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (Join . (x ↦ Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Join (Map² (y ↦ g) (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g) . (x ↦ f)) t
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g)) (Map (x ↦ f) t)
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map² (y ↦ g) (Map (x ↦ f) t) ✔


//FreeMonad satisfies functor laws and monad laws. 

//define
interp : ∀(M : Monad). FreeMonad a → M a 
interp M (Pure x) = pure x
interp M (Map f t) = M f (interp M t)
interp M (Join t) = join (M (interp M) (interp M t))

interp M (Map id t) = interp M t 
M id (interp M t) = interp M t
interp M t = interp M t ✔

interp M (Map (g ∘ f) t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = M g (interp M (Map f t)) 
M (g ∘ f) (interp M t) = M g (M f (interp M t)) 
M g (M f (interp M t)) = M g (M f (interp M t)) ✔ 

interp M (Map f (Pure x)) = interp M (Pure (f x))
M f (interp M (Pure x)) = pure (f x)
M f (pure x) = pure (f x)
pure (f x) = pure (f x) ✔

interp M (Map f (Join t)) = interp M (Join (Map² f t))
M f (join (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
join (M² f (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map² f t))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map (Map f) t))
M² f (M (interp M) (interp M t)) = M (interp M) (M (Map f) (interp M t))
M² f (M (interp M) (interp M t)) = M (interp M . Map f) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f . interp M) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f) (M (interp M) (interp M t))
M² f (M (interp M) (interp M t)) = M² f (M (interp M) (interp M t)) ✔

(t : FreeMonad a) ⊦ interp (Join (Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Pure t))) = interp M t
                    join (M (interp M) (pure t)) = interp M t
                    join (pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad a) ⊦ interp M (Join (Map Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Map Pure t))) = interp M t
                    join (M (interp M) (M Pure (interp M t))) = interp M t
                    join (M (interp M . Pure) (interp M t)) = interp M t
                    join (M pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad³ a) ⊦ interp (Join (Map Join t)) = interp (Join (Join t)) : M a
                     join (M (interp M) (interp M (Map Join t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M) (M Join (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M . Join) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M (join . M (interp M) . interp M) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (join (M (interp M) (interp M t))))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (join (M² (interp M) (M (interp M) (interp M t))))
                     M (M (interp M) . interp M) (interp M t) = M² (interp M) (M (interp M) (interp M t))
                     M (M (interp M) . interp M) (interp M t) = M (M (interp M)) (M (interp M) (interp M t))
                     M (M (interp M)) (M (interp M) (interp M t)) = M (M (interp M)) (M (interp M) (interp M t)) ✔


//Note that interp is automatically a natural transformation (preserves map) and
//a monad morphism (moreover preserves pure and join).

//Let's show that interp is a unique monad morphism 
(M : Monad) (μ : FreeMonad ⇝ M) ⊦ μ = interp M : ∀a. FreeMonad a → M a  
//By function extensionality
(M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) ⊦ μ t = interp M t : M a  
//By induction on t
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ μ (Pure x) = interp M (Pure x)  
  //by definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ μ (Pure x) = pure x
  //by properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (x : a) ⊦ pure x = pure x ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = interp M (Map f t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = Map f (interp M t)
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ M f (μ t) = M f (interp M t)
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad a) (f : a → b) ⊦ μ t = interp M t 
  //By induction hypothesis
  ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ μ (Join t) = interp M (Join t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ μ (Join t) = join (M (interp M) (interp M t))
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ join (M μ (μ t)) = join (M (interp M) (interp M t))
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : ) (t : FreeMonad² a) ⊦ M μ (μ t) = M (interp M) (interp M t)
  //By induction hypothesis
  ✔

//Hence FreeMonad is the initial object in the category of monads.

//Let's show that FreeMonad and Id are isomorphic objects of the category of monads.

//There is a monad morphism:
pure : ∀a. Id a → FreeMonad a

//interp gives us a morphism in other direction:
interp Id : ∀a. FreeMonad a → Id a

interp Id . pure = pure = id //follows immediately from definition of interp

pure . interp Id = id
//By function extensionality
(t : FreeMonad a) ⊦ pure (interp Id t) = t
//By induction on t
* (x : a) ⊦ pure (interp Id (Pure x)) = Pure x
            pure (pure x) = Pure x
            pure (id x) = Pure x
            pure x = Pure x
            Pure x = Pure x ✔
* (t : FreeMonad a) (f : a → b) ⊦ pure (interp Id (Map f t)) = Map f t
                                  pure (Id f (interp Id t)) = Map f t
                                  //pure is a natural transformation
                                  Map f (pure (interp Id t)) = Map f t
                                  //By induction hypothesis
                                  Map f t = Map f t ✔
* (t : FreeMonad² a) ⊦ Pure (interp Id (Join t)) = Join t
                       Pure (join (Id (interp Id) (interp Id t))) = Join t
                       //pure preserves join
                       Join (pure (Id pure (Id (interp Id) (interp Id t)))) = Join t
                       Join (pure (Id pure (interp Id (interp Id t)))) = Join t
                       Join (interp Id (interp Id t)) = Join t
                       Join (interp Id t) = Join t
                       Join t = Join t ✔

//Hence Id and FreeMonad are isomorphic objects of the monad category.

∀M. ((∀a. a → M a) ≅ )
≅
∀M. ((∀a. Id a → M a) ≅ )
≅
∀M. ((∀a. FreeMonad a → M a) ≅ )
//I am stuck
//We know that the set of monad morphisms (Free ⇝ M) is isomorphic to singleton set but we can't say the same about
//merely functions (∀a. FreeMonad a → M a)

```

> **Comments:**
> **username_2**: Your goal seems to be to avoid proving directly (via monad laws) that `Id` is an initial object in the category of monads.  But I don't see how your proof is different. You defined `FreeMonad` and then you need to prove that there is a unique monad morphism from `FreeMonad` to `M`. You showed one such monad morphism. How are you going to prove that it is unique; that any other monad morphism `FreeMonad -> M` is equal to that one? If you have a proof of that, you can just as easily prove that there is a unique monad morphism `Id -> M`.  
> **username_2**: One reference about parametricity for type constructors and type classes is this paper http://users.eecs.northwestern.edu/~clk800/rand-test-study/_ftitcc/ftitcc-2009-10-8-12-02-00.pdf  and there is also this tutorial https://www.well-typed.com/blog/2015/08/parametricity-part2/  Although I can't really say that those methods are clearly explained and easy to use. But I am not aware of any other papers or tutorials that explain how to do reasoning with parametricity at the level of type classes ("for all monads m", "For all applicative functor f" etc.).  
> **username_0**: Uniqueness follows from the induction principle / universal property of `FreeMonad`. That's the difference between `Id a` and `FreeMonad a`. The latter is an inductive construction, hence we get an induction principle. Uniqueness follows from induction.  
> **username_2**: I do not know enough about the theory that proves how your `FreeMonad` code is actually constructing an initial object. Your `FreeMonad` is not the same as the usual free monad construction (which takes an arbitrary given functor `F` and wraps it into some structure in order to obtain a free monad on `F`). Could you give a reference? Also, it's not clear to me how you prove that `pure . interp = id`. (The other direction is easy, `interp . pure = id`.)  
> **username_0**: I updated my "answer" to include induction and uniqueness principle of `FreeMonad`. I have a critical hole in my reasoning though. For some reason I assumed that the quotient type I defined makes every function `FreeMonad a -> M a` an actual monad morphism. But that's not true. Hence indeed I can't prove uniqueness of `interp`... My idea was parallel to that of quotient types: every function out of a quotient type is actually a setoid homomorhism (it automatically preserves equations of the quotient type).  
> **username_0**: I somehow wishfully thought that my construction would similarly make every function `FreeMonad a -> M a` a monad morphism... I wonder if something like that is possible in type theory...  
> **username_0**: Regarding `pure . interp = id`, I'd use function extensionality to get: `(x : FreeMonad a) |- pure (interp x) = x` and prove this by induction on `x`  
> **username_0**: Actually, wait, I can't show that `interp` is a unique function `FreeMonad a -> M a`. But I might still be able to show that it's a unique monad morphism...  
> **username_2**: You only need to show that there is a unique monad morphism, not a unique arbitrary function.  
> **username_2**: I find `pure (interp x) = Pure(interp x)` but `x` is not necessarily of the form `Pure (...)`, as `x` could be a `Bind (...)`. So I don't see how to show that `pure (interp x) = x`.  
> **username_0**: I updated my answer with a proof of `pure . interp = id`.  I'll try to compile a full proof of the target equation again this weekend.  
> **username_1**: I do not understand the definition of `FreeMonad`. How are `a` and `b` quantified? Please write explicitly for every variable appearing what it ranges over and where it's introduced (and how it's quantified). Furthermore, in order to have a monad there has to be an underlying functor. What is it?  
> **username_2**: @AndrejBauer The whole point of this `FreeMonad` is to have no underlying functor. It's perhaps a slight abuse of terminology to call this a `FreeMonad`. Equivalently it is a free monad on a void functor (F a = Void). Such a free monad is equivalent to the identity monad.  
> **username_1**: Slight abuse? If you want to be understood, you should change both the notation and the title. Or at the very least put up a very, very big warning that you're abusing accepted terminology.  
> **username_0**: Abusing terminology wasn’t my intention. I just lack proper knowledge to formulate my question in accepted terms. I thought every initial or terminal object is a free object. Or alternatively, that an inductive type like that one generates a monad “freely” without any extra knowledge. I guess I got that wrong. Anyway, I’ll write out my answer over this weekend.  
> **username_1**: I know of two uses of "monad", in category theory and in functional programming, both of which presume an underlying functor. Indeed, it is beginning to look like your question is misleading because of strange terminology.  
> **username_2**: @AndrejBauer I would say that the formulation `(∀(M : Monad). ∀a. a → M a) ≅ ` is perfectly ordinary from the programming language perspective. It is a direct translation from Haskell code. The proof, however, must reformulate that into the language of categories.  
> **username_1**: I am not saying the answer is all wrong, on the contrary, very likely parametricity can be used to prove so something of the kind. The problem is that both the question and the answer are of the "fast & loose" reasoning seen in Haskell community – and that's not math. So far we have neither a well-posed question nor a well-posed answer. The best way to get there is to stop avoiding obvious direct questions. Let me ask again: **What is `Monad`?**  
> **username_3**: As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).  
> **username_0**: I rewrote my answer.  
> **username_0**: I got stuck at the end. I managed to show that FreeMonad is isomorphic to Id as monad objects in the category of monads though.  

---

### Answer by username_2 on 2023-10-07. Score: -1

# This proof is most likely incorrect and is left here only for reference!

Here is a derivation of $\forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1$ based on parametricity.

## Preliminaries

The type $\forall (M:\textrm{Monad}). \forall a. a \to M\, a$ is a type of functions with type parameters $M$ and $a$. In addition, there is a typeclass constraint on the type parameter $M$: the type constructor $M$ must be a monad.

We require that the code of those functions must be purely functional and "fully parametric": the type parameters $M$ and $a$ are used as opaque unknown arbitrary types about which no information may be used. (For example, the code may not try to discover the actual types of $a$ and $M$ using run-time type reflection that some programming languages support. We should imagine that all code is written purely in System F$\omega$ or something similar.) This means the code may use only the monad $M$'s methods, without using any other information about the type $M$. (There is no information at all about the type parameter $a$.)

The assumptions of "full parametricity" about the code allow us to use the parametricity theorems. One consequence of the parametricity theorems is that any fully parametric code with type signature $\forall x.\, F\, x \to G\,x$ (where $F$ and $G$ are covariant type constructors) will automatically satisfy the law of a natural transformation. The natural transformation is between functors $F$ and $G$ that will arise when we translate that code into the language of category theory.

We will use two categories here:

1. The category of types: objects are all System F$\omega$'s ground types (i.e. types of kind $\*$) and morphisms are all functions implementable as terms in System F$\omega$. We will denote this category by `CT`.
2. The category of endofunctors in the category of types. Endofunctors correspond to type constructors in the programming language (types of kind $\*\to\*$). We will denote this category by `Endo(CT)`.

So, the programming language notation $\forall a.\, F\, a \to G\,a$ under assumptions of full parametricity means the type of natural transformations between $F$ and $G$ where $F$ and $G$ are endofunctors in `CT`.

Similarly, the programming language notation $\forall (M:\textrm{Monad}). F\,M \to G\,M$ means the type of natural transformations between some functors $F$, $G$. For our usage, those functors will be between `Endo(CT)` and `CT`.

Finally, the programming language will have to implement all types as sets (actually, as countable sets because the byte size of any value in memory must be finite). So, the category of types `CT` is in some way embedded into the category of sets.

## Simplify $(\forall a. a \to M\, a) \cong M\, \mathbb 1$

This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:

*Yoneda lemma*: For any fixed object $X$ of a category $C$, define the hom-functor $\textrm{Hom}(X, \\_)$ as a functor from $C$ to the category of sets; it maps an object $A$ to the set $\textrm{Hom}(X, A)$ of all morphisms between $X$ and $A$. So, $\textrm{Hom}(X, \\_)$ is a set-valued functor. For any other set-valued functor $M$ from `CT` to the category of sets, the set of all natural transformations of type $\textrm{Hom}(X, \\_) \to M$ is equivalent to the set $M(X)$.

If we use the Yoneda lemma for the category `CT`, we interpret a covariant type constructor $M$ as a set-valued functor from `CT` to the category of sets (since all types are sets). The hom functor for a type $X$ is the type constructor $H\,A = X\to A$. The set of natural transformations from $H$ to $M$ is the type $\forall a.\,H\,a\to M\, a$ under assumptions of full parametricity.

Then the Yoneda lemma gives the following type equivalence:

$$ \forall a. (x \to a) \to M\,a \cong M\,x $$

To obtain $\forall a. a \to M\, a \cong M\, \mathbb 1$, we use the Yoneda lemma with $x = \mathbb 1$.

So, it remains to prove that $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

## From monads to pointed endofunctors

It is easier to prove a stronger statement: instead of the `Monad` typeclass, we require only a `Pointed` typeclass. An endofunctor $F$ is pointed if there exists a natural transformation of type $\textrm{Id} \to F$. In a programming language, this means there exists a value of type $\forall a. a\to F\,a$. This is equivalent to a value of type $F \, \mathbb 1$. There are no laws required for this value.

So, the requirement of having a pointed endofunctor ($F:\textrm{Pointed}$) is the same as assuming an existing value of type $F\,\mathbb 1$.

Then we will obtain the statement

$$ \forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1 $$

as a consequence of a stronger statement:

$$ \forall (F:\textrm{Pointed}).\, F\, \mathbb 1 \cong \mathbb 1$$

or equivalently:

$$ \forall (F:\textrm{Functor}). F\,\mathbb1\to F\,\mathbb1\cong\mathbb1$$

Now we have a simpler problem that can be solved by Yoneda lemma in the category `Endo(CT)`.

## The meaning of $\forall (F:\textrm{Functor})$

In order to use the Yoneda lemma, we need to formulate the last statement more clearly in terms of category theory.

In the programming language notation, a function of type $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$ is simply a function that is parameterized by a type constructor $F$ that is assumed to have a law-abiding `fmap` method (i.e., a covariant type constructor). Also, it is assumed that any function of type $\forall (F:\textrm{Functor}). (...)$ does not use any information about $F$ other than its `fmap` method.

The parametricity theorem says that such functions will satisfy a naturality law with respect to the type parameter $F$. This corresponds in the language of category theory to a natural transformation between functors from `Endo(CT)` to `CT`.

So, the programming language notation $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$ means the type of natural transformations $S\, F\to S\, F$ where we defined a functor $S$:`Endo(CT)`$\to$`CT` by $S\,F = F\,\mathbb 1$.

## Shortcut for the proof

A shortcut is the following identity: for fixed types $b$ and $c$:

$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$

The paper <https://arxiv.org/abs/1402.1699> has a more general result that also covers what we need:

$$ \forall (F:\textrm{Functor}). (a\to F\,b)\to F\,c \cong a\times(b\to c)$$

Setting $a=b=c=\mathbb1$, we obtain $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1) \cong\mathbb1 \to\mathbb1 \cong \mathbb1$.

## Yoneda lemma for endofunctors

Let's look at the identity:

$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$

We can prove this using Yoneda lemma twice.

First, we want to reformulate this from the programming language notation into the category theory language. We want to rewrite the type of functions shown above as a type of some natural transformations like this:

$$ \forall F. P\,F \to Q\,F $$

In the language of category theory, this is the set $P \to Q$ of natural transformations between functors $P$, $Q$.

Between which functors $P$, $Q$ will those natural transformations work? In our case, we must have $P\,F = F\,b$ and $Q\,F = F\,c$. Clearly $P$ maps $F$ to a type from `CT`. So, we need to work with $P$, $Q$ that are functors from `Endo(CT)` to `CT`.

If we want to use the Yoneda lemma, we need a natural transformation between a hom-functor and some other functor. So, $P$ must be a hom-functor (but right now our $P$ is not of that form). The type $ \forall F. P\,F \to Q\,F $ must be of the form that Yoneda lemma requires, which looks like this:

$$ \forall F.\, \textrm{Hom}(X, F) \to Q\,F \cong Q\,X$$

Here $\textrm{Hom}(X, F)$ is the set of all morphisms between $X$ and $F$ in the category `Endo(CT)`. Those morphisms are natural transformations between $X$ and $F$.

In the category theory notation, the Yoneda lemma in the category `Endo(CT)` is:

$$ \textrm{Hom}(X, \\_) \to Q \cong Q\,X$$

Here we interpret $Q$ as a set-valued functor from `Endo(CT)` to the category of sets.

How can we rewrite $P\,F$ as $\textrm{Hom}(X, F)$? What is the endofunctor $X$ from `Endo(CT)` that fits here? To figure that out, write the types in the programming language notation:

$$ P\,F = F\,b \quad \textrm{but}\quad \textrm{Hom}(X, F) = \forall a.\,X\,a\to F\,a $$

We need to find $X$ such that $\forall a.\,X\,a\to F\,a \cong F\,b$.

We use the Yoneda lemma for the category `CT` to find:

$$\forall a.\,(b\to a)\to F\,a \cong F\,b$$

So, a suitable $X$ is the functor defined by the code $X\,a = b \to a$, or in the category theory notation, $X = \textrm{Hom}(b,\\_)$.

With this $X$, we obtain $Q\,X =X\,c=\textrm{Hom}(b,c)$. In the programming language notation, this is just the type $b\to c$.

So, we have proved that the type of natural transformations $P\to Q$ is equivalent to the set $\textrm{Hom}(b,c)$ or, in the programming language notation, to the type $b\to c$.

> **Comments:**
> **username_1**: Please specify the category on which you're using the Yoneda lemma, explain what universal quantification over "functors" is supposed to be, etc.  
> **username_2**: @AndrejBauer I updated my answer.  
> **username_1**: In "Preliminaries" you state that $M$ is a type parameter, but by the end of the paragraph you call it a "monad". Which is it? And if $M$ is indeed a type parameter, then why "$M : \mathrm{Monad}$"? Is $\mathrm{Monad}$ a synonym for $\mathrm{Type}$?  
> **username_1**: In the category `CT`, do you mean only closed terms to be morphisms, and only closed types to be objects? What does it mean for two terms to be equal, precisely (whatever the answer, you must check that composition is associative)?  
> **username_2**: @AndrejBauer I edited the answer to clarify the "Monad" $M$.  As for the category `CT`, I do not know how to define everything completely rigorously down to axioms and first principles. I think both types and terms must be closed. But I don't know how to define equality and how to prove associativity. This probably needs some model and not just definitions about terms of System F$\omega$. This is a basic assumption underlying all reasoning in functional programming. Can you suggest papers or books where the category similar to `CT` is defined completely rigorously?  
> **username_1**: Unfortunately, all I can suggest is [a rant](https://math.andrej.com/2016/08/06/hask-is-not-a-category/). Honestly, I think a more promising direction would be to use all the category-theoretic stuff as inspiration, but to stick to just relational parametricity in the proof, and carry it out purely in the relevant calculus (something like $F^\omega$).  
> **username_1**: But then the trouble is, what sort of parametricity result do we need to handle quantification over all type constructors. I am not an expert on this particular topic, so I don't know if anyone's proved parametricity results for $F^\omega$ (where the argument could be carried out). The only work I am aware of that seems to be related is [On monadic parametricity of second-order functionals](https://www2.in.tum.de/bib/files/Bauer13Parametricity.pdf), but I think it doesn't quite cover enough ground to include this question.  
> **username_2**: @AndrejBauer I will try to do what you say but 1) I thought your "rant" was only about Haskell, with its `seq` etc. But I don't mean to work in Haskell, I want to work in a typed lambda-calculus of some sort. Do you also think that nobody has really constructed a rigorous category like `CT` for any kind of typed lambda-calculus like System F or System F$\omega$? 2) There is a paper http://users.eecs.northwestern.edu/~clk800/rand-test-study/_ftitcc/ftitcc-2009-10-8-12-02-00.pdf about parametricity for type classes. Do you think it's not rigorous? What about https://arxiv.org/abs/1402.1699 ?  
> **username_1**: The word "category" appears exactly once in Voigtländer's paper (according to my PDF viewer), and that's in combination with "hoops". So, no categories in that paper.  
> **username_1**: Jaskelioff and O’Connor's paper has plenty of categories, but it does **not** construct a syntactic category, as far as I can see. It uses more traditional semantic techniques, which are based on *interpreting* the calculi in suitable categories (that themselves are not specifically constructed as syntactic models). So, no categories made out of $F_\omega$ there either.  
> **username_1**: Rather than repeating myself in the comments here, it's probably better to just point to https://mathstodon.xyz/@andrejbauer/110773943434654514. If anyone knows of a precisely constructed "category $F_\omega$" or some such, I'd like to know about it.  
> **username_2**: Would it be acceptable to just replace "syntactic category"  by a "semantic category" in my answer?  
> **username_1**: You mean something in the style of the Jaskelioff and O’Connor's paper? Sure, I think that might work rather well (and is probably easier than finding a suitable parametricity statement).  
> **username_2**: Actually I think there is a crucial error in all my attempts to prove this. The error seems to be that from `∀ M: Pointed. something` it does not actually follow that `∀ M: Monad. something`. It could be that there is some combination of `M`'s `pure` and `bind` that creates a nontrivial value of type  . We need to prove that there can't be such a combination.  
> **username_4**: Here is a paper from ICFP 2010 that contains parametricity results for F_omega and all PTS  
> **username_2**: @MaxNew Could you give a link to that paper please?  
> **username_4**: Sorry here it is: https://dl.acm.org/doi/10.1145/1863543.1863592 . And I'll point out that there's been tons of work in the intervening years on dependent type theories and external and internal parametricity.  

---

