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](https://zbmath.org/?q=an:0573.03029).



Are bi-embeddable dilators equal?
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.


