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

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2243 bytes --]

On Wednesday, November 7, 2018 at 3:05:44 PM UTC+1, Peter LeFanu Lumsdaine 
wrote:
>
> Yep, I indeed meant “agnostic” MLTT — in particular, without univalence 
> (or roughly-equivalent things like the glue-types of cubical type theory).  
> There are lots of motivations for working over that as far as possible: 
> baking univalence into material where it’s not really required feels like 
> when classical mathematicians make use of AC for no real advantage.
>

I'm in some respects sympathetic to this. We just have to be aware that 
working in agnostic type theory leaves us with a burden of 
mentally/manually handling the relevant notions of identity because the 
identity types cannot be relied upon.

But do you really think they don’t consider FinSet_N to be a category??  I 
>> find that very hard to believe: I am pretty sure that most traditional 
>> category theorists would consider FinSet_N a category without any doubt at 
>> all, which really seems to imply that the standard concept of category is 
>> more like “precategory” than “univalent category”.
>>
>
Well, FinSet_N presents FinSet and we often elide the difference between an 
object and a presentation for it, but we do so at our own peril. 
Traditionally, all categories are presented by a strict category, but 
traditional category theorists context-switch easily between strict and 
univalent categories (using heuristics about “evil”–there we go with the 
preaching again, sorry!).

I'm beginning to despair for ever using the word “category” again without a 
modifier. The notion of “precategory” is pretty weird in the standard 
model: Why should the notion of an infinity-groupoid with a family of 
hom-sets be the sanctified notion?! Of course it turns out to be a useful 
notion, just like group presentations are useful. But group theory is about 
groups, not group presentations.


-- 
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 #1.2: Type: text/html, Size: 3210 bytes --]