The following math.stackexchange question asked whether there is a name for a certain sort of relation. I have become interested in the question, and no one suggested a name there, so I am asking here instead. Furthermore I would be interested in the name of the category of such relations.
http://math.stackexchange.com/questions/391108/is-there-a-name-for-relations-with-this-propertyhttps://math.stackexchange.com/questions/391108/is-there-a-name-for-relations-with-this-property
I repeat the specification from the above link. The relations are those of the form $\rho : X \rightarrow Y$ such that for all $x,x' \in X$ and all $y,y' \in Y$ we have that the following conditions
$$xy \in \rho$$ $$x'y \in \rho$$ $$xy' \in \rho$$ imply that $$x'y' \in \rho$$
By "category of such relations" I mean the category whose objects are such relations $\rho : X_\rho \rightarrow Y_\rho$, and whose morphisms are pairs of functions $(f_X : X_\rho \to X_{\rho'}, \,\, f_Y : Y_\rho \to Y_{\rho'})$ that preserve relatedness, i.e. $xy \in \rho \Rightarrow f_X(x)f_Y(y) \in \rho'$.
I am considering these concepts in the context of John Reynold's work on relational parametricity in type theory.
