In Girard's $\Pi^1_2$-logic, a dilator $D$ is a endofunctor which commutes with pull-back and direct limit on $\mathrm{ON}$, the category whose objects are ordinals and morphisms are strictly increasing functions. For dilator $D_0,D_1$, an embedding from $D_0$ to $D_1$ is natural transformation from $D_0$ to $D_1$.

My question

Is a following statement true?

If dilators $D_0,D_1$ are bi-embedable, that is there is embeddings $T_0\colon D_0\Rightarrow D_1, T_1\colon D_1\Rightarrow D_0$, then $D_0=D_1$.

I think this statement is true because the fact embeddings of dilators is equal to injective homomorphism when dilators are considered as structures. However I can't check this fact because the paper is written in French….

Girard, Jean-Yves; Ressayre, Jean Pierre, Elements de logique $\Pi^1_n$, Recursion theory, Proc. AMS-ASL Summer Inst., Ithaca/N.Y. 1982, Proc. Symp. Pure Math. 42, 389-445 (1985). ZBL0573.03029.