English
Let 𝒜 be an index type, f : 𝒜 → FormalCoproduct C a and t a FormalCoproduct C. Then the maps from the constructed cofan to t are in natural bijection with families of maps from each component f i to t. This is the universal property of coproducts realized explicitly as an Equivalence.
Русский
Пусть 𝒜 — множество индексов, f : 𝒜 → FormalCoproduct C, и t — копроизведение C. Тогда гомоморфизмы из построенного кофана в t естественным образом эквивалентны семейству гомоморфизмов из каждого компонента f i в t. Это явное равенство свойств копроизводного объекта.
LaTeX
$$$\\left((\\mathrm{cofan} \\; \\mathcal{A} f).pt \\to t\\right) \\simeq \\left(\\prod_{i:\\mathcal{A}} (f\\,i \\to t)\\right)$$$
Lean4
/-- The explicit `Equiv` between maps from the constructed coproduct `cofan 𝒜 f` and families of
maps from each component, which is the universal property of coproducts. -/
@[simps!]
def cofanHomEquiv : ((cofan 𝒜 f).pt ⟶ t) ≃ ((i : 𝒜) → (f i ⟶ t))
where
toFun m i := (cofan 𝒜 f).inj i ≫ m
invFun s := ⟨fun p ↦ (s p.1).f p.2, fun p ↦ (s p.1).φ p.2⟩
left_inv m := hom_ext rfl (fun ⟨i, x⟩ ↦ by simp [cofan_inj])
right_inv p := by ext <;> simp
