> I tend to associate the term "elementary embedding" with more fancy contexts from logic... but maybe this is right.
>
> In simpler terms, it's a map between posets \$$f : X \to Y\$$ such that \$$x \le x'\$$ if and only if \$$f(x) \le f(x')\$$.

*Elementary embedding* is not right. It's merely an [*embedding*](https://en.wikipedia.org/wiki/Embedding#Universal_algebra_and_model_theory), rather than an elementary embedding.

Here's an example of an embedding that is not elementary. We can embed the singleton poset **Unit** (the singleton poset) into **Bool** with \$$f\$$ where \$$f(\ast) = \mathtt{false}\$$. While \$$\mathbf{Unit} \models \forall x. x \leq \ast\$$, it is not the case that \$$\mathbf{Bool} \models \forall x. x \leq f(\ast)\$$.

Thanks for catching my mistake.