ofBifunctor — Mathlib

Lean4
/-- `F` is monoidal given a unit isomorphism `ε : 𝟙_ D ≅ F.obj (𝟙_ C)` and a tensorator isomorphism
`μ : F - ⊗ F - ≅ F (- ⊗ -)` as a natural isomorphism between bifunctors, satisfying the
relevant compatibilities.
-/
def ofBifunctor : F.CoreMonoidal where
  εIso := ε
  μIso X Y := (μ.app X).app Y
  μIso_hom_natural_left f X := NatTrans.congr_app (μ.hom.naturality f) X
  μIso_hom_natural_right X f := (μ.hom.app X).naturality f
  associativity X Y Z := NatTrans.congr_app (NatTrans.congr_app (NatTrans.congr_app associativity X) Y) Z
  left_unitality X := NatTrans.congr_app left_unitality X
  right_unitality X := NatTrans.congr_app right_unitality X
Похожие утверждения