Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: universe sizes

view this post on Zulip Jacques Carette (Aug 21 2021 at 13:48):

In a different thread:
Mike Shulman said:

You're saying that the type of E-categories can be parametrized over three unrelated universes, for the types of objects, morphisms, and equalities respectively, and that the slice/comma construction doesn't act on such E-categories leaving all the universes fixed. So it could either be an endomorphism of (in Coq notation) ECat@{i j k} with extra constraints k <= j <= i, or it could take input in ECat@{i j k} and yield output in ECat@{max(i,j) max(j,k) k}.

I suppose I would argue that one should always impose the constraint k <= j <= i.

Hmm, I now have serious doubts about the latter. Let's just consider i and j for objects and homs (locally).

  1. for 1-object categories, we can take i to be 0, and j can be as large as we want
  2. we can also have discrete categories, with i as large as one wants, and j can be 0.

So it appears to me that they really ought to be completely independent from each other.

view this post on Zulip Mike Shulman (Aug 21 2021 at 13:55):

Well, there's a one-element set in every universe, so 1-object categories can also fit in j <= i.

view this post on Zulip Jacques Carette (Aug 21 2021 at 13:59):

If you're allowing yourself to modify the native universe that objects live in by injecting them into something large enough (like, say, j), then yes, of course. That doesn't feel... elegant?

view this post on Zulip Mike Shulman (Aug 22 2021 at 00:03):

Isn't your unit type universe-polymorphic?