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:


  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


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

  • $\begingroup$ Are you trying to have more than Nat-many universes? It is not clear what you are asking. $\endgroup$ Dec 29, 2016 at 15:06
  • $\begingroup$ The paper seems to do that. $\endgroup$
    – 盛安安
    Dec 29, 2016 at 15:09
  • 1
    $\begingroup$ I know what's in the paper. What are you trying to do? What is your question? $\endgroup$ Dec 29, 2016 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, 2016 at 15:17
  • $\begingroup$ I want to know the intention of generalizing universe construction to a binder. $\endgroup$
    – 盛安安
    Dec 29, 2016 at 15:19

1 Answer 1


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!

  • $\begingroup$ Do you identify the $\mathbb{N}$ in the universe with the traditional meta-theoretic index level? $\endgroup$
    – 盛安安
    Dec 30, 2016 at 5:25
  • $\begingroup$ I guess the answer is indeed "yes" $\endgroup$
    – 盛安安
    Dec 30, 2016 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$ Dec 30, 2016 at 20:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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