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
<p.l.lu...@gmail.com> wrote:
>
> On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote:
>>
>> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote:
>>>
>>> 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.
>>
>>
>> No, you get the notion of a strict category, which in some sense is all that you directly have in set theory.
>
>
> No in turn: you can arguably get either strict categories, or precategories, or what Thorsten dubbed “wild categories” above, since “set” in set theory is the (naïve) interpretation of both “set” and “type”. (Just as when you transcribe classical definitions in a constructive setting, you sometimes want to read “predicate” just as “predicate” and other times as “decidable predicate” — all predicates are decidable classically, but that doesn’t mean that their constructive transcription should include “decidable” by default.)
>
> –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.