Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.Arrow.Hom.mk_hom

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W}
  (f :
    (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj A ⟶
      (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj B)
  (hfl : Q (CategoryTheory.Arrow.Hom.left f)) (hfr : W (CategoryTheory.Arrow.Hom.right f)),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Arrow.Hom.mk f hfl hfr) = f

Defined in

Mathlib.CategoryTheory.MorphismProperty.Comma

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.IsMultiplicative