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