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

\homework{Databases}

\begin{document}
\maketitle

Let $\cat{Fin}$ be the full subcategory of $\cat{Set}$ whose objects are the finite sets.
Let $F : \cat{Fin} \mto \cat{Set}$ be the inclusion functor.
Define $\cat{Dat}$ to be $F \downarrow \cat{Set}$.
Let $U : \cat{Dat} \mto \cat{Set}$ be the right projection for the comma category.

The intuition is that $\cat{Dat}$ represents the category of databases.
An object $I \xto{d} X$ represents a database of $X$ values; the $I$ represents the finite set of entries, and $d$ specifies the $X$-value of each entry.
A morphism $\langle i : I \to J, f : X \to Y, \noprf \rangle$ represents applying the computation $f$ to each entry to get a corresponding entry in the target database, where the corresponding entry is specified by $i$.
In particular, if $f$ is an identity function, then the function~$i$ shows that the entries of the source database are a subset of the entries of the target database.

\begin{exercise}
Prove that $U$ is an opfibration.
\end{exercise}

\begin{proof}
Given an object $I \xto{d} X$ and a function $f : X \to Y$, let the lifting of $Y$ be $I \xto{d \cocomp f} Y$ and the lifting of $f$ be $\langle \id, f, \noprf \rangle$.
To prove $\langle \id, f, \noprf \rangle$ is opcartesian, suppose there is a morphism $\langle i, f', \noprf \rangle : (I \xto{d} X) \mto (I' \xto{d'} X')$ and a function $g : Y \to X'$ such that $f \cocomp g$ equals $f'$.
Then $\langle i, g, \noprf \rangle$ is a lifting of $g$ with the property that $\langle \id, f, \noprf \rangle \cocomp \langle i, g, \noprf \rangle$ equals $\langle i, f', \noprf \rangle$.
For uniqueness, suppose $\langle i', g', \noprf \rangle$ is also a lifting of $g$ with the property that $\langle \id, f, \noprf \rangle \cocomp \langle i', g', \noprf \rangle$ equals $\langle i, f', \noprf \rangle$.
To be a lifting of $g$, $g'$ must equal $g$, and for the equality to hold, $\id \cocomp i'$ must equal $i$, which implies $i'$ equals $i$.
Thus, $\langle i', g', \noprf \rangle$ equals $\langle i, g, \noprf \rangle$.
\end{proof}

\end{document}