[proofplan] We prove the principle by interpreting the original statement $P$ inside the opposite category of an arbitrary small category $\mathcal C$. The opposite category has the same objects and the same underlying arrows, but every morphism is read in the reverse direction and composition is reversed; in particular, smallness is preserved. After defining dualization recursively on the categorical language, a structural induction on formulas shows that truth of $P$ in $\mathcal C^{\mathrm{op}}$ is exactly truth of $P^{\mathrm{op}}$ in $\mathcal C$. Since $\mathcal C^{\mathrm{op}}$ is a small category and $P$ is valid in every small category, $P$ holds in $\mathcal C^{\mathrm{op}}$, hence $P^{\mathrm{op}}$ holds in $\mathcal C$. [/proofplan] [step:Construct the opposite category of an arbitrary small category] Let $\mathcal C$ be an arbitrary small category. Define the opposite category $\mathcal C^{\mathrm{op}}$ as follows. The objects of $\mathcal C^{\mathrm{op}}$ are the objects of $\mathcal C$. For objects $A$ and $B$, a morphism $A \to B$ in $\mathcal C^{\mathrm{op}}$ is, by definition, a morphism $B \to A$ in $\mathcal C$. Since $\mathcal C$ is small, its collection of objects and its collection of morphisms are sets; the same collections underlie $\mathcal C^{\mathrm{op}}$, so $\mathcal C^{\mathrm{op}}$ is also small once the category axioms are verified. For each morphism $f: A \to B$ in $\mathcal C$, write \begin{align*} f^{\mathrm{op}}: B &\to A \end{align*} for the corresponding morphism in $\mathcal C^{\mathrm{op}}$. The identity morphism on an object $A$ in $\mathcal C^{\mathrm{op}}$ is the same underlying morphism $\operatorname{id}_A: A \to A$ from $\mathcal C$. If $f: A \to B$ and $g: B \to C$ are morphisms in $\mathcal C$, then the corresponding morphisms in $\mathcal C^{\mathrm{op}}$ are \begin{align*} g^{\mathrm{op}}: C &\to B, & f^{\mathrm{op}}: B &\to A . \end{align*} Their composite in $\mathcal C^{\mathrm{op}}$ is defined by \begin{align*} f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} g^{\mathrm{op}} &:= (g \circ_{\mathcal C} f)^{\mathrm{op}} . \end{align*} The identity laws in $\mathcal C^{\mathrm{op}}$ follow from the identity laws in $\mathcal C$. Indeed, if $f: A \to B$ is a morphism in $\mathcal C$, then $f^{\mathrm{op}}: B \to A$ is a morphism in $\mathcal C^{\mathrm{op}}$, and \begin{align*} f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} \operatorname{id}_B &= (\operatorname{id}_B \circ_{\mathcal C} f)^{\mathrm{op}} = f^{\mathrm{op}}, \\ \operatorname{id}_A \circ_{\mathcal C^{\mathrm{op}}} f^{\mathrm{op}} &= (f \circ_{\mathcal C} \operatorname{id}_A)^{\mathrm{op}} = f^{\mathrm{op}}. \end{align*} Associativity also follows from associativity in $\mathcal C$. Let $f: A \to B$, $g: B \to C$, and $h: C \to D$ be composable morphisms in $\mathcal C$. Then $h^{\mathrm{op}}: D \to C$, $g^{\mathrm{op}}: C \to B$, and $f^{\mathrm{op}}: B \to A$ are composable in $\mathcal C^{\mathrm{op}}$, and the two defined triple composites are \begin{align*} f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} \left(g^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} h^{\mathrm{op}}\right) &= f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} (h \circ_{\mathcal C} g)^{\mathrm{op}} \\ &= ((h \circ_{\mathcal C} g) \circ_{\mathcal C} f)^{\mathrm{op}}, \\ \left(f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} g^{\mathrm{op}}\right) \circ_{\mathcal C^{\mathrm{op}}} h^{\mathrm{op}} &= (g \circ_{\mathcal C} f)^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} h^{\mathrm{op}} \\ &= (h \circ_{\mathcal C} (g \circ_{\mathcal C} f))^{\mathrm{op}}. \end{align*} Since associativity in $\mathcal C$ gives \begin{align*} (h \circ_{\mathcal C} g) \circ_{\mathcal C} f &= h \circ_{\mathcal C} (g \circ_{\mathcal C} f), \end{align*} the two triple composites in $\mathcal C^{\mathrm{op}}$ are equal. Thus $\mathcal C^{\mathrm{op}}$ is a small category. [/step] [step:Relate formulas in $\mathcal C^{\mathrm{op}}$ to dual formulas in $\mathcal C$] We first define the dual formula $\varphi^{\mathrm{op}}$ recursively. For an atomic type assertion saying that a morphism variable has source $A$ and target $B$, the dual assertion says that the same morphism variable has source $B$ and target $A$. Identity assertions are unchanged, since $\operatorname{id}_A$ has the same source and target. An atomic composition assertion $h = g \circ f$, where $f: A \to B$, $g: B \to C$, and $h: A \to C$, is dualized to the assertion $h = f \circ g$ with all arrows read in the reversed types. Atomic equality assertions between parallel morphisms are unchanged. The operations $\neg$, $\wedge$, $\vee$, $\implies$, universal quantification, and existential quantification commute with dualization, except that each quantified morphism variable of type $A \to B$ is assigned the reversed type $B \to A$. With this recursive definition, we claim that for every categorical formula $\varphi$, every assignment of its object variables to objects of $\mathcal C$, and every assignment of its morphism variables to morphisms whose types match the interpretation in $\mathcal C^{\mathrm{op}}$, the following equivalence holds: \begin{align*} \mathcal C^{\mathrm{op}} \models \varphi \quad \Longleftrightarrow \quad \mathcal C \models \varphi^{\mathrm{op}} . \end{align*} This is proved by structural induction on the recursively defined formula $\varphi$. For atomic source-target assertions, the equivalence is exactly the definition of morphisms in $\mathcal C^{\mathrm{op}}$: an arrow $A \to B$ in $\mathcal C^{\mathrm{op}}$ is an arrow $B \to A$ in $\mathcal C$. For identity assertions, the same morphism $\operatorname{id}_A$ serves as the identity in both categories, with the same object $A$. For composition assertions, the defining rule \begin{align*} f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} g^{\mathrm{op}} &= (g \circ_{\mathcal C} f)^{\mathrm{op}} \end{align*} says precisely that composition in the opposite category translates to composition in the reversed order in $\mathcal C$. Equalities of morphisms are preserved because $\mathcal C$ and $\mathcal C^{\mathrm{op}}$ use the same underlying morphisms. Boolean connectives preserve the equivalence by the induction hypothesis. Quantifiers preserve it because $\mathcal C$ and $\mathcal C^{\mathrm{op}}$ have the same objects and the same underlying morphisms, with only the source and target directions reversed. Therefore the equivalence holds for every formula, and in particular for every sentence $P$: \begin{align*} \mathcal C^{\mathrm{op}} \models P \quad \Longleftrightarrow \quad \mathcal C \models P^{\mathrm{op}} . \end{align*} [guided] The point of this step is to make precise the phrase “translate back from the opposite category.” Let $\varphi$ be a categorical formula in the first-order categorical language whose variables are typed as object variables or as morphism variables with specified source and target object variables. Define $\varphi^{\mathrm{op}}$ recursively as follows: reverse the source and target in each atomic morphism-typing assertion; leave identity and equality assertions unchanged except for the reversed ambient types; replace each atomic composition assertion $h = g \circ f$ by the reversed-order assertion $h = f \circ g$ with all morphism types reversed; commute dualization with $\neg$, $\wedge$, $\vee$, $\implies$, $\forall$, and $\exists$, while reversing the type of every quantified morphism variable. Fix an assignment of each object variable of $\varphi$ to an object of $\mathcal C$, and fix an assignment of each morphism variable of $\varphi$ to an underlying morphism whose source and target match the interpretation in $\mathcal C^{\mathrm{op}}$. We prove, by structural induction on this recursive construction of $\varphi$, that \begin{align*} \mathcal C^{\mathrm{op}} \models \varphi \quad \Longleftrightarrow \quad \mathcal C \models \varphi^{\mathrm{op}} . \end{align*} First consider the atomic formulas. If the atomic assertion says that a morphism has type $A \to B$ in $\mathcal C^{\mathrm{op}}$, then the definition of $\mathcal C^{\mathrm{op}}$ says exactly that the same underlying morphism has type $B \to A$ in $\mathcal C$. This is precisely the dual source-target assertion. If the atomic assertion is an identity assertion, the same morphism $\operatorname{id}_A: A \to A$ is the identity on $A$ in both $\mathcal C$ and $\mathcal C^{\mathrm{op}}$, so the assertion is unchanged after dualising. If the atomic assertion is a composition assertion, then for morphisms $f: A \to B$ and $g: B \to C$ in $\mathcal C$ the defining rule \begin{align*} f^{\mathrm{op}} \circ_{\mathcal C^{\mathrm{op}}} g^{\mathrm{op}} &= (g \circ_{\mathcal C} f)^{\mathrm{op}} \end{align*} shows that composition in $\mathcal C^{\mathrm{op}}$ translates to composition in the reversed order in $\mathcal C$. If the atomic assertion is equality of morphisms, then equality is preserved because $\mathcal C$ and $\mathcal C^{\mathrm{op}}$ have the same underlying morphisms; only their source and target directions are read oppositely. Now assume the equivalence has been proved for formulas $\psi$ and $\theta$. For negation, conjunction, disjunction, and implication, the truth values of the compound formulas are determined by the truth values of their constituent formulas, so the induction hypothesis gives the corresponding equivalence for $\neg \psi$, $\psi \wedge \theta$, $\psi \vee \theta$, and $\psi \implies \theta$. For quantifiers, the ranges are also matched: object quantifiers range over the same objects in $\mathcal C$ and $\mathcal C^{\mathrm{op}}$, and morphism quantifiers range over the same underlying arrows with source and target reversed. Therefore existential and universal quantifiers preserve the equivalence under the same assignment convention. Thus the structural induction proves that for every categorical formula $\varphi$, \begin{align*} \mathcal C^{\mathrm{op}} \models \varphi \quad \Longleftrightarrow \quad \mathcal C \models \varphi^{\mathrm{op}} . \end{align*} In particular, when $P$ is a sentence, there are no free variables or assignments left to specify, and we obtain \begin{align*} \mathcal C^{\mathrm{op}} \models P \quad \Longleftrightarrow \quad \mathcal C \models P^{\mathrm{op}} . \end{align*} [/guided] [/step] [step:Apply validity of the original statement to the opposite small category] Assume $P$ is true in every small category. Since $\mathcal C^{\mathrm{op}}$ is a small category by the first step, the hypothesis gives \begin{align*} \mathcal C^{\mathrm{op}} \models P . \end{align*} By the formula-translation equivalence from the second step, \begin{align*} \mathcal C \models P^{\mathrm{op}} . \end{align*} Because $\mathcal C$ was an arbitrary small category, $P^{\mathrm{op}}$ is true in every small category. This proves the duality principle. [/step]