It looks like you're new here. If you want to get involved, click one of these buttons!
Let's start trying to understand enriched profunctors. We'll start with a very nice special case: 'feasibility relations'.
Definition. Suppose \( (X, \le_X) \) and \( (Y, \le_Y) \) are preorders. Then a feasibility relation from \(X\) to \(Y\) is a monotone function
$$ \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} .$$ If \(\Phi\) is a feasibility relation from \(X\) to \(Y\) we write \( \Phi : X\nrightarrow Y \). If \( \Phi(x,y) = \text{true}\), we say \(x\) can be obtained given \(y\).
The idea is that we use elements of \( X\) to describe 'requirements' - things you want - and elements of \(Y\) to describe 'resources' - things you have. A feasibility relation \( \Phi : X \nrightarrow Y \) says when what you want can be obtained from what you have! And the fact that it's monotone makes a lot of sense.
In fact:
Theorem. A function \(\Phi : X^{\text{op}} \times Y \to \mathbf{Bool}\) is a feasibility relation if and only if:
If \(\Phi(x,y) = \text{true}\) and \(x' \le_X x\) then \(\Phi(x',y) = \text{true}\).
If \(\Phi(x,y) = \text{true}\) and \(y \le_Y y'\) then \(\Phi(x,y') = \text{true}\).
Translating this into English, we see it makes perfect sense:
If what you want can be obtained from the resources you have, and then you change your mind and want less, you can still obtain what you want.
If what you want can be obtained from the resources you have, and then you acquire more resources, you can still obtain what you want.
But let's prove the theorem. This is mainly a nice review of various concepts.
Proof. First, remember that \(\textbf{Bool}\) is the preorder with two elements \(\text{true}\) and \(\text{false}\), with
$$ \text{false} \le \text{true} . $$ We can read \(\le\) here as 'implies'.
Second, remember that \(X^{\text{op}}\) is the opposite of the preorder \(X\), with the definition of \(\le\) turned around:
$$ x \le_{X^{\text{op}}} x' \text{ if and only if } x' \le_X x $$ Third, remember that \( X^{\text{op}} \times Y \) is the product of the preorders \(X^{\text{op}}\) and \(Y\). So, its elements are pairs \( (x,y) \) with \(x \in X\) and \(y \in Y\), and we define a concept of \(\le\) on these pairs by
$$ (x,y) \le (x',y') \text{ if and only if } x' \le_X x \text{ and } y \le_Y y' .$$ Note how I said \(x' \le x\). This looks backwards, but it's not one of my usual typos! It works this way because of the \(\text{op}\) in \( X^{\text{op}} \times Y \).
Now we're ready to see exactly what a feasibility relation, that is a monotone function \(\Phi : X^{\text{op}} \times Y \to \mathbf{Bool}\), really is. It's a function that obeys
$$ (x,y) \le (x',y') \text{ implies } \Phi(x,y) \le \Phi(x',y') $$ or in other words
$$ \text{ if } x' \le_X x \text{ and } y \le_Y y', \text{ then } \Phi(x,y) \text{ implies } \Phi(x',y') $$ Translating this into English to see what this means, it says:
If you can get what you want from the resources you have, and then you change your mind and want less, and also go out and get more resources, then you can still get what you want.
Here "less" really means "less than or equal to", and "more" really means "greater than or equal to" - English is not very good at saying these things quickly! So, the process of wanting less and getting more resources can always be broken into two steps:
wanting less but keeping the resources the same, and then
getting more resources but wanting the same thing.
So, this condition
$$ \text{ if } x' \le_X x \text{ and } y \le_Y y', \text{ then } \Phi(x,y) \text{ implies } \Phi(x',y') $$ is equivalent to the combination of both these conditions:
If \(x' \le_X x \), then \( \Phi(x,y) \) implies \(\Phi(x',y)\).
If \(y \le y'\), then \( \Phi(x,y) \) implies \( \Phi(x,y')\).
But here's another equivalent way to say these two things:
If \(\Phi(x,y) = \text{true}\) and \(x' \le_X x\) then \(\Phi(x',y) = \text{true}\).
If \(\Phi(x,y) = \text{true}\) and \(y \le_X y'\) then \(\Phi(x,y') = \text{true}\).
Logic! Ain't it great? \( \qquad \blacksquare \)
Next time I'll show you how to draw pictures of feasibility relations, and look at some examples. We've already drawn pictures of preorders, or at least posets: they're called Hasse diagrams, and they look like a bunch of dots, one for each element of our poset \(X\), and a bunch of arrows, enough so that \(x \le y\) whenever there's a path of arrows leading from \(x \) to \( y \). So, to draw a feasibility relation \(\Phi : X \nrightarrow Y\), we'll draw two Hasse diagrams and some extra arrows to say when \( \Phi(x,y) = \text{true}\).
Finally, two puzzles:
Puzzle 169. I gave a verbal argument for how we can break up any inequality \( (x,y) \le (x',y') \) in \(X^{\text{op}} \times Y\) into two other inequalities. Can you write this out in a purely mathematical way?
Puzzle 170. What if we have a morphism in a product of categories \( \mathcal{C} \times \mathcal{D}\). Can we always write it as a composite of two morphisms, copying the procedure in my verbal argument and Puzzle 169? How does this work?
Comments
Are the puzzles hard for some reason? They're supposed to be easy once you get this idea:
Maybe translating these words into facts about the preorder \( X^{\text{op}} \times Y\) is hard? Or maybe the puzzles are so easy that everyone is waiting for someone else to do them?
Are the puzzles hard for some reason? They're supposed to be easy once you get this idea: > So, the process of wanting less and getting more resources can always be broken into two steps: > * wanting less but keeping the resources the same, and then > * getting more resources but wanting the same thing. Maybe translating these words into facts about the preorder \\( X^{\text{op}} \times Y\\) is hard? Or maybe the puzzles are so easy that everyone is waiting for someone else to do them?
I don't think they're hard, it's just, I've been reading on co/ends since the \(\text{hom}\)-functor lecture, and the condition in puzzle 169 reminds me of a co-wedge.
However, the typing is off.
I don't think they're hard, it's just, I've been reading on co/ends since the \\(\text{hom}\\)-functor lecture, and the condition in puzzle 169 reminds me of a co-wedge. However, the typing is off.
Can we express the conditions in puzzle 169 as the diagram,
\[ \begin{matrix} & & \Phi(=_{X^{op}},\leq_Y) & & \\ & \Phi(x',y) & \rightarrow & \Phi(x',y') & \\ \Phi(\leq_{X^{op}},=_Y) & \downarrow & & \downarrow & \\ & \Phi(x,y) & \rightarrow & true & \end{matrix} \]
Can we express the conditions in puzzle 169 as the diagram, \\[ \begin{matrix} & & \Phi(=\_{X^{op}},\leq\_Y) & & \\\\ & \Phi(x',y) & \rightarrow & \Phi(x',y') & \\\\ \Phi(\leq\_{X^{op}},=\_Y) & \downarrow & & \downarrow & \\\\ & \Phi(x,y) & \rightarrow & true & \end{matrix} \\]
re Puzzle 169 how about
\((x, y) \leq_{X^\textrm{op}\times Y} (x',y') \iff x \leq_{X^\textrm{op}} x'\) and \(y \leq_Y y' \iff x' \leq_X x\) and \(y \leq_Y y'\)
re **Puzzle 169** how about \\((x, y) \leq_{X^\textrm{op}\times Y} (x',y') \iff x \leq_{X^\textrm{op}} x'\\) and \\(y \leq_Y y' \iff x' \leq_X x\\) and \\(y \leq_Y y'\\)
re Puzzle 170
\((f, g) : (C, D)\rightarrow (C', D') = (f, 1_{D'})\circ (1_C, g) : (C, D)\rightarrow (C, D')\rightarrow (C', D') = (1_{C'}, g)\circ (f, 1_D) : (C, D)\rightarrow (C', D)\rightarrow (C', D')\)
re **Puzzle 170** \\((f, g) : (C, D)\rightarrow (C', D') = (f, 1_{D'})\circ (1_C, g) : (C, D)\rightarrow (C, D')\rightarrow (C', D') = (1_{C'}, g)\circ (f, 1_D) : (C, D)\rightarrow (C', D)\rightarrow (C', D')\\)
I don't think I fully understand the questions though.
I don't think I fully understand the questions though.
I think you do, but I am not sure I understand things either.
I think you do, but I am not sure I understand things either.
At least Anindya understood the questions well enough to correctly answer them!
The point of the questions was this: after we think about it a minute, the definition of feasibility relation says that
$$ \text{if } (x,y) \le (x',y') \text{ in } X^{\text{op}} \times Y, \text{ then }\Phi(x,y) \text{ implies } \Phi(x',y') .$$ But the theorem claims that this one condition is equivalent to two conditions:
if \(x' \le x \) in \(X\), then \( \Phi(x,y) \) implies \(\Phi(x',y)\) for all \(y \in Y\),
if \(y \le y'\) in \(Y\), then \( \Phi(x,y) \) implies \( \Phi(x,y')\) for all \(x \in X\).
So, somehow we must be able to take a single inequality in \( X^{\text{op}} \times Y\) and break it into two inequalities, one in \(X\) and one in \(Y\).
The proof of the theorem explains how... but it might not be clear to everyone. So I wanted you to figure it out:
Puzzle 169. The one inequality \((x,y) \le (x',y')\) in \( X^{\text{op}} \times Y\) is equivalent to two inequalities, one in \(X\) and one in \(Y\). What are they?
But preorders are just a special case of categories, and this fact is just a special case of a fact about categories:
Puzzle 170. Any morphism in a product of categories, \(\mathcal{C} \times \mathcal{D}\), is a composite of two morphisms, one built from a morphism in \(\mathcal{C}\) and one built from a morphism in \(\mathcal{D}\). What are they?
Both puzzles have two correct answers! Why?
This stuff isn't very deep, but it's good to know when you're working with products of categories, or preorders.
At least Anindya understood the questions well enough to correctly answer them! The point of the questions was this: after we think about it a minute, the definition of feasibility relation says that \[ \text{if } (x,y) \le (x',y') \text{ in } X^{\text{op}} \times Y, \text{ then }\Phi(x,y) \text{ implies } \Phi(x',y') .\] But the theorem claims that this one condition is equivalent to _two_ conditions: 1. if \\(x' \le x \\) in \\(X\\), then \\( \Phi(x,y) \\) implies \\(\Phi(x',y)\\) for all \\(y \in Y\\), 2. if \\(y \le y'\\) in \\(Y\\), then \\( \Phi(x,y) \\) implies \\( \Phi(x,y')\\) for all \\(x \in X\\). So, somehow we must be able to take a _single_ inequality in \\( X^{\text{op}} \times Y\\) and break it into _two_ inequalities, one in \\(X\\) and one in \\(Y\\). The proof of the theorem explains how... but it might not be clear to everyone. So I wanted you to figure it out: **Puzzle 169.** The one inequality \\((x,y) \le (x',y')\\) in \\( X^{\text{op}} \times Y\\) is equivalent to two inequalities, one in \\(X\\) and one in \\(Y\\). What are they? But preorders are just a special case of categories, and this fact is just a special case of a fact about categories: **Puzzle 170.** Any morphism in a product of categories, \\(\mathcal{C} \times \mathcal{D}\\), is a composite of two morphisms, one built from a morphism in \\(\mathcal{C}\\) and one built from a morphism in \\(\mathcal{D}\\). What are they? Both puzzles have _two correct answers!_ Why? This stuff isn't very deep, but it's good to know when you're working with products of categories, or preorders.
Now that I think about it, the answer in puzzle 170 implies the answer in puzzle 169.
But to answer 170, a morphism \(h\) in \(\mathcal{C} \times \mathcal{D}\) is equal to a pair of morphisms, one morphism \(f\) in \(\mathcal{C}\) and a morphism \(g\) in \(\mathcal{D}\),
\[ h: \mathcal{C} \times \mathcal{D} \to \mathcal{C} \times \mathcal{D} \\ h = \langle f, g \rangle \]
Setting, \(\mathcal{C}\) to \(X^{op}\), \(\mathcal{D}\) to \(Y\), \(f\) to \(\leq_{X^{op}}\) and \(g\) to \(\leq_Y\) answers question 169.
Now that I think about it, the answer in puzzle 170 implies the answer in puzzle 169. But to answer 170, a morphism \\(h\\) in \\(\mathcal{C} \times \mathcal{D}\\) is equal to a pair of morphisms, one morphism \\(f\\) in \\(\mathcal{C}\\) and a morphism \\(g\\) in \\(\mathcal{D}\\), \\[ h: \mathcal{C} \times \mathcal{D} \to \mathcal{C} \times \mathcal{D} \\\\ h = \langle f, g \rangle \\] Setting, \\(\mathcal{C}\\) to \\(X^{op}\\), \\(\mathcal{D}\\) to \\(Y\\), \\(f\\) to \\(\leq\_{X^{op}}\\) and \\(g\\) to \\(\leq_Y\\) answers question 169.
OK I think I see the connection now.
We're trying to prove this theorem:
Showing that the one condition implies the two conditions is trivial. But what about the other way round?
Suppose we have the two conditions and also \((x,y) \le (x',y')\), ie \(x'\le x\) and \(y\le y'\).
We have a choice of two routes here.
One route goes: \((x,y) \le (x',y) \le (x',y')\), so \(\Phi(x, y)\) implies \(\Phi(x',y)\) by condition 1, which implies \(\Phi(x',y')\) by condition 2.
The other route goes: \((x,y) \le (x,y') \le (x',y')\), so \(\Phi(x, y)\) implies \(\Phi(x,y')\) by condition 2, which implies \(\Phi(x',y')\) by condition 1.
So we can prove our theorem in two distinct ways corresponding to the two ways of "factorising" \((x,y) \le (x',y')\).
OK I think I see the connection now. We're trying to prove this theorem: > the definition of feasibility relation says that > > \[ \text{if } (x,y) \le (x',y') \text{ in } X^{\text{op}} \times Y, \text{ then }\Phi(x,y) \text{ implies } \Phi(x',y') .\] > > this one condition is equivalent to two conditions: > > 1. if \\(x' \le x \\) in \\(X\\), then \\( \Phi(x,y) \\) implies \\(\Phi(x',y)\\) for all \\(y \in Y\\), > > 2. if \\(y \le y'\\) in \\(Y\\), then \\( \Phi(x,y) \\) implies \\( \Phi(x,y')\\) for all \\(x \in X\\). Showing that the one condition implies the two conditions is trivial. But what about the other way round? Suppose we have the two conditions and also \\((x,y) \le (x',y')\\), ie \\(x'\le x\\) and \\(y\le y'\\). We have a choice of two routes here. One route goes: \\((x,y) \le (x',y) \le (x',y')\\), so \\(\Phi(x, y)\\) implies \\(\Phi(x',y)\\) by condition 1, which implies \\(\Phi(x',y')\\) by condition 2. The other route goes: \\((x,y) \le (x,y') \le (x',y')\\), so \\(\Phi(x, y)\\) implies \\(\Phi(x,y')\\) by condition 2, which implies \\(\Phi(x',y')\\) by condition 1. So we can prove our theorem in two distinct ways corresponding to the two ways of "factorising" \\((x,y) \le (x',y')\\).
Anindya - right! There are always two ways to "factorize" an inequality in a product of preorders, and as Keith noted, this is a special case of a more general fact: there are always two ways to factorize a morphism in a product of categories.
Namely, as you said a while back, any morphism in a product of categories \(\mathcal{C} \times \mathcal{D}\) is of the form
$$ (f,g) : (x,y) \to (x',y') $$ and we always have
$$ (f,g) = (f,1_{y'}) \circ (1_x, g) $$ but also
$$ (f,g) = (1_{x'}, g) \circ (f, 1_y) $$ It's nice to think of this using a commutative square:
$$ \begin{matrix} & & (f, 1_y) & & \\ & (x,y) & \rightarrow & (x',y) &\\ (1_x, g) & \downarrow & & \downarrow & (1_{x'},g) \\ & (x,y') & \rightarrow & (x',y') &\\ & & (f,1_{y'}) & & \\ \end{matrix} $$ The morphism \((f,g)\) goes down the diagonal of this square, from upper left to lower right - but this typesetting system is too wimpy for me to draw it here!
Anindya - right! There are always two ways to "factorize" an inequality in a product of preorders, and as Keith noted, this is a special case of a more general fact: there are always two ways to factorize a morphism in a product of categories. Namely, as you said a while back, any morphism in a product of categories \\(\mathcal{C} \times \mathcal{D}\\) is of the form \[ (f,g) : (x,y) \to (x',y') \] and we always have \[ (f,g) = (f,1_{y'}) \circ (1_x, g) \] but also \[ (f,g) = (1_{x'}, g) \circ (f, 1_y) \] It's nice to think of this using a commutative square: \[ \begin{matrix} & & (f, 1_y) & & \\\\ & (x,y) & \rightarrow & (x',y) &\\\\ (1_x, g) & \downarrow & & \downarrow & (1_{x'},g) \\\\ & (x,y') & \rightarrow & (x',y') &\\\\ & & (f,1_{y'}) & & \\\\ \end{matrix} \] The morphism \\((f,g)\\) goes down the diagonal of this square, from upper left to lower right - but this typesetting system is too wimpy for me to draw it here!
Hi John, I don't know if you're aware, but this lecture doesn't seem to be included on this page yet. I think it's also missing the lecture about free and forgetful functors from chapter 3 (which renumbers everything).
Hi John, I don't know if you're aware, but this lecture doesn't seem to be included on [this page](http://www.azimuthproject.org/azimuth/show/Applied+Category+Theory#Course) yet. I think it's also missing the lecture about free and forgetful functors from chapter 3 (which renumbers everything).
Also here's a diagram of the commutative square in puzzle 170 (similar to the one drawn by John above).
Because the diagram commutes, we have \( (f,g) = (f,1_{y'}) \circ (1_x,g) = (1_{x'},g) \circ (f,1_y) \). If \( (f,g) \) is a preorder on \( X^\mathrm{op} \times Y\), then the diagram is the solution to puzzle 169. You can translate the category theoretic concepts back into preorder ones for a proof: If \(x' \le x\) in \(X\), then \(x \le x'\) in \(X^\mathrm{op}\) and if \(y \le y'\) in \(Y\), then by reflexitivity, we have \((x,y) \le (x',y)\) and \((x',y) \le (x',y')\). By transitivity, we have \((x,y) \le (x',y)\) and \((x',y) \le (x',y')\) implies \((x,y)\le (x',y')\).
Also here's a [diagram of the commutative square](https://tikzcd.yichuanshen.de/#eyJub2RlcyI6W3sicG9zaXRpb24iOlswLDBdLCJ2YWx1ZSI6Iih4LHkpIn0seyJwb3NpdGlvbiI6WzEsMF0sInZhbHVlIjoiKHgnLHkpIn0seyJwb3NpdGlvbiI6WzEsMV0sInZhbHVlIjoiKHgnLHknKSJ9LHsicG9zaXRpb24iOlswLDFdLCJ2YWx1ZSI6Iih4LHknKSJ9XSwiZWRnZXMiOlt7ImZyb20iOjAsInRvIjoxLCJ2YWx1ZSI6IihmLDFfeSkifSx7ImZyb20iOjAsInRvIjozLCJ2YWx1ZSI6IigxX3gsZykiLCJsYWJlbFBvc2l0aW9uIjoicmlnaHQifSx7ImZyb20iOjMsInRvIjoyLCJ2YWx1ZSI6IihmLDFfe3knfSkiLCJsYWJlbFBvc2l0aW9uIjoicmlnaHQifSx7ImZyb20iOjEsInRvIjoyLCJ2YWx1ZSI6IigxX3t4J30sZykifSx7ImZyb20iOjAsInRvIjoyLCJsYWJlbFBvc2l0aW9uIjoicmlnaHQiLCJ2YWx1ZSI6IihmLGcpIn1dfQ==) in puzzle 170 (similar to the one drawn by John above). Because the diagram commutes, we have \\( (f,g) = (f,1_{y'}) \circ (1_x,g) = (1_{x'},g) \circ (f,1_y) \\). If \\( (f,g) \\) is a preorder on \\( X^\mathrm{op} \times Y\\), then the diagram is the solution to puzzle 169. You can translate the category theoretic concepts back into preorder ones for a proof: If \\(x' \le x\\) in \\(X\\), then \\(x \le x'\\) in \\(X^\mathrm{op}\\) and if \\(y \le y'\\) in \\(Y\\), then by reflexitivity, we have \\((x,y) \le (x',y)\\) and \\((x',y) \le (x',y')\\). By transitivity, we have \\((x,y) \le (x',y)\\) and \\((x',y) \le (x',y')\\) implies \\((x,y)\le (x',y')\\).
Scott wrote:
Thanks! I've been falling behind on adding lectures to that page. I'm doing it now, but I want to remind everyone that we're all able to edit these Azimuth Wiki pages by clicking at the bottom of the page. It's not hard, and I would be very happy not to be the only one doing this work. At certain points, enthusiastic students have done large amounts of work on the Wiki, and that's great.
Scott wrote: > Hi John, I don't know if you're aware, but this lecture doesn't seem to be included on [this page](http://www.azimuthproject.org/azimuth/show/Applied+Category+Theory#Course) yet. I think it's also missing the lecture about free and forgetful functors from chapter 3 (which renumbers everything). Thanks! I've been falling behind on adding lectures to that page. I'm doing it now, but I want to remind everyone that we're all able to edit these Azimuth Wiki pages by clicking at the bottom of the page. It's not hard, and I would be very happy not to be the only one doing this work. At certain points, enthusiastic students have done large amounts of work on the Wiki, and that's great.
Thanks!
I didn't know that! I'll keep that in mind, next time I see a discrepancy!
Thanks! > I want to remind everyone that we're all able to edit these Azimuth Wiki pages by clicking at the bottom of the page. It's not hard, and I would be very happy not to be the only one doing this work. I didn't know that! I'll keep that in mind, next time I see a discrepancy!
Some minor stuff, when
$$ \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} $$ we write \( \Phi : X\nrightarrow Y \) but nLab, Wikipedia and Borceaux write \( \Phi : Y\nrightarrow X \) (from the covariant to the contravariant argument).
Some minor stuff, when \[ \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} \] we write \\( \Phi : X\nrightarrow Y \\) but nLab, Wikipedia and Borceaux write \\( \Phi : Y\nrightarrow X \\) (from the covariant to the contravariant argument).
Jesus - yes, there are huge religious wars fought over this arbitrary convention.
I actually prefer the nLab, Wikipedia and Borceaux convention, because a \(\mathcal{V}\)-enriched functor from \(\mathcal{X} \times \mathcal{Y}^{\text{op}}\) to \(\mathcal{V}\) can be reinterpreted as a functor from \(\mathcal{X}\) to the so-called presheaf category \(\mathcal{V}^{\mathcal{Y}^{\text{op}}}\), and that's a good thing. For example, the '\(\mathcal{V}\)-enriched Yoneda embedding' is a \(\mathcal{V}\)-enriched functor
$$ Y \colon \mathcal{X} \to \mathcal{V}^{\mathcal{X}^{\text{op}}} .$$ However, Fong and Spivak use the convention I'm using here... and that's why I'm using it.
I disagree with a lot of their conventions; luckily, it doesn't really matter much which conventions you use.
Jesus - yes, there are huge religious wars fought over this arbitrary convention. I actually prefer the nLab, Wikipedia and Borceaux convention, because a \\(\mathcal{V}\\)-enriched functor from \\(\mathcal{X} \times \mathcal{Y}^{\text{op}}\\) to \\(\mathcal{V}\\) can be reinterpreted as a functor from \\(\mathcal{X}\\) to the so-called **presheaf category** \\(\mathcal{V}^{\mathcal{Y}^{\text{op}}}\\), and that's a good thing. For example, the '\\(\mathcal{V}\\)-enriched Yoneda embedding' is a \\(\mathcal{V}\\)-enriched functor \[ Y \colon \mathcal{X} \to \mathcal{V}^{\mathcal{X}^{\text{op}}} .\] However, Fong and Spivak use the convention I'm using here... and that's why I'm using it. I disagree with a lot of their conventions; luckily, it doesn't really matter much which conventions you use.
Edit: Now i understand how the definition works out. It is also neat that the preimage of true forms a upper set in \( X^{\text{op}} \times Y. \) If more such nice properties arise, I get why ther rather reversed the arrows in X instead of defining the feasability relation in a different way.
But why does x′≤x not work fine with \( \Phi : X \times Y \to \mathbf{Bool} ? \) With \( {\text{op}} \), there seems to be a notion of going 'backwards' in x′≤x as opposed to x≤x′. But in a poset \( (X, ≤) \) i think we can always go backwards and forwards as much as we like, given the pairs are part of the relation ≤.
I think I understood that reversing the arrows in a category is analog to reversing a preorder. But I don't understand why it is necessary. According to my understanding, it should be possible to avoid ever having to write \( {X^\text{op}} \) by choosing the preorder relations \( \leq_{X} \) and \( \leq_{Y} \) in an appropriate way when working with feasibility relations, their combinations, tensors and all the other constructs. Where is my error?
PS: I am having a blast catching up to the active areas of this class! It is so great seeing how the CT parts are interconnected, but also connectable to the real world! :) Thank you very much John!
Edit: Now i understand how the definition works out. It is also neat that the preimage of true forms a upper set in \\( X^{\text{op}} \times Y. \\) If more such nice properties arise, I get why ther rather reversed the arrows in X instead of defining the feasability relation in a different way. ------ > Note how I said x′≤x. This looks backwards, but it's not one of my usual typos! It works this way because of the op in \\( \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} ? \\) But why does x′≤x not work fine with \\( \Phi : X \times Y \to \mathbf{Bool} ? \\) With \\( {\text{op}} \\), there seems to be a notion of going 'backwards' in x′≤x as opposed to x≤x′. But in a poset \\( (X, ≤) \\) i think we can always go backwards and forwards as much as we like, given the pairs are part of the relation ≤. I think I understood that reversing the arrows in a category is analog to reversing a preorder. But I don't understand why it is necessary. **According to my understanding, it should be possible to avoid ever having to write \\( {X^\text{op}} \\) by choosing the preorder relations \\( \leq_{X} \\) and \\( \leq_{Y} \\) in an appropriate way when working with feasibility relations, their combinations, tensors and all the other constructs.** Where is my error? ----------- PS: I am having a blast catching up to the active areas of this class! It is so great seeing how the CT parts are interconnected, but also connectable to the real world! :) Thank you very much John!