Ralph Matthes

Would there be a way to define a bicategory of monoidal categories on the basis of categories instead of univalent categories and only restrict to univalent categories for the purpose...

The second layer for the unitors and the associator also redoes a generic construction several times. For example, one could just put `Definition bidisp_lu_disp_prebicat : disp_prebicat tu_cat := disp_cell_unit_prebicat disp_lu_disp_cat_data.`...

I see that the blocking problem is solved, but I do not know how to mark this in the system. Anyway, I had made proposals for specific situations and asked...

@Kfwullaert I did not see those further simplifications coming. Very well observed. Yes, I think you should merge the three files of the second layer, even if they can be...

Still plenty of compilation warnings for a known cause.

@Kfwullaert Yes, please remove these curly variable binders.

Where is file `UniMath/CategoryTheory/Monoidal/MonoidalCategoriesReordered.v`?

@Kfwullaert > @rmatthes I think everything what should be in there is (if I did not forget anything). There is 1 lemma that I've admitted. The proof is commented out...

I maybe have lost track of a previous statement on the following matter: the file CurriedMonoidalCategories.v is not dependent on the notion of bicategory and should be moved into UniMath/CategoryTheory/Monoidal...

Yes, there was also the move from `iso` to `z_iso`, and the currently used `nat_z_iso` requires pointwise `is_z_isomorphism`.