Ulrik’s email nicely lays out the three key notions (pre-category, strict category, univalent category), and the argument for the Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning “univalent category” by default. For my part I lean the other way: I think it’s too radical to use “category” for a definition which doesn’t come out equivalent to the traditional definition under the naïve set interpretation (or under the addition of UIP to the type theory). Choosing terminology that actively clashes with traditional terminology makes it much harder to compare statements in HoTT with their classical analogues, and see what difference HoTT really makes to the development of topics. Based on that criterion, I strongly prefer taking category to mean “precategory”. A big payoff from this is that if you formalise something using “category ” to mean “precategory” in type theory without assuming UA, then you can read the result either as valid in HoTT, or (under the set-interpretation) as ordinary arguments in classical category theory, with all the terms meaning just what they traditionally would. Univalence of categories is an important and powerful property, but not an innocuous one; it changes the character of the resulting “category theory” in interesting ways. Making the restriction to univalent categories tacit is misleading to readers who aren’t fully “insiders”, and obscures understanding its effects. –p. -- 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.