> To answer "What is a \\(\mathbf{Bool}\\)-functor?", it is an [elementary embedding](https://ncatlab.org/nlab/show/elementary+embedding) of one preorder into another.

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')\\).

> To answer "What is a \\(\mathbf{Cost}\\)-functor?", it is a generalization of an [isometry](https://en.wikipedia.org/wiki/Isometry) like you mentioned.

Yes, if we change the inequality to an equation in the definition of \\(\mathbf{Cost}\\)-functor we get an isometry between Lawvere metric spaces: a map that preserves distances.

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')\\).

> To answer "What is a \\(\mathbf{Cost}\\)-functor?", it is a generalization of an [isometry](https://en.wikipedia.org/wiki/Isometry) like you mentioned.

Yes, if we change the inequality to an equation in the definition of \\(\mathbf{Cost}\\)-functor we get an isometry between Lawvere metric spaces: a map that preserves distances.