関数外延性を仮定する。\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)を関手、\(s,t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\)を自然変換とすると、同値

\((s=t)\simeq (\forall _{x:C}s(x)=t(x))\) を構成できる。