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

[Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1770 bytes --]

On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbuchholtz@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.

[-- Attachment #2: Type: text/html, Size: 2667 bytes --]