English
Given a family X: I1 ⊕ I2 → C, a cofan c of X, and colimit cofans c1 for X∘inl and c2 for X∘inr, one obtains a canonical binary cofan with legs c1.pt and c2.pt and vertex c.pt.
Русский
Для семейства X: I1 ⊕ I2 → C, данного кофана c для X и колимитных кофанов для X∘inl и X∘inr строится канонический бинарный кофан с ногами c1.pt, c2.pt и вершиной c.pt.
LaTeX
$$$\\text{binaryCofanSum}(c,c_1,c_2,h_c,h_{c1},h_{c2}) = \\text{BinaryCofan}(c_1.pt, c_2.pt)$$$
Lean4
/-- Given a family of objects `X : I₁ ⊕ I₂ → C`, a cofan of `X`, and two colimit cofans
of `X ∘ Sum.inl` and `X ∘ Sum.inr`, this is a cofan for `c₁.pt` and `c₂.pt` whose
point is `c.pt`. -/
@[simp]
def binaryCofanSum : BinaryCofan c₁.pt c₂.pt :=
BinaryCofan.mk (Cofan.IsColimit.desc hc₁ (fun i₁ => c.inj (Sum.inl i₁)))
(Cofan.IsColimit.desc hc₂ (fun i₂ => c.inj (Sum.inr i₂)))
