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)