English
Every presieve on X can be represented as an ofArrows data: there exist indices and arrows giving R = ofArrows Y f.
Русский
Каждая предсистема на X может быть представлена как ofArrows: существуют индексы и стрелы, дающие R = ofArrows Y f.
LaTeX
$$$\\exists \\iota, Y, f: R = \\mathrm{ofArrows} Y f$$$
Lean4
theorem ofArrows_bind {ι : Type*} (Z : ι → C) (g : ∀ i : ι, Z i ⟶ X) (j : ∀ ⦃Y⦄ (f : Y ⟶ X), ofArrows Z g f → Type*)
(W : ∀ ⦃Y⦄ (f : Y ⟶ X) (H), j f H → C) (k : ∀ ⦃Y⦄ (f : Y ⟶ X) (H i), W f H i ⟶ Y) :
((ofArrows Z g).bind fun _ f H => ofArrows (W f H) (k f H)) =
ofArrows (fun i : Σ i, j _ (ofArrows.mk i) => W (g i.1) _ i.2) fun ij => k (g ij.1) _ ij.2 ≫ g ij.1 :=
by
funext Y
ext f
constructor
· rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩
exact ofArrows.mk (Sigma.mk _ _)
· rintro ⟨i⟩
exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)
