\(F:\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)\)を対象とする。[006A]よりレトラクト\((\sum _{G:\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)}F\cong G)\triangleleft (\sum _{G:\mathord {\textnormal {\textsf {Fun}}}(C,D)}\lbrace t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\mid \forall _{x:C}\mathord {\textnormal {\textsf {IsIso}}}(t(x))\rbrace )\)を得る。後者が可縮であることを示すには、[006B]より

\(\sum _{G_{0}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}}\sum _{G_{1}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(G_{0}(x_{1}),G_{0}(x_{2}))}\lbrace t:\prod _{x:C}F(x)\cong G_{0}(x)\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G_{1}(f)\circ t(x_{1})=t(x_{2})\circ F(f)\rbrace \) が可縮であることを示せばよい。\(\sum _{G_{0}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}}\prod _{x:C}F(x)\cong G_{0}(x)\)の部分は\(\prod _{x:C}\sum _{y:D}F(x)\cong y\)のレトラクトなので、[0029]と\(D\)が圏であるという仮定から可縮である。よって、件の型は\(\lbrace G_{1}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(F(x_{1}),F(x_{2}))\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G_{1}(f)\circ \mathord {\textnormal {\textsf {id}}}=\mathord {\textnormal {\textsf {id}}}\circ F(f)\rbrace \)のレトラクトである。この型はさらに\(\prod _{x_{1},x_{2}:C}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\lbrace g:\mathord {\textnormal {\textsf {Map}}}(F(x_{1}),F(x_{2}))\mid g=F(f)\rbrace \)のレトラクトであるが、これは[0029]と[0026]より可縮である。