Jonathan wrote:

>First, going nowhere might actually cost you. Maybe you're renting. Second, it pays to take the scenic route! Even if you end up back where you started, you won't be worse off than if you'd stayed put. Shop around!

I really dig this version of reality! Seems like good life advice.

> **Puzzle 88.** Show that these choices actually makes \$$\mathbf{Cost}\$$ into a symmetric monoidal poset.

We have \$$([0,\infty],\ge,+,0) \$$. Note the unintuitive opposite ordering of \$$\mathbf{Cost}\$$. E.g \$$1 \ge 3 \$$. Because of the \$$\infty \$$ we need to consider the special cases it creates.

**Poset Conditions:** \$$x \ge x\$$ clearly holds, also for \$$\infty \$$. \$$x \ge y \$$ and \$$y \ge z \$$ implies \$$x \ge z \$$ also holds since we have a linear order. E.g \$$0 \ge 2 \$$ and \$$2 \ge \infty \$$ and indeed \$$0 \ge \infty \$$. Finally, \$$x \ge y \$$ and \$$y \ge x \$$ implies \$$x = y \$$ holds again because we have a linear order without equivalent elements.

**Monoid Conditions:** \$$I \otimes x = x = x \otimes I \$$ holds since \$$0 + x = x = x + 0\$$ for all x including \$$\infty \$$. \$$(x \otimes y) \otimes y = x \otimes (y \otimes z)\$$ since addition is associative.

**Symmetric Monoidal Poset Conditions:** \$$x \ge x' \$$ and \$$y \ge y' \$$ implies \$$x \otimes y \ge x' \otimes y' \$$ holds for all \$$x,x',y,y'\$$ including \$$\infty \$$. E.g \$$0 \ge \infty \$$ and \$$\infty \ge \infty \$$ and indeed \$$0 + \infty \ge \infty + \infty \$$. Finally, \$$x \otimes y \ge y \otimes x\$$ and \$$y \otimes x \ge x \otimes y\$$ both hold since \$$x+y = y+x\$$ since addition is commutative.

*Question:* John called this thing a **symmetric monoidal poset**, but since it's a poset and \$$x \ge y \$$ and \$$y \ge x \$$ implies \$$x = y \$$, shouldn't \$$x \otimes y \ge y \otimes x\$$ and \$$y \otimes x \ge x \otimes y\$$ imply \$$x \otimes y = y \otimes x\$$, meaning it's the same as a **commutative monoidal poset**. I guess the question boils down to whether the product of a poset with itself is also a poset. If we define the product as: \$$(x,y) \le_{X \times X} (y,y') \text{ iff } x \le_X y \text{ and } x' \le_X y' \$$ this seems to be the case.