\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\mathord {\textnormal {\textsf {diag}}}(A):A\to A\times A\)であって、任意の\(a:A\)に対して\(\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a\)かつ\(\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a\)となるものを構成せよ。