English
For any i, j with same additivity context, the map respects the composition structure: map f i k ⋯ equals the composite map through i -> j then j -> k.
Русский
Для любых i, j в контексте добавления равенств отображение map уважает композицию: map f i k ⋯ равняется композиции через i ⟶ j затем j ⟶ k.
LaTeX
$$$\\forall i,j,k,\\ map f i k = map f i j hij \\circ map f j k hjk.$$$
Lean4
/-- The morphism `X i ⟶ X j` obtained by composing morphisms of
the form `X n ⟶ X (n + 1)` when `i ≤ j`. -/
def map : ∀ {X : ℕ → C} (_ : ∀ n, X n ⟶ X (n + 1)) (i j : ℕ), i ≤ j → (X i ⟶ X j)
| _, _, 0, 0 => fun _ ↦ 𝟙 _
| _, f, 0, 1 => fun _ ↦ f 0
| _, f, 0, l + 1 => fun _ ↦ f 0 ≫ map (fun n ↦ f (n + 1)) 0 l (by omega)
| _, _, _ + 1, 0 => nofun
| _, f, k + 1, l + 1 => fun _ ↦ map (fun n ↦ f (n + 1)) k l (by omega)
