Existence and uniqueness of \(j_f\) are the universal properties of \(2\text{-}\mathrm{coim}(f)\) and \(2\text{-}\mathrm{im}(f)\): the composite \(2\text{-}\mathrm{coker}(f)\circ f\) is isomorphic to a null morphism, so \(f\) factors through \(2\text{-}\mathrm{im}(f)=2\text{-}\mathrm{ker}(2\text{-}\mathrm{coker}(f))\), and dually the resulting morphism factors through \(2\text{-}\mathrm{coim}(f)\). Uniqueness holds because \(2\text{-}\mathrm{coim}(f)\) is a 2-epimorphism and \(2\text{-}\mathrm{im}(f)\) a 2-monomorphism, so any two 1-cells filling the triangle agree, by Remark 2.14 and its dual.

If \(j_f\) is an equivalence, then \(f\cong 2\text{-}\mathrm{im}(f)\circ \bigl(j_f\circ 2\text{-}\mathrm{coim}(f)\bigr)\) exhibits \(f\) as a normal 2-monomorphism after a normal 2-epimorphism, the second factor because a 2-cokernel composed with an equivalence is again a 2-cokernel; so \(f\) is normal. Conversely, let \(f\cong m\circ e\) with \(m\) a normal 2-monomorphism and \(e\) a normal 2-epimorphism. By Proposition 3.9 we have \(2\text{-}\mathrm{ker}(f)\simeq 2\text{-}\mathrm{ker}(e)\), and \(e\) is the 2-cokernel of its 2-kernel by Proposition 3.11, so \(2\text{-}\mathrm{coim}(f)\simeq e\); dually \(2\text{-}\mathrm{im}(f)\simeq m\). Under these equivalences the defining relation reads \(m\circ j_f\circ e\cong m\circ e\), and as \(m\) is fully faithful and \(e\) cofully faithful, \(j_f\) is isomorphic to an identity, hence an equivalence.

By Proposition 3.9, since \(2\text{-}\mathrm{im}(g)\) is a normal 2-monomorphism, \(2\text{-}\mathrm{ker}(g)\simeq 2\text{-}\mathrm{ker}(2\text{-}\mathrm{coim}(g))\); dually, since \(2\text{-}\mathrm{coim}(f)\) is a normal 2-epimorphism, \(2\text{-}\mathrm{coker}(f)\simeq 2\text{-}\mathrm{coker}(2\text{-}\mathrm{im}(f))\). Now \(2\text{-}\mathrm{im}(f)\simeq 2\text{-}\mathrm{ker}(g)\) as in (i) if and only if (iii) holds, because \(2\text{-}\mathrm{coim}(g)\), being a normal 2-epimorphism, is the 2-cokernel of its 2-kernel by Proposition 3.11; likewise \(2\text{-}\mathrm{coker}(f)\simeq 2\text{-}\mathrm{coim}(g)\) as in (ii) if and only if (iii) holds, because \(2\text{-}\mathrm{im}(f)\), being a normal 2-monomorphism, is the 2-kernel of its 2-cokernel.

Suppose \(m=2\text{-}\mathrm{ker}(e)\). From \(e\circ k\cong 0\) the morphism \(k\) factors through \(m\), say \(k\cong m\circ u\), and then \(w\cong q\circ m\circ u\cong 0\) because \(q\circ m\cong 0\). Conversely suppose \(w\cong 0\), and let \(t\) satisfy \(e\circ t\cong 0\). Then \(t\) factors through \(k\), say \(t\cong k\circ u\), so that \(q\circ t\cong w\circ u\cong 0\); and \(m\), being a normal 2-monomorphism, is a 2-kernel of its own 2-cokernel \(q\) by Proposition 3.11, so \(t\) factors through \(m\). Together with \(e\circ m\cong 0\) and the fact that \(m\) is a 2-monomorphism, this exhibits \(m\) as a 2-kernel of \(e\). That \(e\) is then a 2-cokernel of \(m\) is the same argument read in the dual.

No proof environment in the paper (the proof is either immediate or spread over the surrounding text); the dependencies shown are those of the Lean proof.

Write \(m\colon K\to X\), \(e\colon X\to R\), \(k=2\text{-}\mathrm{ker}(e)\) and \(q=2\text{-}\mathrm{coker}(m)\), so that \(w=q\circ k\). Being a normal 2-epimorphism, \(e\) is a 2-cokernel of \(k\), by Proposition 3.11.

Let \(u\colon R\to T\) satisfy \(u\circ e\circ m\cong 0\). Then \(q=2\text{-}\mathrm{coker}(m)\) yields \(u'\colon C\to T\) with \(u'\circ q\cong u\circ e\), and \(u'\circ w\cong u\circ e\circ k\cong 0\). Conversely, let \(v\colon C\to T\) satisfy \(v\circ w\cong 0\). Then \(v\circ q\circ k\cong 0\) and \(e=2\text{-}\mathrm{coker}(k)\) yields \(v'\colon R\to T\) with \(v'\circ e\cong v\circ q\), and \(v'\circ e\circ m\cong v\circ q\circ m\cong 0\). Each construction undoes the other, since \(e\) and \(q\) are 2-epimorphisms.

Now let \(q_1\colon R\to Q_1\) be a 2-cokernel of \(e\circ m\) and \(q_2\colon C\to Q_2\) one of \(w\). Applying the first construction to \(q_1\) and the second to \(q_2\) gives \(q_1'\colon C\to Q_1\) with \(q_1'\circ q\cong q_1\circ e\) and \(q_1'\circ w\cong 0\), and \(q_2'\colon R\to Q_2\) with \(q_2'\circ e\cong q_2\circ q\) and \(q_2'\circ e\circ m\cong 0\); whence \(x\colon Q_2\to Q_1\) with \(x\circ q_2\cong q_1'\) and \(y\colon Q_1\to Q_2\) with \(y\circ q_1\cong q_2'\). Then \(x\circ q_2'\circ e\cong x\circ q_2\circ q\cong q_1'\circ q\cong q_1\circ e\), so \(x\circ q_2'\cong q_1\) as \(e\) is a 2-epimorphism; hence \(x\circ y\circ q_1\cong q_1\) and \(x\circ y\cong \operatorname {id}_{Q_1}\), \(q_1\) being a 2-epimorphism. Symmetrically \(y\circ x\cong \operatorname {id}_{Q_2}\). So \(x\) is an equivalence.

Let \(0\colon A\to B\) be null. Since \(\operatorname {id}_{A}\) is a 2-kernel of it, \(2\text{-}\mathrm{Coim}(0)=2\text{-}\mathrm{Cok}(\operatorname {id}_{A})\), which is trivial because a 2-epimorphism has trivial 2-cokernel, by the dual of Lemma 2.24; dually \(2\text{-}\mathrm{Im}(0)=2\text{-}\mathrm{Ker}(\operatorname {id}_{B})\) is trivial. Now any morphism \(t\colon P\to I\) between trivial objects is an equivalence: taking \(s\colon I\to P\) to be a null morphism, both \(t\circ s\) and \(\operatorname {id}_{I}\) are null, hence isomorphic by Lemma 2.6, and dually for \(s\circ t\). The composite \(2\text{-}\mathrm{ker}(\operatorname {id}_{B})\circ t\circ 2\text{-}\mathrm{coker}(\operatorname {id}_{A})\) is therefore a normal 2-monomorphism after a normal 2-epimorphism—a 2-cokernel composed with an equivalence being again a 2-cokernel—and it is null, hence isomorphic to \(0\).

By Lemma 4.2 a morphism is normal exactly when its comparison is an equivalence. We show that each of the three conditions asserts precisely this for the dinversion of an arbitrary antinormal decomposition of the zero map. Condition (i) is that assertion verbatim.

For (ii), a normal chain complex and a position \(n\) provide the antinormal decomposition \((2\text{-}\mathrm{im}(d_{n+1}),2\text{-}\mathrm{coim}(d_n))\) of the zero map, whose antinormal composite is null since \(d_n\circ d_{n+1}\cong 0\); its dinversion is \(w_n\), with comparison \(j_n\). Conversely an antinormal decomposition \((m,e)\) of the zero map, with \(m\colon K\to X\) and \(e\colon X\to R\), sits at position \(0\) of the normal chain complex with \(K\), \(X\) and \(R\) in degrees \(2\), \(1\) and \(0\), a bizero object in every other degree, \(m\) and \(e\) as the two remaining differentials and null morphisms elsewhere; the padding is normal by Proposition 4.13, and the dinversion at position \(0\) is \(w\). Hence (i) and (ii) coincide.

For (iii), take a morphism of short 2-exact sequences with identity middle component, with top row \(A\xrightarrow []{a}B\xrightarrow []{b}C\), bottom row \(X\xrightarrow []{c}B\xrightarrow []{d}Z\) and verticals \(f\), \(\operatorname {id}_{B}\), \(h\). Then \((a,d)\) is an antinormal decomposition of the zero map, since \(d\circ a\cong d\circ c\circ f\cong 0\), with dinversion \(w=2\text{-}\mathrm{coker}(a)\circ 2\text{-}\mathrm{ker}(d)\cong b\circ c\). We claim \(2\text{-}\mathrm{ker}(w)\simeq f\). Indeed \(w\circ f\cong b\circ a\cong 0\), so \(f\) factors through \(2\text{-}\mathrm{ker}(w)\); and if \(t\) carries an invertible 2-cell \(w\circ t\cong 0\), then \(b\circ (c\circ t)\cong 0\), so the universal property of \(a=2\text{-}\mathrm{ker}(b)\) gives \(s\) with \(a\circ s\cong c\circ t\), whence \(c\circ f\circ s\cong c\circ t\) and, \(c\) being fully faithful, \(f\circ s\cong t\) essentially uniquely. Dually \(2\text{-}\mathrm{coker}(w)\simeq h\). Thus \(2\text{-}\mathrm{Coim}(w)\simeq 2\text{-}\mathrm{Cok}(f)\) and \(2\text{-}\mathrm{Im}(w)\simeq 2\text{-}\mathrm{Ker}(h)\), with \(j_w\) the comparison \(2\text{-}\mathrm{Cok}(f)\to 2\text{-}\mathrm{Ker}(h)\).

Conversely, let \((m,e)\) be an antinormal decomposition of the zero map. Take the top row \(K\xrightarrow []{m}X\xrightarrow []{2\text{-}\mathrm{coker}(m)}2\text{-}\mathrm{Cok}(m)\) and the bottom row \(2\text{-}\mathrm{Ker}(e)\xrightarrow []{2\text{-}\mathrm{ker}(e)}X\xrightarrow []{e}R\), both short 2-exact by Proposition 3.11, and the identity of \(X\) as middle component. The invertible 2-cell \(e\circ m\cong 0\) factors \(m\) through \(2\text{-}\mathrm{ker}(e)\) by some \(t\colon K\to 2\text{-}\mathrm{Ker}(e)\) and factors \(e\) through \(2\text{-}\mathrm{coker}(m)\) by some \(r\colon 2\text{-}\mathrm{Cok}(m)\to R\); these are the two outer verticals, and no coherence condition need be checked, by Proposition 3.26. The dinversion of the resulting configuration is \(2\text{-}\mathrm{coker}(m)\circ 2\text{-}\mathrm{ker}(e)\), which is \(w\) itself. Hence (i) and (iii) coincide.

Conditions (ii) and (iii) are dual, so we prove that (i) and (ii) are equivalent, using the Pure Snake characterisation Proposition 4.18 (iii).

Given a totally normal sequence of 2-monomorphisms \(A\xrightarrow []{a}X\xrightarrow []{c}B\), put \(b=c\circ a\) and form the morphism of short 2-exact sequences with identity middle component whose top row is \(A\xrightarrow []{b}B\xrightarrow []{2\text{-}\mathrm{coker}(b)}2\text{-}\mathrm{Cok}(b)\), bottom row \(X\xrightarrow []{c}B\xrightarrow []{2\text{-}\mathrm{coker}(c)}2\text{-}\mathrm{Cok}(c)\), and right vertical \(r\) induced by \(2\text{-}\mathrm{coker}(c)\circ b\cong 0\). Both rows are short 2-exact by Proposition 3.11, as \(b\) and \(c\) are normal 2-monomorphisms, and no coherence condition arises, by Proposition 3.26. As in the proof of Proposition 4.18, the dinversion is \(w=2\text{-}\mathrm{coker}(b)\circ c\), with \(2\text{-}\mathrm{ker}(w)\simeq a\) and \(2\text{-}\mathrm{coker}(w)\simeq r\); hence the induced 1-cell \(2\text{-}\mathrm{Cok}(a)\simeq 2\text{-}\mathrm{Coim}(w)\to 2\text{-}\mathrm{Cok}(b)\) is \(2\text{-}\mathrm{im}(w)\circ j_w\), with 2-cokernel \(r\). The sequence \(2\text{-}\mathrm{Cok}(a)\to 2\text{-}\mathrm{Cok}(b)\to 2\text{-}\mathrm{Cok}(c)\) is therefore short 2-exact if and only if \(j_w\) is an equivalence, that is, if and only if \(w\) is normal; and by Proposition 4.18 this holds for all such \(w\) precisely when the 2-category is homologically self-dual.

Conversely, let \((m,e)\) be an antinormal decomposition of the zero map, with dinversion \(w=2\text{-}\mathrm{coker}(m)\circ 2\text{-}\mathrm{ker}(e)\). The invertible 2-cell \(e\circ m\cong 0\) corestricts \(m\) to a morphism \(t\colon K\to 2\text{-}\mathrm{Ker}(e)\) with \(m\cong 2\text{-}\mathrm{ker}(e)\circ t\), and \(t\) is a normal 2-monomorphism by part (ii) of Proposition 3.6, the 2-monomorphism \(2\text{-}\mathrm{ker}(e)\) cancelling off the normal 2-monomorphism \(m\). So \(K\xrightarrow []{t}2\text{-}\mathrm{Ker}(e)\xrightarrow []{2\text{-}\mathrm{ker}(e)}X\) is a totally normal sequence of 2-monomorphisms. Applying (ii) to it returns a short 2-exact sequence whose 2-monomorphism part is the induced 1-cell \(2\text{-}\mathrm{Cok}(t)\to 2\text{-}\mathrm{Cok}(m)\); composed with \(2\text{-}\mathrm{coker}(t)\), that 1-cell is \(w\), by the construction of the induced morphism. Hence \(w\) is a normal 2-monomorphism after a normal 2-epimorphism, so normal.

Write \(p=2\text{-}\mathrm{coker}(f)\circ 2\text{-}\mathrm{ker}(g)\); then \(H\) is its 2-image, with \(r=2\text{-}\mathrm{coim}(p)\) and \(s=2\text{-}\mathrm{im}(p)\). For a morphism \(x\) into \(2\text{-}\mathrm{Ker}(g)\), an invertible 2-cell \(p\circ x\cong 0\) amounts to \(2\text{-}\mathrm{ker}(g)\circ x\) factoring through \(2\text{-}\mathrm{im}(f)=2\text{-}\mathrm{ker}(2\text{-}\mathrm{coker}(f))\); since \(2\text{-}\mathrm{im}(f)\simeq 2\text{-}\mathrm{ker}(g)\circ 2\text{-}\mathrm{im}(e)\) and \(2\text{-}\mathrm{ker}(g)\) is fully faithful, this amounts to \(x\) factoring through \(2\text{-}\mathrm{im}(e)\). Hence \(2\text{-}\mathrm{ker}(p)\simeq 2\text{-}\mathrm{im}(e)\) and \(H=2\text{-}\mathrm{Coim}(p)\simeq 2\text{-}\mathrm{Cok}(e)\); dually \(H=2\text{-}\mathrm{Im}(p)\simeq 2\text{-}\mathrm{Ker}(m)\).

The pair \((f,g)\) is exact in \(B\) precisely when \(2\text{-}\mathrm{im}(f)\simeq 2\text{-}\mathrm{ker}(g)\), that is, when \(2\text{-}\mathrm{im}(e)\simeq 2\text{-}\mathrm{Ker}(g)\), that is, when \(2\text{-}\mathrm{Coim}(p)=H\) is trivial; this is (iii)\(\Leftrightarrow \)(iv). If \((f,g)\) is exact, then \(2\text{-}\mathrm{ker}(g)\circ e\cong f\cong 2\text{-}\mathrm{im}(f)\circ 2\text{-}\mathrm{coim}(f)\) with \(2\text{-}\mathrm{im}(f)\simeq 2\text{-}\mathrm{ker}(g)\), so \(e\simeq 2\text{-}\mathrm{coim}(f)\) is a normal 2-epimorphism and dually \(m\simeq 2\text{-}\mathrm{im}(g)\) is a normal 2-monomorphism; thus (iii) implies (i) and (ii). Conversely, a 2-epimorphism has trivial 2-cokernel and a 2-monomorphism has trivial 2-kernel by Lemma 2.24, so \(e\) a 2-epimorphism gives \(H\simeq 2\text{-}\mathrm{Cok}(e)\) trivial and \(m\) a 2-monomorphism gives \(H\simeq 2\text{-}\mathrm{Ker}(m)\) trivial; thus (i) and (ii) each imply (iv).

The proof of Proposition 4.18 identifies \(f\) with \(2\text{-}\mathrm{ker}(w)\) and \(h\) with \(2\text{-}\mathrm{coker}(w)\) for the dinversion \(w\cong b\circ c\), so that \(2\text{-}\mathrm{Coim}(w)\simeq 2\text{-}\mathrm{Cok}(f)\) and \(2\text{-}\mathrm{Im}(w)\simeq 2\text{-}\mathrm{Ker}(h)\) and the comparison \(j_w\) of Lemma 4.2 is the displayed \(j\). Its uniqueness is that of Lemma 4.2: \(2\text{-}\mathrm{coker}(f)\) is a 2-epimorphism and \(2\text{-}\mathrm{ker}(h)\) a 2-monomorphism, so any two 1-cells filling the triangle agree. Homological self-duality makes \(w\) normal, hence \(j\) an equivalence by Lemma 4.2, which is 2-exactness at \(X\) and at \(C\); exactness at \(A\) and at \(Z\) says that \(f\) is a 2-monomorphism and \(h\) a 2-epimorphism, which they are, being a 2-kernel and a 2-cokernel of \(w\).