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!