ofBifunctor — Mathlib

Lean4
/-- `F` is monoidal given a co/unit morphisms `ε/η : 𝟙_ D ↔ F.obj (𝟙_ C)` and tensorators
`μ / δ : F - ⊗ F - ↔ F (- ⊗ -)` as natural transformations between bifunctors, satisfying the
relevant compatibilities.
-/
def ofBifunctor (ε_η : ε ≫ η = 𝟙 _) (η_ε : η ≫ ε = 𝟙 _) (μ_δ : μ ≫ δ = 𝟙 _) (δ_μ : δ ≫ μ = 𝟙 _) : F.Monoidal
    where
  toLaxMonoidal := .ofBifunctor ε μ associativity left_unitality right_unitality
  toOplaxMonoidal := .ofBifunctor η δ oplax_associativity oplax_left_unitality oplax_right_unitality
  ε_η := ε_η
  η_ε := η_ε
  μ_δ X Y := NatTrans.congr_app ((NatTrans.congr_app μ_δ) X) Y
  δ_μ X Y := NatTrans.congr_app ((NatTrans.congr_app δ_μ) X) Y
Похожие утверждения