\documentclass{article}
\input{packages}
\input{def}

\homework{Proofs}

\begin{document}
\maketitle

\begin{exercise}
Let $\mo{trans} : \langle \{a,b,c\}, \{\langle a, b \rangle, \langle b, c \rangle\} \rangle \mto \langle \{a, b, c\}, \{\langle a, b \rangle, \langle b, c \rangle, \langle a, c \rangle\} \rangle$ be a morphism of $\cat{Rel}(2)$ whose underlying function is the identity.
Call its domain $\ob{P}$ and its codomain $\ob{R}$.
Describe, in standard set-theoretic terms, what the pushout of the following is, for any object $\ob{X}$ and morphism $\mo{f} : \ob{P} \mto \ob{X}$:
\begin{center}
\begin{tikzpicture}
\node(p) at (-1,1) {$\ob{P}$};
\node(r) at (1,1) {$\ob{R}$};
\node(x) at (-1,-1) {$\ob{X}$};
\draw[->] (p) -- node[above]{$\mo{trans}$} (r);
\draw[->] (p) -- node[left]{$\mo{f}$} (x);
\end{tikzpicture}
\end{center}
Prove that your description is actually a pushout.
\end{exercise}

\begin{proof}
Let $\ob{Y} = \langle X, R_\ob{X} \cup \{\langle f(a), f(c) \rangle\} \rangle$.
Let $\kappa_\ob{X}$ be the identity function, which is obviously relation preserving.
Let $\kappa_\ob{R}$ be the underlying function of $\mo{f}$, which is relation preserving because $\mo{f}$ is relation preserving and $f(a)$ is related to $f(c)$ in $\ob{Y}$ by definition.

Suppose there is an object $\ob{Z}$ with morphisms $\mo{g} : \ob{X} \mto \ob{Z}$ and $\mo{h} : \ob{R} \mto \ob{Z}$ such that $\mo{f} \cocomp \mo{g}$ equals $\mo{trans} \cocomp \mo{h}$.
Then, for $\kappa_\ob{X} \cocomp [\mo{g}, \mo{h}]$ to equal $\mo{g}$, the underlying function of $[\mo{g}, \mo{h}]$ must be the underlying function of $\mo{g}$ because the underlying function of $\kappa_\ob{X}$ is the identity, which guarantees uniqueness of $[\mo{g}, \mo{h}]$.
This also implies that $\kappa_\ob{R} \cocomp [\mo{g}, \mo{h}]$ equals $\mo{h}$, since the underlying function of $\kappa_\ob{R}$ is $f$, and $\mo{f} \cocomp \mo{g}$ equaling $\mo{trans} \cocomp \mo{h}$ implies $f \cocomp g$ equals $h$.
For existence, we must prove that $g$ is relation-preserving from $\ob{Y}$ to $\ob{Z}$ and that $\kappa_\ob{R} \cocomp g$ equals $h$.
Given two elements related in $\ob{Y}$, by the definition of the relation of $\ob{Y}$, they must either be related in $\ob{X}$ or they must be the pair $\langle f(a), f(c) \rangle$.
The former case is preserved because $\mo{g}$ is relation-preserving from $\ob{X}$ to $\ob{Z}$.
For the latter case, $g(f(a))$ equals $h(a)$ and $g(f(c))$ equals $h(c)$, and $a$ and $c$ are related in $\ob{R}$, so $\mo{h}$ being relation-preserving implies that $g(f(a))$ must be related to $g(f(c))$ in $\ob{Z}$.
\end{proof}

\end{document}