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!