I have asked on the HoTT mailing list for peoples opinions on naming “precategories” and “categories”. Please join the discussion!
Part of the reason is that if most of the community feel one is better than the other I will probably change the Wiki articles to accomodate this. It would also be useful for the second edition of the HoTT book.
]]>