English
In the alternate mk' construction, the 0-th component equals X₀: (mk' X₀ X₁ d₀ succ').X 0 = X₀.
Русский
В альтернативном mk' конструкторе нулевой компонент равен X₀.
LaTeX
$$$$(\\mathrm{mk}'\\ X_0 X_1\ d_0\ succ').X_0 = X_0$$$$
Lean4
/-- An auxiliary construction for `mkHom`.
Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in `mkHom`.
-/
def mkHomAux : ∀ n, Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n + 1) ⟶ Q.X (n + 1)), f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f
| 0 => ⟨zero, one, one_zero_comm⟩
| n + 1 => ⟨(mkHomAux n).2.1, (succ n (mkHomAux n)).1, (succ n (mkHomAux n)).2⟩
