We got stuck on the definition of ordinals when we built the `DEST`

(Double Extension Set Theory) checker on `Cubical Agda`

and reproduced the theorem in [1].

The following concepts are all taken from [1], which defines the Transitive, Trichotomy, Singleton and Well-found:

$\mathrm {Trans}_1(x):=\forall y\in_1x \forall z\in_1 y(z\in_1x)$

$\mathrm {Trichotomy}_1(x):=\forall(y,z)\in_1x ( y\in_1z \vee y=z \vee z\in_1y)$

$S_1(x):=\exists y\forall z(z\in_1y \leftrightarrow z=x)$

$\mathbf{S}_1:= \{x:S_1(x)\}$

$\mathrm {wf}_1(A):= \forall C (\forall x (x \in_1A\wedge x\in_1C\wedge \exists y(y<x\to y\in_1C)) \to \\ \exists z(z<x\to z\in_1C \wedge\forall w(w<z\to w\not\in_1C)))$

The problem is in the section "the set of ordinals":

$$\mathbf{ORD}:=\{\alpha: \\ \forall\beta\in_1\alpha(\beta\color{red}{\in_2}\mathbf{S}_1)\wedge \\ \mathrm {Trans}_1(\alpha)\wedge\forall\beta\in_1\alpha(\mathrm {Trans}_1(\beta))\wedge \\ \mathrm {Trichotomy}_1(\alpha)\wedge\mathrm {wf}_1(\alpha)\}$$

The definition of $\mathbf{ORD}$ uses two different membership relations and is therefore not a uniform formula. By `Axiom Scheme of Comprehension`

[1], $\mathbf{ORD}$ is not a `DEST`

set.

[1]: Holmes, M.R. The Structure of the Ordinals and the Interpretation of ZF in Double Extension Set Theory. Stud Logica 79, 357–372 (2005). https://doi.org/10.1007/s11225-005-3611-x or https://randall-holmes.github.io/Papers/doubleZF2.pdf