Let me add one more point: in agnostic type theory, we can't define the 
type of (Cauchy) real numbers, so we make do with the setoid of Cauchy 
sequences. Likewise, we can't define the type of (univalent) categories, so 
we make do with the 2-groupoid of precategories, equivalences and natural 
isomorphisms.

In agnostic type theory we are both in setoid and higher groupoid hell. In 
set theory/extensional type theory, we can escape the setoid hell, but 
still have the higher groupoid hell, and in HoTT we can finally escape this 
particular family of infernos :)

On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote:
>
> 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.