The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that "a monad transformer is equivalent to its base monad". A monad transformer probably carries more information than its base monad, because there is no known way of mechanically converting a given base monad into its monad transformer.
By definition, a transformer's base monad can be obtained by applying the transformer to Id. This is denoted by F Id. You claim that F Id ≅ ∀ (m: Monad). F m. This seems to be correct.
Also you are correct that a proof will involve parametricity at the level of monads.
A possible proof could go like this. Consider the category of monads: objects are monads and arrows are monad morphisms. In that category, a monad transformer is an endofunctor. (This is true for almost all monad transformers, except Continuation and Codensity and some other variants of those monads. See https://stackoverflow.com/questions/63882053/whats-a-functor-on-the-category-of-monads?rq=3 and see also my answers in Explaining monad transformers in categorical terms and in https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io .)
Then we want to prove the following property:
F Id ≅ ∀ (m: Monad). F m
where ∀ (m: Monad) goes over all monads.
The first step is to prove that the identity monad Id is an initial object in the category of monads. For any given monad M, there is only one monad morphism between Id and M (that morphism is given by the monad M's unit method, unit: ∀ a. Id a → M a). I omit the proof of this property.
The second step is to use the Yoneda lemma (still in the category of monads). The Yoneda lemma says: For any Set-valued functor G (that is, a functor from the category of monads to the category of sets), the Yoneda lemma says:
G X ≅ Nat(Hom(X, _), G) ,
where Nat(K, L) is the set of natural transformations between functors K and L; Hom(X, _) is the Set-valued functor that maps a given monad M into the set of morphisms (in the category of monads) between the monads X and M.
Now we want to apply the Yoneda lemma to our situation where G = F is our monad transformer endofunctor. But then there is a technical difficulty: we cannot use the Yoneda lemma because G is not a set-valued functor (it's a monad-valued functor). We need to map monads into sets in some way. This is not straightforward; for instance, it is not clear how to choose a set that would correspond to the List monad or to the Maybe monad. It is easier to introduce a type parameter t and talk about the type List t or Maybe t. For any given type t there is a well-defined set of all values of type List t. So, we can temporarily choose some arbitrary type t and define a set-valued functor G that maps a monad m into the set of all values of type (F m) t. For this functor G, the Yoneda lemma shown above will hold.
The third step is to choose X = Id in the Yoneda lemma and find:
G Id ≅ Nat(Hom(Id, _), G)
The fourth step is to see why it makes sense to write the right-hand side as ∀ (m: Monad). G m in the notation of a programming language. In fact, since we are working in a purely functional language where parametricity holds, any value of type ∀ (m: Monad). G m must be implemented in a way that is fully parametric in the monad m: it may use only the monad m's methods but no other knowledge about m.
The set Hom(Id, M) is a single-element set because Id is an initial object and there is only one monad morphism between Id and M. So, the functor Hom(Id, _) is a constant functor that maps any object into a single-element set.
What is the set of natural transformations between that constant functor and G? A component at m of such a transformation is a morphism of type Hom(Id, m) => G m. Here => means the arrow in the category Set.
But Hom(Id, m) is a single-element set. So, a morphism Hom(Id, m) => G m is the same as just choosing one element in the set G m.
We find that a natural transformation between Hom(Id, _) and G is the same as a choice, for each monad m, of an element in the set G m in a way that does not depend on the monad m other than through the monad m's methods (in other words, in a fully parametric way). An element in the set G m is the same as a value of type F m t. In a programming language, we would write that as the type ∀ (m: Monad). F m t assuming that values of that type must be fully parametric. The assumption of parametricity allows us to use the parametricity theorem and is necessary because otherwise the values of type ∀ (m: Monad). F m t would not correspond to natural transformations.
In this way we find, in a programming language notation, that:
(F Id) t ≅ ∀ (m: Monad). F m t
This holds for all types t. So, we can rewrite this identity more concisely as:
F Id ≅ ∀ (m: Monad). F m
There are certainly some rough edges in this sketch of a proof, but I'm not sufficiently well-versed in category theory to polish it off.
The analogy with the Yoneda lemma for ordinary types and endofunctors gives the following equivalence between types:
F 0 ≅ ∀ t. F t
because 0 is an initial object in the category of types.
