English
Auxiliary construction for mkHom: builds a family of commutative squares by induction, ensuring eventual consistency of the squares even if not explicit at the type level.
Русский
Вспомогательное построение для mkHom: по индукции строит семейство коммутативных квадратов, обеспечивая согласованность квадратов в итоговом отображении.
LaTeX
$$$\\mathrm{mkHomAux} : \\mathbb{N} \\to \\Sigma' (f: P.X_n \\to Q.X_n) (f': P.X_{n+1} \\to Q.X_{n+1}), f \\circ (Q.d\\, n\\,(n+1)) = (P.d\\, n\\,(n+1)) \\circ f'$$$
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 (n + 1) = P.d n (n + 1) ≫ f'
| 0 => ⟨zero, one, one_zero_comm⟩
| n + 1 => ⟨(mkHomAux n).2.1, (succ n (mkHomAux n)).1, (succ n (mkHomAux n)).2⟩
