English
Every glued element x arises as ι_i(y) for some i and y.
Русский
Каждый элемент склейки x равен ι_i(y) для некоторого i и y.
LaTeX
$$$\\exists i\\in J,\\; \\exists y\\in U_i:\\; D.\\u0307\\u0131_i(y)=x$$$
Lean4
theorem types_ι_jointly_surjective (D : GlueData (Type v)) (x : D.glued) : ∃ (i : _) (y : D.U i), D.ι i y = x :=
by
delta CategoryTheory.GlueData.ι
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
rcases D.types_π_surjective x with
⟨x', rfl⟩
--have := colimit.isoColimitCocone (Types.coproductColimitCocone _)
rw [←
show (colimit.isoColimitCocone (Types.coproductColimitCocone.{v, v} _)).inv _ = x' from
ConcreteCategory.congr_hom (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
exact
⟨i, y, by
simp
rfl⟩
