>**Puzzle 86.** Show that \\(\mathbf{Bool}\\) becomes a symmetric monoidal poset if we use the usual ordering \\(\tt{false} \le \tt{true}\\), take \\(\otimes\\) to be \\(\wedge\\) - that is, "and" - and take \\(I\\) to be \\(\tt{true}\\) .

I'm just going to gut out the definition for a monoidal preorder from the book and modify it for a symmetric monoidal poset.

>Definition 2.1. A symmetric monoidal structure on a poset (X, ≤) consists of two constituents:

(i) an element I ∈ X, called the monoidal unit, and

(ii) a function ⊗: X × X → X, called the monoidal product.

Yes, we take \\(I\\) to be \\(\tt{true}\\) and take \\(\otimes\\) to be \\(\wedge\\), as was given.

>These constituents must satisfy the following properties:

(a) for all x1, x2, y1, y2 ∈ X, if x1 ≤ y1 and x2 ≤ y2, then x1 ⊗ x2 ≤ y1 ⊗ y2,

Since \\(\otimes\\) is defined to be \\(\wedge\\) - that is, "and", this is somewhat trivially true.

$$

x_1 \wedge x_2 \leq y_1 \wedge y_2 \Leftrightarrow x_1 \leq y_1 \ \tt{and} \ x_2 \leq y_2

$$

>(b) for all x ∈ X, the equations I ⊗ x = x and x ⊗ I = x hold,

Since and'ing by the truth does nothing to our object \\(x\\), this holds.

$$

\tt{true}\wedge x = x =x \wedge \tt{true}

$$

>(c) for all x, y, z ∈ X, the equation (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z) holds,

Follows from the associativity of \\(\wedge\\),

$$

(x\wedge y) \wedge z = x \wedge (y \wedge z)

$$

>(d) for all x, y ∈ X, the [equation] x ⊗ y = y ⊗ x holds.

Follows from th symmetry of \\(\wedge\\),

$$

x \wedge y = y \wedge x.

$$

Edit: Whoops almost forgot.

Lastly, for a poset, we need to check anti-symmetry, x ≤ y and y ≤ x.

$$

\tt{false} \leq x \ and \ x \leq \tt{false} \Rightarrow x =\tt{false}

$$

holds, and likewise so does,

$$

x \leq \tt{true} \ \tt{and} \ \tt{true} \leq x \Rightarrow x =\tt{true}

$$

I'm just going to gut out the definition for a monoidal preorder from the book and modify it for a symmetric monoidal poset.

>Definition 2.1. A symmetric monoidal structure on a poset (X, ≤) consists of two constituents:

(i) an element I ∈ X, called the monoidal unit, and

(ii) a function ⊗: X × X → X, called the monoidal product.

Yes, we take \\(I\\) to be \\(\tt{true}\\) and take \\(\otimes\\) to be \\(\wedge\\), as was given.

>These constituents must satisfy the following properties:

(a) for all x1, x2, y1, y2 ∈ X, if x1 ≤ y1 and x2 ≤ y2, then x1 ⊗ x2 ≤ y1 ⊗ y2,

Since \\(\otimes\\) is defined to be \\(\wedge\\) - that is, "and", this is somewhat trivially true.

$$

x_1 \wedge x_2 \leq y_1 \wedge y_2 \Leftrightarrow x_1 \leq y_1 \ \tt{and} \ x_2 \leq y_2

$$

>(b) for all x ∈ X, the equations I ⊗ x = x and x ⊗ I = x hold,

Since and'ing by the truth does nothing to our object \\(x\\), this holds.

$$

\tt{true}\wedge x = x =x \wedge \tt{true}

$$

>(c) for all x, y, z ∈ X, the equation (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z) holds,

Follows from the associativity of \\(\wedge\\),

$$

(x\wedge y) \wedge z = x \wedge (y \wedge z)

$$

>(d) for all x, y ∈ X, the [equation] x ⊗ y = y ⊗ x holds.

Follows from th symmetry of \\(\wedge\\),

$$

x \wedge y = y \wedge x.

$$

Edit: Whoops almost forgot.

Lastly, for a poset, we need to check anti-symmetry, x ≤ y and y ≤ x.

$$

\tt{false} \leq x \ and \ x \leq \tt{false} \Rightarrow x =\tt{false}

$$

holds, and likewise so does,

$$

x \leq \tt{true} \ \tt{and} \ \tt{true} \leq x \Rightarrow x =\tt{true}

$$