I am reading notes on categorical logic by Awodey and Bauer. This is one of its beginner exercises:
I claim that this is not a category. Let us consider some $R \subseteq A \times B$, which has as its domain $A' \subset A$ and its codomain $B' \subset B$. Then, $R \subseteq A' \times B'$, which means that $R : A \to B$ and $R : A' \to B'$. This violates the following axiom of category theory, namely that morphisms have a unique domain and codomain:
Hence, $\mathsf{Rel}$ is not a category.
Am I correct? Thank you for your input! :)
You are not correct.
Your thought is analogous to the thought:
But technically speaking when we restrict domains and codomains we are actually talking about different functions: it is an (common) abuse of notation to keep "$f$" for both the functions $\Bbb R\to[0,\infty)$ and $\Bbb R\to\Bbb R$, even if they are morally essentially the same thing.
Back to categories. Yes, $R\subseteq A'\times B'$ is true. Yes, there would then be a related arrow $R':A'\to B'$. You would even get a commutative diagram: $$\begin{align}&A'\overset{R'}{\longrightarrow}&B'\\&\downarrow&\downarrow\\&A\overset{R}{\longrightarrow}&B\end{align}$$
In $\mathsf{Rel}$. But $R'$ is not the same thing as the arrow $R$. The arrow $R$ and the relation $R$ are not the same thing, so it is even an abuse of notation to call them both by the same name. While a relation $R$ might not have a well-defined domain or codomain in the sense that any relation can fit as a subset of a larger set, the data of the arrow is not the same as the data of $R$, the data of the arrow incorporates $A,B$ also.
This leads to the thorny question of how we should actually encode the data of categories on a set-theoretic level. That's not a question I'm qualified to answer, and there are many different viewpoints and common methods. It is very often I see in category theoretic texts the following line: "By passing to a higher universe, ..." and the moral of that story (for me) is, for most people's intents and purposes, it really doesn't matter how the data is encoded. Just get on with things and do category theory!