English
For a family t that assigns to each i a presieve on Y i (depending on the arrow f i), the uncurry of s.bind t equals the union over i in s.uncurry of the image under the map taking a morphism to its composition with i.2 of the uncurry of t i.
Русский
Для семейства t, присваивающего каждому i пресейв на Y i, распакованный пресейв s.bind t равен объединению по i из s.uncurry образа отображения, отправляющего g на g ≫ i.2, от uncurry t i.
LaTeX
$$$ (s.bind t).uncurry = \\bigcup_{i \\in s.uncurry} \\Sigma.map\\, id\\ (\\lambda Z\\ g, (g \\;\\gg\\; i.2)) '' (t\\ _\\ ‹_›).uncurry $$$
Lean4
@[simp]
theorem uncurry_bind (t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y) :
(s.bind t).uncurry = ⋃ i ∈ s.uncurry, Sigma.map id (fun Z g ↦ (g ≫ i.2 : Z ⟶ X)) '' (t _ ‹_›).uncurry :=
by
ext ⟨Z, v⟩; simp only [Set.mem_iUnion, Set.mem_image]; constructor
· rintro ⟨Y, g, f, hf, ht, hv⟩
exact ⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩
· rintro ⟨⟨_, f⟩, hf, ⟨Y, g⟩, hg, h⟩
rw [Sigma.ext_iff] at h
obtain ⟨rfl, h⟩ := h
rw [heq_iff_eq] at h; subst h
exact ⟨_, _, _, _, hg, rfl⟩
