\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。関数\(\mathord {\textnormal {\textsf {codiag}}}(f):B\mathbin {{}_{f}\smash {+}_{f}}B\to B\)を

• -\(\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {in}}}_{1}(y))\equiv y\)
• -\(\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv y\)
• -\(\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {glue}}}(x))=\mathord {\textnormal {\textsf {refl}}}\)

で定義する。