(Warning: I'm writing this from memory, and don't have the reference handy)
In Categories, Allegories, Freyd and Scedrov prove a theorem
A property of categories is preserved by equivalence if and only if it can be described on a blackboard
The key feature of a blackboard, here, is that if you draw two distinct objects, they remain distinct throughout a description; you can't insist they are equal. So we might restate the theorem as
A property of categories is preserved by equivalence if and only if it does not involve equations of objects
To prove this, Freyd and Scedrov define a formal diagrammatic language whose semantics involve the existence of functors from diagram categories. For example, limits from a category $J$ are described as follows:
- Define a category $J_1$ by adjoining to $J$ a new object $L$, arrows $\hom(L,L) = \hom(L, j) = \{ * \}$
- Define a category $J_2$ by adjoining to $J_1$ a new object $M$ and arrows $\hom(M,M) = \hom(M,j) = \{ * \}$ and $\hom(L,M) = \hom(M,L) = \varnothing$
- Define a category $J_3$ by adjoining to $J_2$ a new arrow $p : M \to L$
Then, a functor $F : J \to \mathcal{C}$ has a limit if and only if:
- There exists a a functor $F_1 : J_1 \to \mathcal{C}$ extending $F$ such that
- For every functor $F_2 : J_2 \to \mathcal{C}$ extending $F_1$
- There exists a unique functor $F_3 : J_3 \to \mathcal{C}$ extending $F_2$.
In the formal version of the claimed theorem, the relevant property is that the functors between the diagram categories must be injective on objects.
An example of a property not preserved by equivalence is as follows:
- Let $J_1$ be the category of two objects and an isomorphism between them
- Let $J_2$ be the category consisting of a single object and $\hom(*, *) = \mathbb{Z}$
And map $J_1 \to J_2$ by sending the two isomorphisms to $\pm 1$. Then, a category $\mathcal{C}$ is skeletal if and only if every functor $J_1 \to \mathcal{C}$ can be extended to a functor $J_2 \to C$.
With the benefit of hindsight, I think the key idea underpinning this is the canonical model structure. In particular, consider the square
$$ \begin{matrix} J &\xrightarrow{f}& \mathcal{C}
\\ i\downarrow\ \ & & \ \ \downarrow e
\\ J' &\xrightarrow{f'} & \mathcal{C}' \end{matrix} $$
A lift, here, is a diagonal arrow $\ell : J' \to \mathcal{C}$ making the diagram commute.
Then $i$ is injective on objects if and only if, for every such diagram where $e$ is a surjective equivalence $e$, a lift exists.
Similarly, $e$ is a surjective equivalence if and only if, for every such diagram where $i$ is injective on objects, a lift exists.
The connection to the logic described above are, if $i$ is injective on objects and $e$ a surjective equivalence, then
A functor $f : J \to \mathcal{C}$ can be extended to $\ell : J' \to \mathcal{C}$ if and only if $ef : J \to \mathcal{C}'$ can be extended to $f' : J' \to \mathcal{C}'$. Furthermore, in both cases the lifts can be chosen so that they are related via $e$.
This extends to the general case, since any equivalence can be 'lifted' to a span of surjective ones; for any equivalence $e:\mathcal{C} \to \mathcal{C}'$, there is a category $\mathcal{C}''$ and surjective equivalences $e_1 : \mathcal{C}'' \to \mathcal{C}$ and $e_2 : \mathcal{C}'' \to \mathcal{C}'$ such that $e e_1 = e_2$.