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

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

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

I'm a bit confused by your message, Peter: HoTT doesn't have a naive set 
interpretation and is inconsistent with UIP, so I'm not sure how that 
should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)

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

On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine 
wrote:
>
> Ulrik’s email nicely lays out the three key notions (pre-category, strict 
> category, univalent category), and the argument for the 
> Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning 
> “univalent category” by default.
>
> For my part I lean the other way: I think it’s too radical to use 
> “category” for a definition which doesn’t come out equivalent to the 
> traditional definition under the naïve set interpretation (or under the 
> addition of UIP to the type theory).  Choosing terminology that actively 
> clashes with traditional terminology makes it much harder to compare 
> statements in HoTT with their classical analogues, and see what difference 
> HoTT really makes to the development of topics.
>
> Based on that criterion, I strongly prefer taking category to mean 
> “precategory”.  A big payoff from this is that if you formalise something 
> using “category ” to mean “precategory” in type theory without assuming UA, 
> then you can read the result either as valid in HoTT, or (under the 
> set-interpretation) as ordinary arguments in classical category theory, 
> with all the terms meaning just what they traditionally would.
>
> Univalence of categories is an important and powerful property, but not an 
> innocuous one; it changes the character of the resulting “category theory” 
> in interesting ways.  Making the restriction to univalent categories tacit 
> is misleading to readers who aren’t fully “insiders”, and obscures 
> understanding its effects.
>
> –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 #1.2: Type: text/html, Size: 2912 bytes --]