Theorems · Theorem · category theory

CategoryTheory.CostructuredArrow.w_prod_snd

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {A B : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (S'.map f.left.2) B.hom.2 = A.hom.2

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category