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 l. } split. { intros ? ? f. apply ρ. } split. { intros ? ? f. apply (nat_z_iso_inv l). } split. { intros ? ? f. apply (nat_z_iso_inv ρ). } split. { intros ? ? ? ? f g h. apply (α ((f , g) , h)). } split. { intros ? ? ? ? f g h. apply ((nat_z_iso_inv α) ((f , g) , h)). } split. { intros ? ? f g h. exact compose. } split. { intros ? ? ? f g h. exact (λ u, (id f #⊗ u)). } intros ? ? ? f g h. exact (λ u, (u #⊗ id 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.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Section Bicat_From_Monoidal_Cat. End Bicat_From_Monoidal_Cat.