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

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

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

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