Theorems · Theorem · category theory

CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_comp

∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  {f₁'' : CategoryTheory.Arrow C₁} (sq₁₃'' : G.PullbackObjObj f₁''.hom f₃.hom) (sq' : f₁'' ⟶ f₁') (sq : f₁' ⟶ f₁),
  CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃' sq) (sq₁₃'.mapArrowLeft sq₁₃'' sq') =
    sq₁₃.mapArrowLeft sq₁₃'' (CategoryTheory.CategoryStruct.comp sq' sq)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category