8.3.3.7 The Internal Hom

The internal Hom of $\mathsf{Rel}$ is the functor

\[ \mathrm{Rel}\colon \mathsf{Rel}^{\mathsf{op}}\times \mathsf{Rel}\to \mathsf{Rel} \]

defined

  • On objects by sending $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$ to the set $\mathrm{Rel}(A,B)$ of Unresolved reference of Unresolved reference.

  • On morphisms by pre/post-composition defined as in Definition 8.1.3.1.1.

Let $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$.

  1. 1.

    Adjointness. We have adjunctions

    witnessed by bijections

    \begin{align*} \mathrm{Rel}(A\times B,C) & \cong \mathrm{Rel}(A,\mathrm{Rel}(B,C)),\\ \mathrm{Rel}(A\times B,C) & \cong \mathrm{Rel}(B,\mathrm{Rel}(A,C)), \end{align*}

    natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$.

Item 1: Adjointness
Indeed, we have

\begin{align*} \mathrm{Rel}(A\times B,C) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{Sets}(A\times B\times C,\{ \mathsf{true},\mathsf{false}\} )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}(A,B\times C)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}(A,\mathrm{Rel}(B,C)), \end{align*}

and similarly for the bijection $\mathrm{Rel}(A\times B,C)\cong \mathrm{Rel}(B,\mathrm{Rel}(A,C))$.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: