# Are bi-embeddable dilators equal?

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 a 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.

No. For example consider the dilator $$D$$ that maps a well-order $$A$$ to the well-order consisting of denotations
1. $$(2n;x,y)$$, where $$y<_Ax$$ are elements of $$A$$;
2. $$(2n+1;x)$$, where $$x\in A$$.
The denotations are compared by lexicographical order. For a morphism $$f \colon A\to B$$ we as usual put $$D(f)((m;x_1,\ldots,x_k))=(m;f(x_1),\ldots,f(x_k))$$. Now consider the dilator $$D'$$ that omits from $$D$$ all the denotations of the form $$(0;x,y)$$. Clearly, $$D$$ and $$D'$$ are bi-embeddable, but not equal.