We have two separate issues here: (1) What is the appropriate notion of category for univalent mathematics. (2) What is the right terminology for it. There is also a separate, orthogonal question, (3) Whether there is a foundation-independent (dubbed "agnostic") notion of category, which gives the right notion for each foundation, *and* can be formulated in MLTT (without K or univalence). Regarding (3), even if this is possible (assuming the question makes sense), it is not given by any of the proposed notions, and this should not be regarded as surprising or shocking. (This raises the question of whether there is a categorical definition of category, for people who would like to see category theory itself as a foundation.) Regarding (1), I think the arguments by Ulrik, Paolo, Mike and Eric (Finster) are pretty convincing: "univalent category" is the right notion of category for univalent mathematics. However, it *is* common and useful in mathematics to formulate and prove theorems with minimal hypotheses, and then what is called a pre-category, and what Thorsten called a wild category, often arise naturally and unavoidably as part of the building blocks of mathematics. Regarding (2), I would say, in view of (the answer to) (3), that it is probably better to avoid the naked terminology "category" in HoTT/UF, as it would give the wrong impression of *capturing* a universal, pre-existing, foundation-independent notion of category (in particular compatible with the ZFC view of what a category is, which has evilness as a built-in feature): * Then "univalent category" could mean, ambiguously but consistently, both (a) a pre-category that satisfies a certain technical condition analogous to the univalence axiom for types, or (b) "the appropriate notion of category for univalent mathematics". (c) In both cases, (a) and (b), the adjective "univalent" makes sense. In (b), it would be not in opposition to "category", but instead in opposition to e.g. "ZFC category". Martin On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote: > > I strongly agree with Ulrik. Perhaps the point that's not getting > across is that we are not talking about terminology for MLTT in > general, but specifically for HoTT (with univalence). The terminology > to be decided on doesn't have to make sense or come out to anything > meaningful in type theory with UIP, and we shouldn't expect it to. > The terminology in MLTT+UIP should be different from that for MLTT+UA, > because they are different theories and relate to "traditional" > mathematics in different *incompatible* ways. I doubt there is *any* > choice of terminology for plain MLTT without UA *or* UIP that is > sensible in that it can be specialized to the right terminology upon > the addition of either of these two inconsistent axioms. > On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine >