Kobe Wullaert

> 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...

> 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...

@rmatthes Concerning disp_cell_unit_bicat, you are completely right, not only are the definitions more easy. Also the univalence proofs become even more easy. I didn't have to construct a factorization just...

@rmatthes I've changed the unitors and associator layers. Much shorter and easier now. I've changed the "message/overview of the file (i.e. the comment in the beginning of the file)" in...

> Still plenty of compilation warnings for a known cause. @rmatthes Should I remove the implicit binder declarations (all in the tensorlayer) in order to get rid of these warnings?

@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 because, although...

@rmatthes I've integrated the work. I've created a section Subtype_AUX where I've put certain things which could be set in the foundations (or more foundations). So we maybe should discuss...

> While it is okay to merge the PR, it would still be better if the parts of general nature were moved upstream (as indicated in my previous comments). Sorry...

A general question: You have defined the arrow category, however, the definition of morphismclass does not make use of this. Why did you not define morphismclass as a subtype of...

> > Thanks a lot for filing this PR. I have made a few small comments. > > Can you describe what the issue is with the admitted proof? You...