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

\homework{Existentials}

\begin{document}
\maketitle

\begin{exercise}
Prove that the existential subtyping relation for a category~$\cat{Bnd}$ and functor $\cat{Bnd} \mto \cat{Prost}$ is always a preorder.
Be detailed in your proof.
\end{exercise}

\begin{proof}
Given an existential type $\exists \Gamma.\; \tau$, we can prove reflexivity using the identity morphism $\id_\Gamma : \Gamma \mto \Gamma$, since $\tau \leq \tau[\id_\Gamma]$ holds due to the fact that functors preserve identities, so $\tau[\id_\Gamma]$ must equal $\tau$, and $\leq$ is assumed to be reflexive.

For transitivity, suppose we know $\exists \Gamma_1.\; \tau_1 \leq \exists \Gamma_2.\; \tau_2 \leq \exists \Gamma_3.\; \tau_3$ holds.
This is possible only if there exist $\theta : \Gamma_2 \mto \Gamma_1$ and $\theta' : \Gamma_3 \mto \Gamma_2$ such that $\tau_1 \leq \tau_2[\theta]$ and $\tau_2 \leq \tau_3[\theta']$ hold.
We demonstrate that $\exists \Gamma_1.\; \tau_1 \leq \exists \Gamma_3.\; \tau_3$ holds by using the morphism $\theta' \cocomp \theta : \Gamma_3 \mto \Gamma_1$.
$\tau_1 \leq \tau_2[\theta]$ holds by assumption; $\tau_2[\theta] \leq \tau_3[\theta'][\theta]$ holds because $\tau_2 \leq \tau_3[\theta']$ holds by assumption and $[\theta]$ is a morphism of $\cat{Prost}$ and therefore preserves subtypings; and $\tau_3[\theta'][\theta]$ equals $\tau_3[\theta' \cocomp \theta]$ because functors are distributive.
So, $\tau_1 \leq \tau_3[\theta' \cocomp \theta]$ holds due to the assumed transitivity of $\leq$.
This proves that $\exists \Gamma_1.\; \tau_1$ is a subtype of $\exists \Gamma_3.\; \tau_3$.
\end{proof}

\begin{exercise}
Prove that $\cat{Prost}$ has an $(\alg{E}, \alg{M})$ factorization structure, where $\alg{E}$ is the set of all epimorphisms and $\alg{M}$ is the set of all \emph{initial} mono-sources.
A $\cat{Prost}$-source $(\ob{C} \xmto{\mo{f}_i} \ob{C}_i)_{i : I}$ is initial when for all pairs $c_1, c_2 : C$, if $\forall i : I.\; f_i(c_1) \leq f_i(c_2)$ holds then $c_1 \leq c_2$ holds as well (note that the reverse implication always holds because each function must be relation-preserving).
You may assume that $\cat{Set}$ has an epi-mono factorization structure, that a morphism in $\cat{Prost}$ is an epimorphism iff its underlying function is an epimorphism, and that a source in $\cat{Prost}$ is a mono-source iff its underlying source is a mono-source.
\end{exercise}

\begin{proof}
First, we demonstrate that $\cat{Prost}$ has epi-initial-mono factorizations.
Given a source $(\mo{f}_i : \ob{R} \mto \ob{R}_i)_{i \in I}$ let $\langle e : R \mto X, (m_i : X \mto R_i)_{i \in I} \rangle$ be the epi-mono factorization in $\cat{Set}$.
Then, define $x \sqsubseteq x'$ to be $\forall i.\; m_i(x) \leq m_i(x')$ (which is a preorder because each $\ob{R}_i$ defines a preorder).
This makes the source $(\mo{m}_i : \langle X, \sqsubseteq \rangle \mto \ob{R}_i)$ initial by definition (and clearly each $\mo{m}_i$ is relation-preserving); it is also mono because its underlying source is mono.
Next, suppose $r \leq r'$ holds in $\ob{R}$, then for any $i \in I$ we know $m_i(e(r)) \leq m_i(e(r'))$ holds, so $e(r) \sqsubseteq e(r')$ holds by definition of $\sqsubseteq$.
Thus, $\mo{e} : \ob{R} \mto \langle X, \sqsubseteq \rangle$ is a morphism in $\cat{Prost}$, and it is epi since its underlying function is epi.
This makes $\langle \mo{e}, (\mo{m}_i)_{i \in I} \rangle$ an epi-initial-mono factorization of $(\mo{f}_i)_{i \in I}$.

Second, we demonstrate that $\cat{Prost}$ has unique epi-initial-mono diagonalizations.
Suppose we have that $\mo{e} \cocomp \mo{g}_i$ equals $\mo{f} \cocomp \mo{m}_i$ in $\cat{Prost}$ for all $i \in I$, where $\mo{e}$ is epi and $(\mo{m}_i)_{i \in I}$ is initial mono.
That implies we also have that $e \cocomp g_i$ equals $f \cocomp m_i$ in $\cat{Set}$ for all $i \in I$, where $e$ is epi and $(m_i)_{i \in I}$ is mono.
Because $\cat{Set}$ has unique epi-mono diagonalizations, there exists a unique function $d$ such that $e \cocomp d$ equals $f$ and $d \cocomp m_i$ equals $g_i$ for all $i \in I$.
Thus, the only thing we need to do is prove that $d$ is relation-preserving.
Suppose we have that $x \leq x'$ holds in the codomain of $\mo{e}$.
Then $m_i(d(x)) \leq m_i(d(x'))$ holds for all $i \in I$ because the left equals $f_i(x)$ and the right equals $f_i(x')$ and each $f_i$ is relation-preserving.
Because $(\mo{m}_i)_{i \in I}$ is initial, this implies $d(x) \leq d(x')$ also holds.
Thus, there exists a unique morphism $\mo{d}$ in $\cat{Prost}$ such that $\mo{e} \cocomp \mo{d}$ equals $\mo{f}$ and $\mo{d} \cocomp \mo{m}_i$ equals $\mo{g}_i$ for all $i \in I$.
\end{proof}

\end{document}