ofBifunctor — Mathlib

Lean4
/-- `F` is oplax monoidal given a counit morphism `η : F.obj (𝟙_ C) ⟶ 𝟙_ D` and a tensorator
`δ : F (- ⊗ -) ⟶ F - ⊗ F -` as a natural transformation between bifunctors, satisfying the
relevant compatibilities.
-/
def ofBifunctor : F.OplaxMonoidal where
  η := η
  δ X Y := (δ.app X).app Y
  δ_natural_left f X := (NatTrans.congr_app (δ.naturality f) X).symm
  δ_natural_right X f := ((δ.app X).naturality f).symm
  oplax_associativity X Y Z := NatTrans.congr_app (NatTrans.congr_app (NatTrans.congr_app oplax_associativity X) Y) Z
  oplax_left_unitality X := NatTrans.congr_app oplax_left_unitality X
  oplax_right_unitality X := NatTrans.congr_app oplax_right_unitality X
Похожие утверждения