English
An auxiliary inductive construction supplying a family of diagrams for the coinductive homotopy, without requiring at the type level that all sequential diagrams commute; the diagrams will be shown to commute later in the development.
Русский
Вспомогательная индуктивная конструкция задаёт семейство диаграмм для коиндуктивной гомотопии без необходимости на уровне типа требовать их взаимной совместимости; далее будет доказано их совместимость.
LaTeX
$$Definition of mkCoinductiveAux₁ with recursive clauses giving diagrams$$
Lean4
/-- An auxiliary construction for `mkInductive`.
-/
def mkCoinductiveAux₂ : ∀ n, Σ' (f : P.X n ⟶ Q.xPrev n) (f' : P.xNext n ⟶ Q.X n), e.f n = f ≫ Q.dTo n + P.dFrom n ≫ f'
| 0 => ⟨0, (P.xNextIso rfl).hom ≫ zero, by simpa using comm_zero⟩
| n + 1 =>
let I := mkCoinductiveAux₁ e zero one comm_one succ n
⟨I.1 ≫ (Q.xPrevIso rfl).inv, (P.xNextIso rfl).hom ≫ I.2.1, by simpa using I.2.2⟩
