CatDat

Implication Details

Claim: Given a functor whose codomain is trivial, and whose domain is inhabited, then it is right-invertible.

Proof: Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.