Solution (source code)

= Solution

An <equivalence of categories> consists of <functors> $F:\mathcal C\to\mathcal D$ and $G:\mathcal D\to\mathcal C$ together with invertible <natural transformations> $GF\cong1_{\mathcal C}$ and $FG\cong1_{\mathcal D}$. A strict <isomorphism of categories> instead requires a <functor> with an inverse whose composites are literally identity <functors>.

First suppose $F$ belongs to an <equivalence of categories>. The isomorphisms $FGD\cong D$ give <essential surjectivity>. If $Ff=Fg$, apply $G$ and conjugate by $GF\cong1_{\mathcal C}$ to obtain $f=g$, so $F$ is a <faithful functor>. Similarly $G$ is a <faithful functor>. Writing $\alpha:GF\xrightarrow{\sim}1_{\mathcal C}$, any $h:FA\to FB$ has a preimage
$$
f=\alpha_B\,G(h)\,\alpha_A^{-1}.
$$
Indeed <naturality> of $\alpha$ gives $GF(f)=G(h)$, and faithfulness of $G$ gives $F(f)=h$. Thus $F$ is a <full and faithful functor>.

Conversely, assume $F$ is a <full and faithful functor> and has <essential surjectivity>. Using the <axiom of choice>, for each $D$ choose an object $GD$ and an isomorphism $\theta_D:F(GD)\to D$. Define $G$ on a <morphism> $h:D\to E$ by the unique lift
$$
F(Gh)=\theta_E^{-1}h\theta_D.
$$
The <full and faithful functor> property makes $G$ preserve identities and composition, and makes $\theta:FG\cong1_{\mathcal D}$ a <natural transformation>. For $A\in\mathcal C$, lift $\theta_{FA}:FGFA\to FA$ uniquely to $\alpha_A:GFA\to A$. Lifting its inverse shows that $\alpha_A$ is invertible. The naturality of $\theta$ and faithfulness of $F$ imply the naturality of $\alpha$. This proves
$$
\boxed{F\text{ is an equivalence}\iff F\text{ is full, faithful and essentially surjective}.}
$$
For large <categories>, this choice argument is understood in a fixed universe, or with the corresponding class-choice convention; ordinary set-sized <axiom of choice> suffices for <small categories>.

For the <category of partial functions>, let $X_+=X\amalg\{*\}$, with a tagged new element as basepoint. Send a <partial function> $f:X\rightharpoonup Y$ to the basepoint-preserving total <function>
$$
f_+(x)=\begin{cases}f(x),&x\in\operatorname{dom}f,\\ *,&x\notin\operatorname{dom}f,\end{cases}
\qquad f_+(*)=*.
$$
Undefined composition is sent to the basepoint, so this is a <functor> $(-)_+:\mathbf{Part}\to\mathbf{Set}_*$. Restriction away from the basepoint recovers each <partial function> uniquely; hence it is a <full and faithful functor>. Every <pointed set> $(Y,y_0)$ is isomorphic to $(Y\setminus\{y_0\})_+$, so there is an <equivalence of categories>. This particular equivalence can also be constructed explicitly, without choice, by deleting and adjoining the basepoint.

These actual <categories> are \b[equivalent but not isomorphic]. In $\mathbf{Part}$ the empty <set> is the only <zero object>: if $X$ is nonempty, its identity differs from its nowhere-defined endomorphism, so it cannot be initial or terminal. In $\mathbf{Set}_*$ every singleton <pointed set> is a <zero object>, and distinct singleton underlying <sets> give distinct objects. An <isomorphism of categories> is a bijection on objects preserving <zero objects>; it cannot take one such object onto several. This uses the categories of all actual <sets>, as in the paper, rather than chosen <skeletal categories> of representatives.

A <skeletal category> has no distinct isomorphic objects. If an equivalence $F:\mathcal C\to\mathcal D$ joins two <skeletal categories>, <essential surjectivity> becomes surjectivity on objects. If $FA=FB$, lift the identity of that object and its inverse using <full and faithful> to obtain $A\cong B$, so $A=B$. Thus $F$ is bijective on objects and on every hom-set. Its inverse on objects and <morphisms> is a strictly inverse <functor>, proving that it is an <isomorphism of categories>.

Under the <axiom of choice>, choose one object from each isomorphism class of a <small category>. The full <subcategory> on those objects is a <skeleton of a category>, and its inclusion is a <full and faithful functor> with <essential surjectivity>, hence an <equivalence of categories>.

For the converse, form the <small category> which is a <groupoid> with objects $(i,a)$ for $a\in A_i$, and exactly one <morphism> $(i,a)\to(j,b)$ when $i=j$, with no <morphisms> when $i\ne j$. Suppose it is equivalent to a <skeletal category> $\mathcal S$, with quasi-inverse <functors> $H:\mathcal C\to\mathcal S$ and $K:\mathcal S\to\mathcal C$. For each $i$, the objects $H(i,a)$ for $a\in A_i$ are isomorphic, hence all equal to a uniquely determined $s_i$. The isomorphism $KH(i,a)\cong(i,a)$ ensures that $K(s_i)=(i,a_i)$ for some $a_i\in A_i$. The rule $i\mapsto a_i$ is a choice function. In particular, no representative in $A_i$ had to be chosen to define $s_i$, since it is unique. Consequently
$$
\boxed{\text{Every small category has a skeletal equivalent}\iff\text{the axiom of choice}.}
$$