I'm a bit confused by your message, Peter: HoTT doesn't have a naive set interpretation and is inconsistent with UIP, so I'm not sure how that should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) This is too clever! If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so. Hence I think the terminology category / univalent category is preferable. This also maintains the traditional wisdom that categories (with trivial ie.e propositional homsets) correspond to preorders. We may add that univalent categories correspond to partial orders. And yes indeed there is something wrong with preorders because they have equality and equivalence and hence it is better to have a preorder. The same holds for categories, you have both equality and isomorphism and hence it is better to have a univalent category. Thorsten From: on behalf of Ulrik Buchholtz Date: Wednesday, 7 November 2018 at 11:44 To: Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine wrote: 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. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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.