monoidalOfHasFiniteProducts — Mathlib

Lean4
/-- A category with a terminal object and binary products has a natural monoidal structure. -/
def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C :=
  letI : MonoidalCategoryStruct C :=
    { tensorObj := fun X Y ↦ X ⨯ Y
      whiskerLeft := fun _ _ _ g ↦ Limits.prod.map (𝟙 _) g
      whiskerRight := fun {_ _} f _ ↦ Limits.prod.map f (𝟙 _)
      tensorHom := fun f g ↦ Limits.prod.map f g
      tensorUnit := ⊤_ C
      associator := prod.associator
      leftUnitor := fun P ↦ Limits.prod.leftUnitor P
      rightUnitor := fun P ↦ Limits.prod.rightUnitor P }
  .ofTensorHom (pentagon := prod.pentagon) (triangle := prod.triangle) (associator_naturality :=
    @prod.associator_naturality _ _ _)
Похожие утверждения