Theorems · Definition · category theory

CategoryTheory.MorphismProperty.prod

{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.CategoryStruct.{u_3, u_1} C₁] →
      [inst_1 : CategoryTheory.CategoryStruct.{u_4, u_2} C₂] →
        CategoryTheory.MorphismProperty C₁ →
          CategoryTheory.MorphismProperty C₂ → CategoryTheory.MorphismProperty (C₁ × C₂)

If W₁ and W₂ are morphism properties on two categories C₁ and C₂, this is the induced morphism property on C₁ × C₂.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Basic

Cited by

11 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryStructCategoryTheory.CategoryStruct