Recall \$$\textbf{Bool} = ( \mathbb{B} , \le, true, \wedge) \$$ from Example 2.24 and \$$\textbf{Cost} = ([0, \infty], \ge, 0, +) \$$ from Example 2.34.
There is a monoidal monotone \$$g : \textbf{Bool} \rightarrow \textbf{Cost} \$$, given by \$$g(false) := \infty \text{ and } g(true) := 0 \$$.

1. Check that the map \$$g : ( \mathbb{B} , \le, \text{true}, \wedge) \rightarrow ([0, \infty], \ge, 0, +) \$$ presented above indeed
* is monotonic,
* satisfies the condition a. of Definition 2.34, and
* satisfies the condition b. of Definition 2.34.
2. Is \$$g \$$ a strict monoidal monotone?

**Definition 2.34**.
Let \$$\mathcal{P} = (P, \le_P , I_P , \otimes_P ) \$$ and \$$\mathcal{Q} = (Q, \le_Q , I_Q , \otimes_Q ) \$$ be monoidal preorders.
A monoidal monotone from \$$\mathcal{P} \$$ to \$$\mathcal{Q} \$$ is a monotone map \$$f : (P, \le_P ) \rightarrow (Q, \le_Q ) \$$, satisfying two conditions:

a. \$$I_Q ≤ f ( I_P ) \$$, and

b. \$$f(p_1 ) \otimes_Q f(p_2 ) ≤ Q f (p_1 \otimes_P p_2 ) \$$

for all \$$p_1 , p_2 \in P \$$ .

**strong monoidal monotone** replace \$$\le\$$ with \$$\cong \$$

**strict monoidal monotone** replace \$$\le\$$ with \$$= \$$

[Previous](https://forum.azimuthproject.org/discussion/1984)
[Next](https://forum.azimuthproject.org/discussion/1986)