Skeletal categories are equivalent iff they are isomorphic

Let $𝖢, 𝖣$ be skeletal categories. Then these are isomorphic iff they are equivalent, #m/thm/cat/evil i.e.

𝖢 ≅ 𝖣 ⟺ 𝖢 ≃ 𝖣 .

Proof

Suppose $𝐹 : 𝖢 ⇄ 𝖣 : 𝐺$ defines an equivalence of categories. Then there exist natural isomorphisms $𝜂 : 1 \Rightarrow 𝐹 𝐺 : 𝖢 \to 𝖢$ and $𝜖 : 1 \Rightarrow 𝐹 𝐺 : 𝖣 \to 𝖣$ , which must be identities since $𝖢$ and $𝖣$ are skeletal.

This is a lemma for the stronger Assuming choice, categories are equivalent iff they have isomorphic skeleta.

#state/tidy | #lang/en | #SemBr