I'm tasked with proving (or disproving) $Rel \cong Rel^{op}$. I just want to double-check my reasoning. Also keep in mind this is mostly a sketch proof - I'm just showing my overall thinking, and not looking to display formality, at least in this post. But if there are glaring errors, yeah, I'd like to deal with those.
So first we consider the categories $Rel, Rel^{op}$. Objects in each are sets, and arrows are relations. Specifically, $R$ is an arrow $R : A \rightarrow B$ defined by $R(A) = \{ (a,b) \in A \times B \;\;\; | \;\;\; a \; R \; b \}$
A noteworthy tidbit is that $Rel = Rel^{op}$. In the respect of the objects in each, that much is obvious; less trivial is the arrows. We take note: if $R : A \rightarrow B$, we can define an arrow by the converse relation $S : B \rightarrow A$.
Since there exists only one arrow in $Hom_{Rel}(A,B)$ corresponding to a given relation $R$ (things either are or are not related), then any such arrow $A \rightarrow B$ is unique for that $R$. Therefore, similarly, the arrow $A \rightarrow A$ is unique, for a fixed relation on $A$, and therefore $S \circ R = 1_A$ and $R \circ S = 1_B$.
(Note of contention: I'm not sure if I have to prove from the definitions of relations that the composition gives the identity. Personally I like the "uniqueness" argument, even if my wording is a bit murky, but I'm not sure if that's good enough. Point being, to any relation R from A to B, we can find an inverse relation S, and their composition gives the identity.)
In the dual category $Rel^{op}$, arrows reverse. But we have the uniqueness of arrows, so $R$ in $Rel$ becomes $S$ in $Rel^{op}$ (using our above definitions for arrows). This generalizes across all the arrows - each arrow becomes its inverse, and since all arrows are invertible, we get the original set of arrows - and (I think) suffices to show $Rel = Rel^{op}$.
Finally, regarding isomorphism, it is trivial. Assuming all the above is correct thus far, then we consider the category of small categories, i.e. $Cat$. Since it's a category itself and $Rel$ is a category there, it follows there is an identity functor to itself. Identity functors are trivially isomorphisms, and since $Rel = Rel^{op}$, $Rel \cong Rel$ implies $Rel \cong Rel^{op}.$
I'm very much not confident where relations are concerned, and the same for functors since they're new to me. Informality aside, though, is this a sufficient argument?
For the record, the idea of $Rel$ being self-dual came from Wikipedia:
https://en.wikipedia.org/wiki/Category_of_relations
A morphism in Rel is a relation, and the corresponding morphism in the opposite category to Rel has arrows reversed, just the converse relation. Thus Rel contains its opposite and is self-dual.
Your situation follows from the following general claim by showing that converse is an involution.
Indeed, by definition, if $f : A → B ∈ $ then $f ˘ : B → A ∈ $ which is the same as saying $f ˘ : A → B ∈ ᵒᵖ$. Hence, the functor $\_˘$ serves as a natural candidate to witness the isomorphism.
That it is an isomorphism follows immediately from that fact that it is an involution.
Examples of this include: