Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Michael Shulman <shulman@sandiego.edu>]

If one wants a name for "pre-category" that sounds less derogatory,
one could say "flagged category".  Talking about "flagged categories",
"strict categories", and "univalent categories" will always be
unambiguous, and individual papers could declare that plain "category"
will locally mean one or another as desired.
On Thu, Nov 8, 2018 at 1:37 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
> 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.
>
> --
> 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.

-- 
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.