\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}

\end{document}