# Universes in Type Theory Part I

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?

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$^{\omega}$ 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!