Theorems · Theorem · category theory

CategoryTheory.Presieve.pullbackArrows.congr_simp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  (R R_1 : CategoryTheory.Presieve X) (e_R : R = R_1) [inst_1 : R.HasPullbacks f] ⦃Y_1 : C⦄ (a a_1 : Y_1 ⟶ Y),
  a = a_1 → CategoryTheory.Presieve.pullbackArrows f R a = CategoryTheory.Presieve.pullbackArrows f_1 R_1 a_1

Defined in

Mathlib.CategoryTheory.Sites.Pretopology

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Presieve.HasPullbacks