Okay now we’re getting back to working on reading papers and all that. So let’s get back into the swing of things with Erik Palmgren’s paper On Universes in Type Theory. I’ve skimmed this paper before but I barely remember any of it, so let’s try and do a better reading, shall we?

First, I want to try and work out why I’m interested in this paper. I’m trying to understand type theory from the more mathematical/foundational view, rather than just from the “how does this work as an implemented theorem prover” perspective that I mostly have right now. I think the fact that I’ve been teaching foundational CS to undergrads for the past nine months has made me realize that there’s a lot of foundational questions about type theory I don’t understand. Of the possibly uncountable set of things I don’t understand, I think making sense of what universes really buy you is one I’m really interested in and it fundamentally ties in with understanding a bit better What HoTT Really Is. I’ve read through most of their textbook before, and I’m currently working on formalizing chunks of it myself in Agda to better get it. On the other hand, whenever the HoTT mailing list gets into deep discussions about the model theory or foundational aspects of things I get lost quickly. There’s a lot of reading I want to do in order to catch up this summer, but I figured why not start with writing about a few papers that are about non-univalent type theory while I beat my head against the model theory of HoTT.

In particular, this paper is about how to extend the power of universes by constructing what they call a “super universe”, which is a universe that contains all of the universes in the normal countable hierarchy as elements *and* contains some transfinite universes. I have *no* real intuition for what transfinite universes are useful for and if that’s something that’s present in any actual implementations of theorem provers. If anyone has answers to those questions, I’d certainly love to know! I mean, the only thing that I can really think of is that a super universe would be similar to having a closed universe with descriptions where the universes themselves have descriptions, which a colleague of mine has worked on. There are surely other uses for the kinds of things describeable by a super-universe, but I’m not aware of it from the programming-in-type-theory perspective.

So, just as a brief introduction to the idea for the non-type-theorists in the room we have that universes are a way to abstract over types themselves. If we consider a function such as the identity function `f x = x`

in a polymorphic language such as Haskell or ML, it will have the type `a -> a`

with an implicit “for all a” at the beginning of the type. This allows the identity function to operate over all possible types since it has uniform behavior over all possible types. Now, in something like Martin-Lof type theory the way you play this particular game is to have a universe such as `Set`

in Agda that allows you to write the polymorphic identity as `(A : Set) -> A -> A`

, which rather than having the polymorphism be implicit allows us to say exactly what we mean. In this way, we are treating types and terms on a bit more equal footing in that indexing over a type is really just indexing over the *terms* of type `Set`

which are the codes. Of course this doesn’t just buy us a form of polymorphism but a well-formed notion of type-operators like in System F since `Set`

is a type and thus we can have functions such as `Set -> Set`

or `(A : Set) -> A -> Set`

etc. to describe our more complicated type families. We also want to be able to define type families recursively over data, which are going to have the form of `A -> Set`

for some `A`

, i.e. that for every element of `A`

we need to return a *type*. Please note, though, that even though I make comparisons to System F and its extensions that this is an *entirely predicative* view of types unlike those systems.

Now, of course, these types aren’t entirely first class (yet) since certainly `Set -> Set`

can’t be an element of `Set`

as `Set : Set`

means that we already have an inconsistent universe (author points at blog title, does “jazz hands”) by an argument akin to Russel’s paradox. In order for them to be on the same footing as other types, we need to introduce a type that is larger than `Set`

. In Agda this is `Set 1`

. The natural hierarchy you’d expect of sets of sets of sets to happen, and that pretty much brings us to the review of universe hiearchies that starts this paper which I’ll actually start next time!