Category of Binary Relations is Isomorphic to its Dual Category I'm working on learning some category theory and the book claims that $\mathbf{Rel} \stackrel{\sim}{=} \mathbf{Rel}^\mathsf{op}$ where $\mathbf{Rel}$ is the category of binary relations. The functor that is supposed to show this is $F : \mathcal{Rel} \rightarrow \mathcal{Rel}^\mathsf{op}$ where it takes objects to themselves and relations to its opposite relation. That is, for an arrow $f$ in $\mathbf{Rel}$, $f \subseteq A \times B$ is mapped to $f^\mathsf{op} := \left\{ <b, a> \in B \times A | <a, b> \in f \right\}$.
My problem is I don't see how this makes it past one of the axioms of being a functor, given in the book as
$F(f: A \rightarrow B) = F(f):F(A) \rightarrow F(B)$
First, I really just don't think I understand how I'm supposed to understand this part of the definition. Am I supposed to be taking the left side of the equality as mapping the arrow, and the right side as asserting that the arrow it is mapped to has as domain and codomain the functor applied to the domain and codomain of the original arrow? 
It seems like on this current example, it doesn't even give us the arrow $f^\mathsf{op}$ because it doesn't exchange the domain and codomain. And there seems to be no way of doing this exchange by mapping the objects to different objects.
In short, I'm probably hopelessly confused. How is it that this is a functor? And how am I supposed to understand this part of the definition of a functor? It seems wishy washy. 
Thank you for any help you may provide.
 A: Also see my comment.
Based on category $\mathcal{C}$ we have category $\mathcal{C}^{op}$
determined by:
1) $\mathcal{C}^{op}$ has the same set of objects as the original
category $\mathcal{C}$
2) For every pair of objects $a,b$ we have $\mathcal{C}^{op}\left(a,b\right)=\mathcal{C}\left(b,a\right)$
3) If we denote the composition on $\mathcal{C}$ by $\circ$ and
the composition on $\mathcal{C}^{op}$ by $\circ^{op}$ then $f\circ^{op}g$
is defined iff $g\circ f$ is defined and this by $f\circ^{op}g:=g\circ f$
If $g\in\mathcal{C}^{op}\left(a,b\right)$ and $f\in\mathcal{C}^{op}\left(b,c\right)$
then $f\circ^{op}g$ should be defined, wich is indeed the case since
$g\in\mathcal{C}\left(b,a\right)\wedge f\in\mathcal{C}\left(c,b\right)$
tells us that $g\circ f$ is defined.
Here $f\circ^{op}g=g\circ f\in\mathcal{C}\left(c,a\right)=\mathcal{C}^{op}\left(a,c\right)$
as we would expect.
You could say that $\mathcal{C}^{op}$ has exactly the same objects and arrows
as $\mathcal{C}$ and the only thing different is the composition. Consequently domain and codomain of an arrow interchange.
Observing an arrow $f$ then we simply must ask ourselves the question
in what context we are observing: is it an arrow of $\mathcal{C}$ here, or an arrow
of $\mathcal{C}^{op}$?
Functor $F:\mathbf{Rel}\rightarrow\mathbf{Rel}^{op}$ as described
in your question sends arrow $f\in\mathbf{Rel}\left(A,B\right)$ to
an arrow $f^{op}$ that belongs to $\mathbf{Rel}\left(B,A\right)=\mathbf{Rel}^{op}\left(A,B\right)=\mathbf{Rel}^{op}\left(F\left(A\right),F\left(B\right)\right)$
as it should be. 
Quite often arrow $f$ in $\mathcal{C}$ is denoted as $f^{op}$ if
it is looked at as an arrow in $\mathcal{C}^{op}$. This is not really
necessary, can clear up things (it tells us what context we are working in) but can also cause confusion. For instance
the arrow $F\left(f\right)$ in your question is also denoted as $f^{op}$
but it is not this $f$ in the other context. If it should be then
we would have $f^{op}\in\mathbf{Rel}\left(A,B\right)=\mathbf{Rel}^{op}\left(B,A\right)$
which is not the case. 
