CatDat

Implication Details

Claim: Given a functor whose codomain is core-connected, and whose domain is inhabited, then it is essentially surjective.

Proof: Let $F : \C \to \D$ be a functor from an inhabited category to a core-connected category. Choose any object $X \in \C$. For every $Y \in \D$ we have $Y \cong F(X)$. Thus, $F$ is essentially surjective.