Theorems · Definition · category theory

CategoryTheory.Presieve.pullbackArrows.recOn

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X}
  [inst_1 : R.HasPullbacks f] {motive : ⦃Y_1 : C⦄ → (a : Y_1 ⟶ Y) → CategoryTheory.Presieve.pullbackArrows f R a → Prop}
  ⦃Y_1 : C⦄ {a : Y_1 ⟶ Y} (t : CategoryTheory.Presieve.pullbackArrows f R a),
  (∀ (Z : C) (h : Z ⟶ X) (hRh : R h), motive (CategoryTheory.Limits.pullback.snd h f) ⋯) → motive a t

Defined in

Mathlib.CategoryTheory.Sites.Sieves

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Presieve.HasPullbacks