English
Given a cofan for the last n entries and a binary cofan that merges with the (n+1)-st element, produce a cofan for all n+1 entries.
Русский
Имея кобину для последних n элементов и двоичный кобан, объединяющий с (n+1)-м элементом, получить кобин для всех n+1 элементов.
LaTeX
$$$$ \mathrm{extendCofan}: \text{Cofan fun i : Fin n => f(i.succ)} \to \text{BinaryCofan} (f(0)) \to \text{Cofan}(f). $$$$
Lean4
/-- Given `n+1` objects of `C`, a cofan for the last `n` with point `c₁.pt`
and a binary cofan on `c₁.X` and `f 0`, we can build a cofan for all `n+1`.
In `extendCofanIsColimit` we show that if the two given cofans are colimits,
then this cofan is also a colimit.
-/
@[simps!]
def extendCofan {n : ℕ} {f : Fin (n + 1) → C} (c₁ : Cofan fun i : Fin n => f i.succ) (c₂ : BinaryCofan (f 0) c₁.pt) :
Cofan f :=
Cofan.mk c₂.pt
(by
refine Fin.cases ?_ ?_
· apply c₂.inl
· intro i
apply c₁.ι.app ⟨i⟩ ≫ c₂.inr)
