Theorems · Theorem · category theory

CategoryTheory.Limits.pullbackAssoc_hom_fst

∀ {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₄).hom
      (CategoryTheory.Limits.pullback.fst f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      (CategoryTheory.Limits.pullback.fst f₁ f₂)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Cited by

3 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