I have converted this PR from "draft" to "ready for review", so that I and others are able to comment.

A suggestion (relating to Benedikt's comments): to make these changes easier, the definition enriched_precat (https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Enriched/Enriched.v#L119) can be improved. A definition enriched_precat_laws (which is just (enriched_id_ax d) × (enriched_assoc_ax d).) can be added, and then for each enriched precategory, you can then just add a separate statement (which is just laws) can be proven and ended with Qed. The same idea can be used for functors.

I have been asked by @benediktahrens to provide a review for this PR. My feeling is that this changes the status of the development of enriched category theory in UniMath (which I welcome in principle), which therefore also requires a more rigorous review of the already existing code. Anyway, coqwc presently (before merging this PR) only sees 120 lines of definitions and 37 lines of proofs in the whole Enriched directory. And to the best of my knowledge, these definitions are not used elsewhere in UniMath. In particular, there is no validation of this code against the rest of UniMath, such as verifying that enriched categories are indeed a generalization of ordinary categories (in which sense will this hold in the UniMath library and not only mathematically?). It does not seem right either that composition is not given in diagrammatic order, which is the standard in UniMath. Previous to the PR, there were only three declared coercions. This is probably not enough (there are maybe too many pr1 already in that code, and this could become much worse when working with the definitions in application scenarios). The code is not so beautiful either: there are still dirprod and tpair in definitions, and axioms are stated with placeholders _.

The PR proposes more coercions and many more lines of verification, but still no validation w.r.t to the UniMath environment. I think that the problems at the base should be addressed at the same time and not later when there is much more code to "tame".

Is our composition operator in categories backwards? If so, I forgot.

By the way, the phrase "diagrammatic order" is ambiguous, because diagrams can also be drawn with leftward pointing arrows.

I cite from Categories.v:
Definition precategory_id_comp (C : precategory_ob_mor) : UU := (∏ c : C, c --> c) (* identities *) × (∏ a b c : C, a --> b -> b --> c -> a --> c). (* composition *)
Vertical composition in bicategories follows the same pattern.

By the way, it could be worth defining enrichment over bicategories instead of the special case of over monoidal categories.

@rmatthes : Thanks a lot for forming and sharing thoughts about this PR and the state of enriched categories in UniMath.

• I agree that the existing code needs to be improved to become usable at scale.
• I also agree that a validation (in the form of an equivalence of types between categories and categories enriched over set?) would be important for the sake of completeness. (I don't see any obstacle to constructing such an equivalence, it just needs to be done.)

@umedaikiti : in case you are interested in working on enriched categories in UniMath, and in case you are willing to spend a little bit of effort on getting the basic definitions into shape, I am very happy to help. I have already given feedback to your code - in case you have questions or comments, please let me know!

Thanks for the reviews. Yes, I am happy to work on the improvement.

• I agree that the code should be more beautiful.
• The equivalence between ordinary categories and Set-enriched categories would be easily proved if we have the cartesian monoidal category of sets. I know that the category of set is defined under UniMath/CategoryTheory/categories/HSET/ together with the terminal object and binary products, but it seems that the cartesian monoidal category is not defined. I believe that the (theoretically) best way is to define the general cartesian monoidal category and then instantiate it to HSET. Unfortunately the general cartesian monoidal category Monoidal structure on cartesian categories #1031 is left unmerged. I don't know yet how much work is needed to fix Monoidal structure on cartesian categories #1031, but I will try to take a look.
• I prefer the current order of composition rather than the diagrammatic order because the standard order in the enriched category theory is the current one and reversing it would be a little bit confusing especially when the monoidal category is not symmetric. For example, when we define left/right modules in the enriched category theory (see e.g. https://doi.org/10.1016/j.aim.2015.11.012), "left" and "right" must be reversed if we reverse the composition order. I think that this leads to inconsistent terminology between UniMath and the standard mathematics.

I only comment on the last point about the order of composition. I did not find it easy to read the UniMath library with the compositions turned around. I had to accept this decision by those who created the library. But the library does not deviate from standard mathematical notions. Even if left and right whiskering are rather called pre_whisker and post_whisker, respectively (which is even more suggestive as notation), they properly map to lwhisker and rwhisker in the notion of bicategories. Regardless of composition order or other notational/presentational devices, no one would exchange the notions of left and right adjoint either. In the development of monads, there is the file LModules.v with left modules for monads. They also properly correspond to the left modules as published by Hirschowitz and Maggesi. However, the development makes use of a legacy notation □ (I show one line from the output of git grep □):
UniMath/CategoryTheory/Core/Functors.v:Notation "G □ F" := (functor_composite F G) (at level 35, only parsing) : cat.
So, on the level of notation, the order of composition is again turned around (with respect to the standard UniMath notation for functor composition: Notation "F ∙ G" := (functor_composite F G) : cat. whose symbol looks different in Emacs from here.

The grep output is not vast at all and also shows uses of □ for different purposes. So, it should at least be very easy to remove this identified (legacy) inconsistency in notation. And no new one should enter, and as I argued before, the "lonesome" file Enriched.v was not considered a problem, but when making more out of it, the usual standards should apply.

@umedaikiti : Thanks a lot for implementing the suggestions!

For me, this PR represents a definite improvement, even though it does not yet fix all the problems identified by @rmatthes. Hence, I am very happy to merge this PR if @umedaikiti agrees - recall that this PR was marked as "draft" by @umedaikiti, and I only marked it as "ready for review" to be able to comment on it.

I have no objection to merging this PR. I will probably prove the equivalence between ordinary and Set-enriched categories later, but this can be discussed as a separate issue or PR.

Thanks a lot for your contribution to UniMath!