Lean4
/-- The oplax monoidal functor structure induced by a `Functor.CoreMonoidal` structure. -/
@[simps -isSimp]
def toOplaxMonoidal : F.OplaxMonoidal where
η := h.εIso.inv
δ X Y := (h.μIso X Y).inv
δ_natural_left _
_ := by
rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc, ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_id, comp_id]
δ_natural_right _
_ := by
rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc, ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_id, comp_id]
oplax_associativity X Y
Z := by
rw [← cancel_epi (h.μIso (X ⊗ Y) Z).hom, Iso.hom_inv_id_assoc, ← cancel_epi ((h.μIso X Y).hom ▷ F.obj Z),
hom_inv_whiskerRight_assoc, associativity_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv, comp_id]
oplax_left_unitality
_ := by
rw [← cancel_epi (λ_ _).hom, Iso.hom_inv_id, h.left_unitality, assoc, assoc, Iso.map_hom_inv_id_assoc,
Iso.hom_inv_id_assoc, hom_inv_whiskerRight]
oplax_right_unitality
_ := by
rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc, Iso.map_hom_inv_id_assoc,
Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
