Let Rel be the category whose objects are sets and whose morphisms are binary relations, with composition defined by $x (S \circ R) z \Leftrightarrow (\exists y : x R y \wedge y S z)$, and identity the equality relation.

If we have relations $R \in Rel(X, X')$ and $S \in Rel(Y, Y')$, we can define a relation $(R \to S) \in Rel(X \to Y, X' \to Y')$ by \begin{equation} f (R \to S) g \Leftrightarrow (\forall x \in X, x' \in X' : x R x' \Rightarrow f(x) S g(x')), \end{equation} i.e. functions are related iff they map related arguments to related values.

Unfortunately, this does not constitute a bifunctor $\to : Rel \times Rel \to Rel$. Indeed, composition is not respected. We have $(R' \to S') \circ (R \to S) \subseteq (R' \circ R) \to (S' \circ S)$, but in general these relations are not equal.

My question is: what is this operation $\to$? Is its behaviour documented, and perhaps an instance of a more general structure?