[UniMath] some thoughts

[Vladimir Voevodsky]

About the naming of categories (cf. issue #362 in UniMath).

In the theory of infty-categories, (infty,1)-categories with hom-sets are called 1-categories or (1,1)-categories.

We currently call them Precategories. I do not like the current name since it is completely non-descriptive. It is, however, easy to replace with anything else, which is why I agreed to it in the first place. Our current "precategories" are (infty,1)-categories with only one layer of associativity and identity conditions imposed (and without the univalence condition).

We recently extended "assoc" etc. to binary operations on general types. We will soon have assoc and assoc2 (the pentagon). The latter will be used for example in the definition of monoidal categories (attn. @AnthonyBordg).

We will soon have (infty,2)-categories as precategories with additional structure - among which will be the the analogs of the assoc2 for multi-object composition.

The levels/layers in the concept of a general (infty,infty)-category are complicated.

a. There is firstly, how many levels there are of morphism types that are different of the equality types. (infty,0)-category has 0 levels, that is, it is simply a type. (infty,1)-category has 1 level. (infty,2) has 2-levels and (infty,159) has 159 levels.

b. There is secondly, how high an h-level may have the types of objects and the types of morphisms on each level where they may be different from equalities. For what, I think, people in the set-theoretic maths call (infty,d)-category it is a sequence of (d+1) numbers (l_0,...,l_d) where (2,...,2) corresponds to a d-category where objects and morphisms of all levels form sets.

So we should have a number d, including infty, and a list of d+1 numbers, also including infty. To comply with the convention of the set-theoretic maths we should write the length of the sequence after the sequence itself.

For example, the type of the ((0,2),1)-categories is equivalent to the type of sets with monoidal operation. As set-theoretic maths suggest, the type of the ((0,...,0,2),d)-categories for d>1 is, independently from d, equivalent to the type of sets with a commutative monoidal operation.

c. There is, thirdly, how many levels of the associativity and the left and right unity conditions as well as mixed associativities are added for each composition. The combinatorics of this part of the structure I do not yet know.

Going back to Precategories and ignoring for now the unsolved problem (c) we see that they should be called ((infty,2),1)-categories. Indeed, no restriction on the type of objects is imposed (infty), types of morphisms are sets (2) and there is only one level of morphism types where they differ from the identity types (1).

For now, until a solution for (c) is found, Precategories is fine to me.

Vladimir.

--
You received this message because you are subscribed to the Google Groups "Univalent Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to univalent-mathem...@googlegroups.com.
To post to this group, send email to univalent-...@googlegroups.com.
Visit this group at https://groups.google.com/group/univalent-mathematics.
To view this discussion on the web visit https://groups.google.com/d/msgid/univalent-mathematics/59E715A6-B4A8-486E-9372-E6CFA525FB9E%40ias.edu.
For more options, visit https://groups.google.com/d/optout.

[Michael Shulman]

Thanks for bringing this up, this is an interesting discussion to
have. I think the original intent of the "pre-" in "precategories"
was to indicate the absence of the univalence condition, not the
absence of higher associativities. In fact, because the homs are
sets, I don't see that any nontrivial higher associativities can be
asked for, can they?

Because of the absence of univalence, I would not agree that these are
what in the theory of oo-categories are called (oo,1)-categories with
hom sets or 1-categories. Specifically, when interpreted in the
simplicial set model, the type-theoretic notion of precategory does
not yield a theory equivalent to that of ordinary 1-categories, but
the notions of strict category (a precategory with a set of objects)
and univalent category both do.

I certainly agree that the term "precategory" could be better. There
is a notion in the theory of oo-categories based on set theory that
*does* correspond to type-theoretic precategories, namely non-complete
Segal spaces with hom-sets, also known as a "flagged oo-category"
(https://arxiv.org/abs/1702.02681) with hom-sets. I suppose we could
appropriate the latter word and call them "flagged categories", or
maybe "oo-flagged categories" to indicate that the type of objects has
no h-level restriction.

In general, an (m,n)-category (n dimensions of morphisms that are not
invertible, with hom-(m-n)-types at the top) could I guess be flagged
separately in all (n+1) dimensions, so we could talk about
(l_0,...,l_n)-flagged (m,n)-categories. This is very like your
proposal, but I think that the presence of absence of univalence is
the most important thing to indicate, since that is the most
significant departure from the terminology in the set-theory-based
theory of oo-categories. Suppose we write "u" in place of a number to
indicate univalence at that dimension (i.e. "unflagged"); of course
this determines the h-level of that dimension, at least if the higher
dimensions are also univalent, but does more than that. Then we would
have:

precategory = (oo,u)-flagged (1,1)-category
univalent category = (u,u)-flagged (1,1)-category
strict category = (0,u)-flagged (1,1)-category (or (2,u)-flagged if
you prefer h-level numbering)
monoid = (-2,u)-flagged (1,1)-category
commutative monoid = (-2,-2,u)-flagged (2,2)-category = ...
monoidal univalent category = (-2,u,u)-flagged (2,2)-category

(It is a nice observation that flagging with contractible types
implements the degeneration of higher structures into monoidal lower
structures from the "periodic table of n-categories"! I had not
thought of that before.)

If one wants to consider structures that have hom-types that aren't
sets but don't have all the higher associativities that ought then to
be required of an (m,k)-category, one natural terminology would be
"A_n category", since in algebraic topology A_n is used for algebras
over operads that have associativity (and unitality, although in their
case that is often strict) up to n-ary operations but no higher.

> 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 HomotopyTypeThe...@googlegroups.com.