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: deprecated: logic

Topic: Dependent universes?

Tim Campion (Oct 29 2022 at 19:43):

In dependent type theory with universes, each universe is typically taken to be a type in the empty context. Has anybody ever explored a notion of "universe" which allows one to have certain "universes" which only make sense in certain non-empty contexts?

I'm not sure what an example might be -- I'm asking partly because I'm curious if anybody has ever found a motivation to study such a thing!

Tim Campion (Oct 29 2022 at 19:43):

Here's an attempt at an example. Consider a dependent type theory for modal reasoning. Let's say that among the types available for you are certain "types of possible worlds". For simplicity, maybe there's just one type $\dashv W$ whose terms are the elements of some Kripke frame or something. Then maybe you could have, in the context of a possible world $w: W$, a dependent universe $w : W \dashv \mathcal U(w)$ where a term of $\mathcal U(w)$ is some kind of type which only makes sense to talk about in the context of the possible world $w$.... This doesn't sound so convincing so far -- it seems like right now $\mathcal U$ could be formalized as an ordinary universe which simply has different terms in the context of different possible worlds, as one would expect. To make it more interesting... what if the rules for universe formation can vary between the possible worlds? Like, maybe in the empty context there is only one universe, but in some possible worlds there is a "successor" operation on universes which spawns some possible-world-dependent hierarchy of universes....

Tim Campion (Oct 29 2022 at 19:49):

Here's another attempted example. Think about algebraic geometry, and specifically about motivic homotopy theory. The $\infty$-category $H(S)$ of motivic spaces over a base scheme $S$ is locally cartesian closed, but is typically not an $\infty$-topos -- descent fails. However, there are _some_ universes in $H(S)$. These are various "moduli stacks" parameterizing different classes of motivic spaces. I'm not an expert, but I would guess that probably the question "which classes of motivic spaces in $H(S)$ are parameterized by a moduli stack?" (i.e. "what universes exist in $H(S)$?") will have an answer which _depends_ on $S$. So you could maybe imagine a type theory where the types are roughly motivic spaces, and where the context can include a "base scheme" $S$ (or maybe more generally a "base motivic space"). Then depending on this contextual factor (which base scheme you're working over), the rules for universe formation might vary. So you might end up thinking in terms of "universes" which only make sense in certain contexts.

Tim Campion (Oct 29 2022 at 19:51):

Anyway, whatever motivation one might have, I guess my questions are:

1. Is it clear what should be encompassed by a theory of "dependent universes"?

2. Has anybody written about a theory of "dependent universes"?

3. Is there some good motivation to explore such a notion (whether along the lines of my attempted examples, or otherwise)?

Morgan Rogers (he/him) (Oct 29 2022 at 19:52):

[Obligatory joke about these being objects of study in some possible world]

Morgan Rogers (he/him) (Oct 29 2022 at 19:55):

The motivic spaces example certainly looks like compelling motivation to me, I'm sure someone can run with that. I would be (pleasantly!) surprised if dependent universes have already received attention, although I'm by no means the person who would know if that were the case.

Tim Campion (Oct 29 2022 at 19:56):

I guess you could also do something like the following. Maybe your theory includes a type $T$ of "witnesses that the Grothendieck universe axiom holds". In the context of some $t:T$, you can now form a whole bunch of new universes which you couldn't in the empty context (assuming that there's no closed term of type $T$). Maybe you could even find yourself mapping the territory of the set-theoretic multiverse with some framework like this...

Mike Shulman (Oct 29 2022 at 21:27):

What about plain universe polymorphism? $i : \mathsf{Level} \vdash U_i$. Universe levels aren't always actually variables in a context, but I think in Agda there is actually a type of levels (which belongs to the $$\omega$$th universe).

John Baez (Oct 30 2022 at 17:20):

(Annoying fact: putting some text like "th" right after math in dollar signs makes the dollar signs not work here!)