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

[Erik Palmgren <palmgren@math.su.se>]

Setoid hell? This sounds like a sermon ... :-)  I think the critique 
needs to be a little more specific.

Den 2018-11-07 kl. 12:51, skrev Ulrik Buchholtz:
> 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 
> <mailto: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.