English
The bind of arrows preserves the OfArrows structure: the bind of Z g with f is equal to an OfArrows with the composed data.
Русский
Связывание стрелок сохраняет структуру OfArrows: связка стрелок Z g с f равна OfArrows с композиционными данными.
LaTeX
$$$$\\bigl(\\mathrm{Presieve}.\\mathrm{bind}\\; (X,g)\\bigr) = \\mathrm{Presieve}.\\mathrm{ofArrows}\\ (p\\mapsto Y_{p.fst} (p.snd))\\ (\\text{comp } (g p.fst) (f p.fst))$$$$
Lean4
theorem bindOfArrows_ofArrows {ι : Type*} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {σ : ι → Type*}
{Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) :
Presieve.bindOfArrows X f (fun i ↦ .ofArrows (Y i) (g i)) =
Presieve.ofArrows (fun p : Σ i, σ i ↦ Y p.1 p.2) (fun p ↦ g p.1 p.2 ≫ f p.1) :=
by
refine le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)
rintro W u ⟨i, v, ⟨j⟩⟩
exact ⟨Sigma.mk i j⟩
