This supplementary note describes an earlier formalization. Its code links are temporarily disabled pending review for rebuild2.
Reordering inverse conditions
In the construction of inverse data, a triangle has one short edge prescribed and its long edge identified with an identity. One can impose these constraints in either order. The comparison must preserve the projection to the original family of arrows.
The first two lemmas use only the absolute pullback structure of Chapter 1.
Supplementary Lemma 1. Let \(f\colon B\to A\), \(g\colon T\to A\), \(h\colon T\to E\), and \(s\colon D\to E\). Put \(R=B\times _A T\), with projections \(p,q\), and \(J=T\times _E D\), with projection \(j\colon J\to T\). There is a specified equivalence \[ \Phi \colon R\times _E D\longrightarrow J\times _A B, \qquad \pi _B\Phi =p\pi _R, \] where the two fiber products use \((hq,s)\) and \((gj,f)\) respectively. In particular, if \(p\pi _R\) is an equivalence, so is \(\pi _B\).
Proof idea
Nested pullback comparison first gives \(R\times _E D\simeq R\times _T J\). Exchange the two legs to obtain \(J\times _T R\), then flatten using the defining pullback of \(R\), with its legs exchanged, to obtain \(J\times _A B\). All three comparison functors are equivalences by pullback pasting.
Trace the projection to \(B\) through the three stages. Their specified projection comparisons give \(\pi _B\Phi =p\pi _R\). The two-out-of-three property then gives the last assertion. This step uses the projection comparison in addition to equivalence of the categories. □
Supplementary Lemma 2. Let \(e\colon E\to C\) and \(c\colon C\to E\) be equipped with an identification \(ec=\mathrm {id}_C\). Let \(T\) be a pullback of \(e\) along \(b\colon B\to C\), with projections \(h\colon T\to E\) and \(t\colon T\to B\). Then \[ t\pi _T\colon T\times _E C\longrightarrow B \] is an equivalence, where the pullback uses \(h\) and \(c\).
Proof idea
Paste the defining pullback of \(T\times _E C\) with the given pullback square for \(T\). The outer rectangle is a pullback of \(ec\) along \(b\). Since \(ec\) is identified with the identity, its pullback projection is an equivalence. Pullback symmetry supplies the orientation used in the nested construction. □
Application to inverse triangles
Write \(\operatorname {Triang}(C)\) for the triangle category, \(\operatorname {Ar}(C)\) for the arrow category, and \(d_C\colon C\to \operatorname {Ar}(C)\) for the identity-arrow functor. Put \[ J(C)=\operatorname {Triang}(C)\times _{\operatorname {Ar}(C)} C, \] using long-edge restriction and \(d_C\). Its two short-edge maps to \(\operatorname {Ar}(C)\) describe the given arrow in one-sided inverse data.
Supplementary Lemma 3. Assume the Segal and commutative-square axioms and their interval endpoint data. Let \(f\colon B\to \operatorname {Ar}(C)\) be a family. Its canonical morphism expression has endpoints \(e_0f,e_1f\) and identity frames, where \(e_0,e_1\) are endpoint evaluations. Suppose this expression is equipped with invertibility data. For either short-edge map \(J(C)\to \operatorname {Ar}(C)\), the projection \[ J(C)\times _{\operatorname {Ar}(C)}B\longrightarrow B \] is an equivalence.
Proof idea
Fix the relevant short edge first. Composition by that invertible arrow is an equivalence, so the corresponding long-edge square is a pullback. Apply Supplementary Lemma 2 using the identity-arrow section of the relevant endpoint evaluation functor. This proves the projection is an equivalence when the long edge is made constant second.
Apply Supplementary Lemma 1 to reverse the order of the two constraints. Its projection equation identifies the tested map with the displayed projection from one-sided inverse data. This proves the assertion for each short edge. The Rezk axiom is not used here. □
The later isomorphism-embedding argument combines the two inverse conditions. This note isolates the pullback calculation supplying their individual projections.