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?