It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.2K
- Applied Category Theory Course 352
- Applied Category Theory Seminar 4
- Exercises 149
- Discussion Groups 49
- How to Use MathJax 15
- Chat 479
- Azimuth Code Project 108
- News and Information 145
- Azimuth Blog 149
- Azimuth Forum 29
- Azimuth Project 189
- - Strategy 108
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 711
- - Latest Changes 701
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 21
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 39

Options

1) Justify each of the four steps \( (=, \le, \le, =) \) in Eq. (4.27).

2) In the case \( \mathcal{V} = \textbf{Bool} \), we can directly show each of the four steps in Eq. (4.27) is actually an equality. How?

**Equation 4.27**

Φ(p, q) I ⊗ Φ(p, q) ≤ P(p, p) ⊗ Φ(p, q) ≤ Ü P(p, p 1 ) ⊗ Φ(p 1 , q) (U P .Φ)(p, q).

## Comments

\(\Phi(p,q)=I\otimes\Phi(p,q)\) holds because \(\mathcal{V}\) is a symmetric monoidal preorder (in particular, this is property b) in the definition of a symmetric monoidal structure on a preorder). \(I\otimes\Phi(p,q)\leq\mathcal{P}(p,p)\otimes\Phi(p,q)\) holds since \(\mathcal{P}\) is a \(\mathcal{V}-\)category (in particular, property a) in the definition of a \(\mathcal{V}-\)category and property a) in the definition of a monoidal structure on a preorder). \(\mathcal{P}(p,p)\otimes\Phi(p,q)\leq\bigvee_{p_1\in\mathcal{P}}\mathcal{P}(p,p_1)\otimes\Phi(p_1,q)\) is true since \(p\in\mathcal{P}\), by the definition of join (joins always exist since \(\mathcal{V}\) is a quantale). \(\bigvee_{p_1\in\mathcal{P}}\mathcal{P}(p,p_1)\otimes\Phi(p_1,q)=(U_\mathcal{P}\circ\Phi)(p,q)\) by the definition of the unit profunctor and the definition of profunctor composition.

If \(\Phi(p,q)=\mathrm{true}\) then, since \(\mathrm{true}\) is the top element of

Bool, all of the other profunctors must also evaluate to \(\mathrm{true}\), since there is nothing larger for them to be. So all the inequalities are equalities. The only other possible value for \((U_\mathcal{P}\circ\Phi)(p,q)\) is \(\mathrm{false}\), which is the bottom element ofBool, so the other profunctors must also be \(\mathrm{false}\), as there is nothing smaller for them to be. So, again all the inequalities are equalities. Since these two possibilities cover all possible values of the profunctors in each part of the chain of equalities and inequalities, all of the relations in the chain are equalities when \(\mathcal{V}=\textbf{Bool}\).`1. \\(\Phi(p,q)=I\otimes\Phi(p,q)\\) holds because \\(\mathcal{V}\\) is a symmetric monoidal preorder (in particular, this is property b) in the definition of a symmetric monoidal structure on a preorder). \\(I\otimes\Phi(p,q)\leq\mathcal{P}(p,p)\otimes\Phi(p,q)\\) holds since \\(\mathcal{P}\\) is a \\(\mathcal{V}-\\)category (in particular, property a) in the definition of a \\(\mathcal{V}-\\)category and property a) in the definition of a monoidal structure on a preorder). \\(\mathcal{P}(p,p)\otimes\Phi(p,q)\leq\bigvee\_{p\_1\in\mathcal{P}}\mathcal{P}(p,p\_1)\otimes\Phi(p\_1,q)\\) is true since \\(p\in\mathcal{P}\\), by the definition of join (joins always exist since \\(\mathcal{V}\\) is a quantale). \\(\bigvee\_{p\_1\in\mathcal{P}}\mathcal{P}(p,p\_1)\otimes\Phi(p\_1,q)=(U\_\mathcal{P}\circ\Phi)(p,q)\\) by the definition of the unit profunctor and the definition of profunctor composition. 2. If \\(\Phi(p,q)=\mathrm{true}\\) then, since \\(\mathrm{true}\\) is the top element of **Bool**, all of the other profunctors must also evaluate to \\(\mathrm{true}\\), since there is nothing larger for them to be. So all the inequalities are equalities. The only other possible value for \\((U\_\mathcal{P}\circ\Phi)(p,q)\\) is \\(\mathrm{false}\\), which is the bottom element of **Bool**, so the other profunctors must also be \\(\mathrm{false}\\), as there is nothing smaller for them to be. So, again all the inequalities are equalities. Since these two possibilities cover all possible values of the profunctors in each part of the chain of equalities and inequalities, all of the relations in the chain are equalities when \\(\mathcal{V}=\textbf{Bool}\\).`

In the current version of Seven Sketches (in Compositionality), there is a third part:

3 Justify each of the three steps \((=,\leq,\leq)\newcommand{\cat}[1]{\mathcal{#1}}\) in \eqref{SecondHalfLeftUnitLaw}. \begin{equation}\label{SecondHalfLeftUnitLaw} \tag{4.29} \cat{P}(p,p_1)\otimes\Phi(p_1,q)=\cat{P}(p,p_1)\otimes\Phi(p_1,q)\otimes I\leq\cat{P}(p,p_1)\otimes\Phi(p_1,q)\otimes\cat{Q}(q,q)\leq\Phi(p,q).\end{equation}(Which the text says follows from Definitions 2.46 and 4.8.)

These follow from \(\mathcal{V}\) being a symmetric monoidal preorder (same property as in the above comment), \(\mathcal{Q}\) being a \(\mathcal{V}-\)category (same as above, which is Definition 2.46), and exercise 4.9 (which immediately follows definition 4.8 and is one of the equivalent ways of defining \(\mathcal{V}-\)profunctors).

`In the current version of Seven Sketches (in Compositionality), there is a third part: 3 Justify each of the three steps \\((=,\leq,\leq)\newcommand{\cat}[1]{\mathcal{#1}}\\) in \eqref{SecondHalfLeftUnitLaw}. \begin{equation}\label{SecondHalfLeftUnitLaw} \tag{4.29} \cat{P}(p,p_1)\otimes\Phi(p_1,q)=\cat{P}(p,p_1)\otimes\Phi(p_1,q)\otimes I\leq\cat{P}(p,p_1)\otimes\Phi(p_1,q)\otimes\cat{Q}(q,q)\leq\Phi(p,q).\end{equation}(Which the text says follows from Definitions 2.46 and 4.8.) These follow from \\(\mathcal{V}\\) being a symmetric monoidal preorder (same property as in the above comment), \\(\mathcal{Q}\\) being a \\(\mathcal{V}-\\)category (same as above, which is Definition 2.46), and exercise 4.9 (which immediately follows definition 4.8 and is one of the equivalent ways of defining \\(\mathcal{V}-\\)profunctors).`