Theorems · Definition · category theory

CategoryTheory.Prod.mkHom

{C : Type u₁} →
  [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] →
        {X₁ X₂ : C} → {Y₁ Y₂ : D} → (X₁ ⟶ X₂) → (Y₁ ⟶ Y₂) → ((X₁, Y₁) ⟶ (X₂, Y₂))

Construct a morphism in a product category by giving its constituent components. This constructor should be preferred over Prod.mk, because Lean infers better the source and target of the resulting morphism.

Defined in

Mathlib.CategoryTheory.Products.Basic

Cited by

108 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 11 definitions · uses no axioms

Assumes

CategoryTheory.CategoryStructCategoryTheory.CategoryStruct