@Keith I agree with the banking analogy. My to-go example are the rational numbers under multiplication. This are the snake equations there: \\( 3 = 1 * 3 = (3 * 1/3) * 3 = 3 * (1/3 * 3) = 3 * 1 = 3 \\)
------
@All This is a beginner question: I am still confused by how exactly profunctors work. Consider
I know that the label \\( \cap_x \otimes 1_x \\) is the name of one particular morphism between \\( 1 \otimes x \\) and \\( ( x \otimes x^\ast ) \otimes x \\). But how do we actually get from \\( 1 \otimes x \\) to \\( ( x \otimes x^\ast ) \otimes x \\) ? Is it by calculating the expression \\( ( 1 \otimes x ) \otimes ( \cap_x \otimes 1_x ) \\)? (I know that "calculating the expression" is vague. But I don't know what we are doing exactly.)
----
Edit: I think I get it: So we have a morphism: \\[ \cap_x \otimes 1_x \colon ( X \otimes X) \to ( X \otimes X \otimes X) \\]
Then we apply it (if we think of the morphism as a function that takes one argument):
\\[ \cap_x \otimes 1_x ( ( I \otimes x_1 ) ) = x_1 \otimes x_1^\ast \otimes x_1 \\]
Observation: Here the notion of isomorphic vs. equal is important. It is true that \\( 1 \otimes x \\) is isomorphic to \\( 1 \\). But they are not equal! If this were a program and \\( \cap_x \otimes 1_x \\) a function, then that function would not accept \\( 1 \\) as an argument, but \\( 1 \otimes x \\). Even though they are isomorphic! For the same reason, \\( 1 \otimes x \otimes 1 \\) would not be accepted as an argument. We need exactly two objects of \\( X \\) that are glued together with the tensor operation.
------
Edit2: **Oh great!** My observation cleared up some of my confusion I had about co-design diagrams and feasibility relations! I did not understand: What is the transformation that enables us to switch cables from one side to the other side? These are isomorphisms!
------
@All This is a beginner question: I am still confused by how exactly profunctors work. Consider
I know that the label \\( \cap_x \otimes 1_x \\) is the name of one particular morphism between \\( 1 \otimes x \\) and \\( ( x \otimes x^\ast ) \otimes x \\). But how do we actually get from \\( 1 \otimes x \\) to \\( ( x \otimes x^\ast ) \otimes x \\) ? Is it by calculating the expression \\( ( 1 \otimes x ) \otimes ( \cap_x \otimes 1_x ) \\)? (I know that "calculating the expression" is vague. But I don't know what we are doing exactly.)
----
Edit: I think I get it: So we have a morphism: \\[ \cap_x \otimes 1_x \colon ( X \otimes X) \to ( X \otimes X \otimes X) \\]
Then we apply it (if we think of the morphism as a function that takes one argument):
\\[ \cap_x \otimes 1_x ( ( I \otimes x_1 ) ) = x_1 \otimes x_1^\ast \otimes x_1 \\]
Observation: Here the notion of isomorphic vs. equal is important. It is true that \\( 1 \otimes x \\) is isomorphic to \\( 1 \\). But they are not equal! If this were a program and \\( \cap_x \otimes 1_x \\) a function, then that function would not accept \\( 1 \\) as an argument, but \\( 1 \otimes x \\). Even though they are isomorphic! For the same reason, \\( 1 \otimes x \otimes 1 \\) would not be accepted as an argument. We need exactly two objects of \\( X \\) that are glued together with the tensor operation.
------
Edit2: **Oh great!** My observation cleared up some of my confusion I had about co-design diagrams and feasibility relations! I did not understand: What is the transformation that enables us to switch cables from one side to the other side? These are isomorphisms!
Version 2.1.8p2
