English
A coproduct over coproducts is a coproduct indexed by a product.
Русский
Копродукт над коfановами есть coproduct, индексируемый произведением.
LaTeX
$$$\text{prod}: \; \text{IsColimit } c' \to \text{IsColimit } c$$$
Lean4
/-- A coproduct over coproducts is a coproduct indexed by a product. -/
def prod (c : ∀ i : ι, Cofan (fun j : ι' ↦ X i j)) (hc : ∀ i : ι, IsColimit (c i)) (c' : Cofan (fun i : ι ↦ (c i).pt))
(hc' : IsColimit c') : (IsColimit <| Cofan.mk c'.pt fun p : ι × ι' ↦ (c p.1).inj p.2 ≫ c'.inj _) :=
by
refine mkCofanColimit _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
· exact Cofan.IsColimit.desc hc' fun i ↦ Cofan.IsColimit.desc (hc i) fun j ↦ t.inj (i, j)
· simp
· refine Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_
exact Cofan.IsColimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))
