Definition prebicat_data_from_monoidal : prebicat_data. Proof. use make_prebicat_data. - exact (one_cells_data_from_monoidal ,, two_cells_from_monoidal). - split. { intros ? ? f. exact (id₁ f). } split. { intros ? ? f. apply monoidal_leftunitordata. } split. { intros ? ? f. apply monoidal_rightunitordata. } split. { intros ? ? f. apply monoidal_leftunitorinvdata. } split. { intros ? ? f. apply monoidal_rightunitorinvdata. } split. { intros ? ? ? ? f g h. exact ( α_{ M } f g h ). } split. { intros ? ? ? ? f g h. exact ( αinv_{ M } f g h ). } split. { intros ? ? f g h. exact compose. } split. { intros ? ? ? f g h. exact (λ u, (f ⊗^{ M }_{l} u)). } intros ? ? ? f g h. exact (λ u, (u ⊗^{ M }_{r} h)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Section Bicat_From_Monoidal_Cat. Import Bicat.Notations. Import BifunctorNotations. Import MonoidalNotations. End Bicat_From_Monoidal_Cat.