Remove the notion of "Precategory"

[mortberg]

I think we should remove the notion of "precategory" (categories without the assumption that the hom-types are sets) from the library, or at least decouple them from the theory of categories with hom-sets.

At the moment the hom-set assumption is separate in the form of the isCategory predicate which is like in UniMath which has a has_homsets predicate. This turned out to be a bad design decision as the extra generality with hom-types doesn't have very interesting theory. Plus, when developing 1-category theory it gets very annoying to pass around the "has homsets" assumption explicitly. Another more major problem is that when one has a category and want to use an operation defined for precategories then one needs to forget the "has homsets" assumption, which then often confuses the system, leading to many arguments having to be passed around explicitly (yet another issue related to this is that Agda doesn't have implicit projections making this even more painful than in Coq...). The problems get super annoying when trying to reason about iterated functor categories or slice categories.

What do other people think?

[barrettj12]

I think for sure that Category should be the primary notion. I've never seen the word "Precategory" outside this library

[kangrongji]

Not really relevant to this issue... But I think what corresponds to the usual notion of 1-category is the "univalent category" or the "category" with Set-objects (in library's terms), and they should be equivalent someway. Is there any proof about these in library? Also, does the library have defined the so-called Rezk completion? I mean the procedure which makes category into univalent category.

[mortberg]

No, we don't have the Rezk completion formalized. It would be a nice contribution.

I'll close this PR now that #629 is merged

[anuyts]

As the pull-request above already showed, if anyone is ever going to use precategories more seriously, then this is going to lead to a lot of code duplication.
An alternative could be to define a type HCategory ℓ ℓ' h h' indexed by two levels of type Level and two h-levels of type Maybe ℕ (with nothing standing for infinity); each time one for objects and one for morphisms. Then we can define Category ℓ ℓ' = HCategory ℓ ℓ' nothing (just 2). This way in a first iteration we can program for categories, but whoever needs precategories, or categories with an h-set of objects, or setoids, can start generalizing rather than duplicating the code.