Skip to main content
1 of 3
Tom Ellis
  • 2.9k
  • 2
  • 25
  • 27

Is there a name for relations of this property, and the category of them?

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-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.

Tom Ellis
  • 2.9k
  • 2
  • 25
  • 27