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

[Michael Shulman <shulman@sandiego.edu>]

On Wed, Nov 7, 2018 at 6:05 AM Peter LeFanu Lumsdaine
<p.l.lumsdaine@gmail.com> wrote:
>> 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”.

This is a really interesting question.  Traditional category theorists
do of course consider FinSet_N to be a category; in particular, it
*is* a category according to the definition of "category" in ZFC.

One could view this situation as analogous to that of truncated and
untruncated Sigmas.  When formalizing mathematics in ZFC, there are no
untruncated Sigmas.  When formalizing mathematics in MLTT, there are
no truncated Sigmas.  But when formalizing mathematics in HoTT, we
have both truncated and untruncated Sigmas.  We used to ask the
question "when formalizing mathematics in HoTT, should the quantifier
'there exists' be interpreted as a truncated Sigma or an untruncated
Sigma?"  (This is what led to the somewhat-awkward use of the word
"merely" in the book.)  But more recently a number of us seem to
believe that that's the wrong question, as it presupposes that
mathematics has *already* been interpreted into first-order logic,
which destroys the *natural* distinction between truncated and
untruncated Sigma.  Instead we should directly interpret mathematics
into HoTT, choosing truncated and untruncated Sigmas as appropriate
for the mathematics, without feeling the need to pass through
first-order logic.

Similarly, when formalizing category theory in ZFC, there are no
univalent categories, only strict ones; thus we have to carefully
ignore the strictness when working with categories that "should" be
univalent.  I don't know if there is any foundational theory in which
*all* categories are univalent.  But when formalizing category theory
in HoTT, we have both; and so one might argue that it's wrong to ask
whether the word 'category' should refer to strict categories or
univalent ones, and instead we should use one or the other as
appropriate for the mathematics -- and thus the general word
'category' should refer to something that includes both of them, such
as precategories.

Is that roughly the point you are making, Peter?

I can't deny that there is something to this argument.  However, I
have two objections to it, or at least to its conclusion.  The first
is that the analogy breaks down in the following way.  The awkwardness
of formalizing mathematics in first-order logic comes from
*conflating* truncated and untruncated Sigmas.  Thus, the problem is
solved in HoTT by simply distinguishing them.  However, the
awkwardness of formalizing category theory in ZFC comes not merely
from conflating strict categories with univalent ones, but because
doing category theory with strict categories is *intrinsically*
awkward, whereas most applications of category theory involve only
univalent categories (or more precisely, categories that *should* be
univalent), so that awkwardness shouldn't be necessary.  I think this
is Eric's point: doing category theory with univalent categories is
*nicer* than doing it in ZFC, whereas doing category theory with
strict categories is *no better* than doing it in ZFC.  Why wouldn't
we want to emphasize one of the "selling points" of HoTT in our
terminology?  The strict categories are still there whenever we need
them, but giving them a slightly derogatory red-herring adjective is
appropriate because they are, for the most part, less well-behaved,
and not what the subject of "category theory" is primarily about.

My second objection is to the jump from "something that includes both
strict and univalent categories" to "precategories".  One can argue
that traditional category theorists have a notion of "category" that
includes both strict categories and univalent categories, but I would
argue that their notion does *not* include precategories *other* than
strict and univalent ones; instead it is something more like the
"union" of strict categories and univalent categories, which is much
smaller than the world of precategories.  As evidence, I suggest that
to a traditional category theorist, the statement "a fully faithful
and essentially surjective functor is a (strong) equivalence" is
either "just true", "becomes true if you set up the definitions
correctly", or "becomes true if you assume the axiom of choice"
(depending on the particular category theorist's attitude towards the
axiom of choice).  In HoTT, this statement for univalent categories is
"just true" without any axiom of choice (one way in which doing
category theory with univalent categories is nicer), while this
statement for strict categories is related to the axiom of choice in
exactly the same way as it is in ZFC.  But this statement for general
precategories is *just false*!!  This is easy to see: let Y be any
type, considered as a univalent groupoid, let f : X -> Y be any
surjection of types, and make X into a precategory in the unique way
such that f becomes a fully faithful functor.  Then f is also
essentially surjective, but for it to be an equivalence the surjection
f must have a section; and there are plenty of surjections of types
that have no section, such as the inclusion of the basepoint of S^1.
So precategories are really weird, and if we define the word
"category" to mean "precategory" then category theorists learning
about HoTT will see things like this and react "whoa, category theory
in HoTT is really weird" -- whereas the correct reaction (when using
univalent categories) is "whoa, category theory in HoTT is really
awesome"!

Moreover, as Ulrik pointed out, there is a notion in traditional
(higher) category theory that (under the standard interpretations of
HoTT) does coincide with precategories.  They're called "flagged
categories": https://arxiv.org/abs/1801.08973.  In particular, they
are *not* called just "categories"!  This to me is additional strong
evidence that the traditional category theorist's notion of "category"
does not include precategories.  So if we in HoTT used "category" to
mean "precategory", then we would actually be *renaming* something
that already exists in traditional mathematics, in a highly confusing
way.

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