Hi, First, there are (at least) three mathematically important and useful types: precategories, strict (or set) categories (precategories with a set of objects), and (univalent) categories. I take as one main lesson from HoTT/UF that mathematical objects have types, and that the identity types should indicate the relevant notion of identity. The type of precategories is equivalent to that of type-flagged categories (categories together with a type O and a function from O to the objects of the category). (The equivalence is given by pulling back the category structure to get a precategory structure with O as the type of objects in one way, and taking the Rezk completion together with the object part of unit map in the other.) Two precategories are identified via an equivalence of the O-types and an equivalence of the categories, together with a witness that the square commutes. Two strict categories are identified via an isomorphism, and two (univalent) categories are identified via an equivalence. So I disagree that "precategory" is the usual notion of category: it can't be because the criterion of identity is different. But it's still a useful concept. I personally prefer to keep “category” for univalent precategory, as most often constructions on categories are meant to be well-defined up to equivalence of categories. In the category theory literature written in a set-theory metatheory where the distinction is not so clear, you can of course find plenty of uses of the word “category” where “strict category” is meant from a HoTT/UF point-of-view. The type of precategories as a common generalization of strict and univalent categories is, I think, a new concept to HoTT/UF. (Although infinity-groupoid flagged (infinity,1)-categories arose independently in homotopy theory; these could also be called (infinity,1)-precategories.) Cheers, Ulrik On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote: > > I want to get a general idea of peoples opinions when it comes to naming > categories internal to HoTT. > > On the one hand I have seen, in the HoTT book for example, precategory and > category being used where the latter has the map idtoiso being an > equivalence. > > On the other hand I have seen people call these categories and univalent > categories which is also fine. > > Now because we have Rezk completion every precategory is yearning to > become a category, so some might argue that a distinction isn't necessery. > I would argue that the HoTT book convention is infact more misleading as > "precategory" there is really just the usual notion of category. And a > univalent category is some nice structure we can add to it because we are > working in HoTT. > > What are your thoughts and opinions on this? > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.