Hrbacek, following Ballard, has recently put a certain partial ordering called $\sqsubseteq$ on absolutely everything in order to do nonstandard analysis a la Nelson (i.e. internal set theory):
Let $\mathscr{L}$ be the language of ZFC (and Tarski-Grothendieck if you insist). We say a well-formed formula of $\mathscr{L}$ is an $\in$-formula. We assert that ZFC holds for all well-formed $\in$-formulae.
Now we throw in $\sqsubseteq$ to $\mathscr{L}$ to get a bigger language $\mathscr{HB}.$ First, we assume that ZFC holds for all $\in$-formulae. Let us write
$x \sqsubseteq_\alpha y$ as an abbreviation of
$x \sqsubseteq \alpha \vee x \sqsubseteq y.$
Suppose we have a well-formed formula $P$ of $\mathscr{HB}.$ We write $P^\alpha$ for the replacement of every instance of $\sqsubseteq$ with $\sqsubseteq_\alpha.$
Let us also write $x \sqsubset y$ for
$x \sqsubseteq y \wedge y \not\sqsubseteq x.$
We also write $2^A_{\mathrm{fin}}$ for the set of all finite subsets of $A.$
We also write $(\forall u \sqsubseteq v) P(u,v)$ for $(\forall u)(u \sqsubseteq v \implies P(u,v)),$ and so on for $\exists,$ and for $\in$ as well.
Then Hrbacek's GRIST is the following condition on $\sqsubseteq,$ with four axiom schemata:
R elativization condition on $\sqsubseteq$: $\sqsubseteq$ is a total dense preordering with minimal element
$\emptyset$ and no maximal element; i.e. the conjunction of
Partial ordering: $(\forall u,v,w)((v\sqsubseteq u \wedge w \sqsubseteq v) \implies w \sqsubseteq u) \wedge u \sqsubseteq u;$
Preordering: $(\forall u,v)(u \sqsubseteq v \wedge v \sqsubseteq u);$
Minimality of $\emptyset$: $(\forall u)(\emptyset \sqsubseteq u);$
Illimitability: $(\forall u) (\exists v) (u \sqsubset v);$
Density: $(\forall u,v) (u \sqsubset v \implies (\exists w)(u \sqsubset w \sqsubset v)).$
Axiom schemata, in which we use words so as not to have our eyes completely glaze over:
For any well-formed formula $P$ of $\mathscr{HB}$ depending on finitely many variables,
T ransfer: for all $u \sqsubseteq v$ and $x_1,\ldots, x_n \sqsubseteq u,$
$P^u(x_1,\ldots,x_n) \iff P^v(x_1,\ldots,x_n)$
S tandardization: for all $u \sqsupset \emptyset$ and for all
$A, x_1, \ldots, x_n,$ there are $v \sqsubset u$ and $B \sqsubset v$ such that, for
every $w$ with $v \sqsupseteq w \sqsupset u,$
$(\forall y \sqsubseteq w)(y \in B \iff y \in A \wedge P^w(y,x_1,\ldots,x_n)).$
I dealization: For all $A \sqsubset v$ and all $x_1,\ldots,x_n,$
$(\forall a \in 2^A_{\mathrm{fin}})\big([a\sqsubset v \implies (\exists y)(\forall x \in a) P^v(x,y,x_1,\ldots,x_n)]
\iff[(\exists y)(\forall x \in A)[x \sqsubset u \implies P^v(x,y,x_1,\ldots,x_n)]\big).$
G ranularity: For all $x_1,\ldots,x_k,$ if $(\exists u) P^u(x_1,\ldots,x_k),$ then
$(\exists u)[P^u(x_1,\ldots,x_k) \wedge (\forall v)(v \sqsubset u \implies \neg P^v(x_1,\ldots,x_n))]$