9
$\begingroup$

I'm reading this well-known paper On Universes in Type Theory. At first I expected something similar to Setω in Agda, but it turns out that it's even something more general. It seems to generalize the universe construction from a plain inductive-recursive type to a binder (similar to $\Pi$ and $\Sigma$). The main question I want to ask is, what's the intention behind it?

Here's some Idris code defining usual Tarski-style universes:

mutual

  public export data U : (level : Nat) -> Type where
    GroundU : Ground -> U level
    BinderU : Binder -> (a : U level) -> (b : (x : T {level} a) -> U level) -> U level
    UnivU   : U (S level)
    LiftU   : U level -> U (S level)

  public export T : {level : Nat} -> (code : U level) -> Type

I'm trying to generalize it into something like

mutual

  public export data U : (a : Type) -> (b : (x : a) -> Type) -> Type where
    GroundU : Ground -> U a ???
    ...

What should ??? be? The author of the paper just said universes should be closed under set formers.

edit: I think ??? is simply b ...

$\endgroup$
  • $\begingroup$ Are you trying to have more than Nat-many universes? It is not clear what you are asking. $\endgroup$ – Andrej Bauer Dec 29 '16 at 15:06
  • $\begingroup$ The paper seems to do that. $\endgroup$ – 盛安安 Dec 29 '16 at 15:09
  • 1
    $\begingroup$ I know what's in the paper. What are you trying to do? What is your question? $\endgroup$ – Andrej Bauer Dec 29 '16 at 15:10
  • $\begingroup$ Well ... I came up with an idea that would make use of Setω, so I looked for papers about super universes to see if I can learn something. There are really few papers about it, and this paper is the main one. In order to understand it, I tried to implement it myself. Although now I don't think it would provide insight to my new idea, I still want to understand it. $\endgroup$ – 盛安安 Dec 29 '16 at 15:17
  • $\begingroup$ I want to know the intention of generalizing universe construction to a binder. $\endgroup$ – 盛安安 Dec 29 '16 at 15:19
11
$\begingroup$

One intention behind having a universe operator and a super-universe closed under it, is to give a type-theoretic version of large cardinal axioms known from set theory. An inaccessible cardinal is like a type-theoretic universe. The next interesting kind of cardinal is a Mahlo cardinal. Speaking intuitively, a Mahlo cardinal is one that has "a whole lot" of inaccessible cardinals below it. What would this be in type-theoretic terms? It ought to be some sort of a universe $U$ with lots and lots of universes in it. This is what Palmgren is addressing when he considers super-universes.

There is also a more practical side to having many universes. It is useful to have inductive-recursive types in type theory, for all sorts of purposes. But they let us define new universes, so the question is how many? To get a feel for what Palmgren is doing, instead of shooting for the super-universe right away, try the following sequence of constructions in Agda (using induction-recursion):

  1. Define one universe $U_0$, containing (a code of) $\mathbb{N}$ and closed under $\Pi$ and $\Sigma$. This kind of universe corresponds to an inaccessible cardinal.

  2. Define an operator $U$ which takes any type $A$ and defines a universe which contains (a code of) $A$ and is closed under $\Pi$ and $\Sigma$. This sort of universe operator is akin to Grothendieck's axiom of universes. How many universes can we get by repeatedly applying $U$, starting from $\mathbb{N}$?

  3. To get even more universes, we postulate a super-universe $V$ which contains lots of universes, as follows:

    • $V$ contains $\mathbb{N}$, and is closed under $\Pi$ and $\Sigma$
    • Given (code of) a type $A : V$ and a family $B : A \to V$, there is a universe $U$, which is an element of $V$, it contains all types of the family $B$, and is closed under $\Pi$ and $\Sigma$.

    How many universes does $V$ contain? Note that we can get a family $B : \mathbb{N} \to V$ such that $B(n)$ is the $n$-th universe, and so $V$ must contain a universe $U_\omega$ which contains all of these. And this is only the beginning!

$\endgroup$
  • $\begingroup$ Do you identify the $\mathbb{N}$ in the universe with the traditional meta-theoretic index level? $\endgroup$ – 盛安安 Dec 30 '16 at 5:25
  • $\begingroup$ I guess the answer is indeed "yes" $\endgroup$ – 盛安安 Dec 30 '16 at 5:36
  • $\begingroup$ I used mathematical notation throughout. In ASCII I would write nat instead of $\mathbb{N}$, so it's not meta-theoretic, it's just the type of natural numbers. It doesn't even matter so much that you have nat, I just used it as a base type from which we can get started. If I used bool, you'd be fine as well (except you would have to go one universe higher to get to infinite types, as the first universe would contain only finite types built from bool using $\Pi$ and $\Sigma$). $\endgroup$ – Andrej Bauer Dec 30 '16 at 20:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.