Lean4
/-- The bicategory of algebras (monoids) and bimodules, all internal to some monoidal category. -/
noncomputable def monBicategory : Bicategory (Mon C)
where
Hom X Y := Bimod X Y
homCategory X Y := (inferInstance : Category (Bimod X Y))
id X := regular X
comp M N := tensorBimod M N
whiskerLeft L _ _ f := whiskerLeft L f
whiskerRight f N := whiskerRight f N
associator := associatorBimod
leftUnitor := leftUnitorBimod
rightUnitor := rightUnitorBimod
whiskerLeft_id _ _ := whiskerLeft_id_bimod
whiskerLeft_comp M _ _ _ f g := whiskerLeft_comp_bimod M f g
id_whiskerLeft := id_whiskerLeft_bimod
comp_whiskerLeft M N _ _ f := comp_whiskerLeft_bimod M N f
id_whiskerRight _ _ := id_whiskerRight_bimod
comp_whiskerRight f g Q := comp_whiskerRight_bimod f g Q
whiskerRight_id := whiskerRight_id_bimod
whiskerRight_comp := whiskerRight_comp_bimod
whisker_assoc M _ _ f P := whisker_assoc_bimod M f P
whisker_exchange := whisker_exchange_bimod
pentagon := pentagon_bimod
triangle := triangle_bimod
