Theorems · Theorem · category theory

CategoryTheory.Limits.pullbackAssoc_inv_snd

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      (CategoryTheory.Limits.pullback.snd f₃ f₄)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback