How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?
$\newcommand{\fix}{\mathsf{fix}}$
$\newcommand{\fold}{\mathsf{fold}}$
$\newcommand{\map}{\mathsf{map}}$
Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to rework some stuff slightly for my own understanding. We have: $$C = ∀ r. (F r → r) → r$$ with $F$ functorial. We have: $$\fix : F C → C$$ corresponding to your definition, and I'm going to call a generalization of your m: $$\fold : (F r → r) → C → r \\ \fold\ α\ c = c\ α$$
So, we want to prove that for all $c : C$, $\fold\ \fix\ c = c$
Parametricity looks like this:
$$∀(R : a \Leftrightarrow b).\\ ∀ (α : F a → a) (β : F b → b).\\ (∀ x y. FR(x,y) → R (α\ x, β\ y))\\ → ∀ c. R (c\ α, c\ β)$$
To unpack this a bit, if we have a types $a,b$, a relation $R$ on them, algebra structures $α,β$, and a proof that they preserve the relation, then $R$ relates $c \  α$ to $c \ β$. The idea behind the &quot;preservation&quot; criterion is that $FR(x, y)$ holds if $x$ and $y$ have the same $F$ 'shape', and corresponding occurrences of $a$ and $b$ values are related by $R$.
So, let's make some choices. Suppose we have $ζ : F z → z$. Then: $$a \equiv C \\ b \equiv z \\ R(c, z) \equiv c\ ζ = z \\ α \equiv \fix \\ β \equiv ζ$$ the result of parametricity for these choices will be: $$R(c\ \fix, c\ ζ) \equiv c\ \fix\ ζ = c\ ζ$$
Then by function extensionality we will obtain $c = c\ \fix = \fold\ \fix\ c$. Our obligation is to prove:
$$∀ fc\ fz. FR(fc,fz) → R (\fix\ fc,ζ\ fz)$$
The goal is $$\fix\ fc\ ζ = ζ\ fz$$
By unfolding the definition of $\fix$ we know: $$\fix\ fc\ ζ = ζ (\map_F\ (\fold\ ζ)\ fc)$$
However, the meaning of $FR(fc,fz)$ is actually that $$\map_F\ (\fold\ ζ)\ fc = fz$$ So the result is immediate.
I haven't thought about whether it's possible to make due with dinaturality. I think it is not, but I could be wrong.
Edit:
The free theorem for this scenario is:
$$(∀ x. f (α\ x) = β (\map_F\ f \ x)) \Rightarrow f (c\ α) = c\ β$$
If we choose $$f = \fold\ ζ \\ α = \fix \\ β = ζ$$ then our obligation is:
$$\fold\ ζ\ (\fix\ x) = \fix\ x\ ζ = ζ (\map_F\ (\fold\ ζ)\ x)$$
which is just the definition of $\fix$. The result is:
$$\fold\ ζ\ (c\ \fix) = c\ ζ$$
which again gives us what we wanted. Note that this is also not the same as dinaturality, though. I believe the difference is that dinaturality allows us to shift $f$ around in the expression, but parametricity allows us to absorb it into one of the algebras.