6 August 2019, 7pm
I realized how types of structured sets can be thought of as faithful copresheaves.
Let $F$ be a type of structured sets, e.g. the type of groups or the type of topological spaces. For every structured set $A$ in $F$ we have the underlying set $F(A)$ of $A$. And for every structure-preserving map $f : A \to B$ between structured sets in $F$, we have the underlying map $F(f)$ of $f$.
Note that $F(A)$ is not $A$ because $A$ has additional structure. In fact it is possible for two structured sets to be distinct and yet have the same underlying set, since they may differ in structure while having the same elements. In contrast, $F(f)$ does not have any additional structure on it, compared to $f$, besides the additional structure on its domain and codomain; this means that $f$ is uniquely determined by $F(f)$, $A$ and $B$. We may therefore think of $f$ as the ordered triple $(F(f), A, B)$.
Now, two conditions it's reasonable to expect structure-preserving maps to satisfy are as follows:
For any two structure-preserving maps $f : A \to B$, $g : B \to C$, the composition $(F(g) \circ F(f), A, C)$ is also structure-preserving.
For every structured set $A$, the identity map $(1_A, A, A)$ is structure-preserving.
It is easy to prove that if these two conditions are satisfied, then by taking the structured sets in $F$ as objects and the structure-preserving maps between structured sets in $F$ as morphisms, we obtain a category, and then $F$ is a faithful copresheaf on this category.
Of course, we can replace $\mathsf{Set}$ with an arbitrary category $X$ to get a notion of “structured $X$-object”; a type of structured $X$-objects is a faithful functor into $X$.
This also gives us a way to see faithfulness as a natural notion. Faithfulness of a functor $F : X \to Y$ means that the morphisms in $X$ can be thought of as just structure-preserving morphisms between structured $Y$-objects, without any additional structure on the morphisms themselves as opposed to their domains and codomains.
