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

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

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

On Wed, Nov 7, 2018 at 12:43 PM Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
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?)
>

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.

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

I would argue both are familiar to traditional category theorists.  It’s
not unusual to make use of, for instance, the small model for FinSet where
the set of objects is taken as N — call this FinSet_N, say.  Category
theorists would certainly say that there’s a difference in character
between FinSet_N and FinSet itself: FinSet_N is small; and I think they
would also agree that they’re conscious informally of an extra character
FinSet has, which in HoTT can be precisely expressed as its univalence.

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

–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: 2942 bytes --]