Universes in Type Theory Part II

(I’m really experimenting a bit with formatting here because I’m trying to learn what I can do in my org-mode workflow that can actually be rendered properly in a wordpress blog that I ain’t hosting)

Alright, we’re back and we’ll start actually delving into Universes in Type Theory today. So this first section is going to review how hierarchies of universes work. The first real decision point of presentation here is that we’re going to use Tarski-style universes instead of Russell-style universes. Now what on Earth does that mean? It means that instead of something like in Agda where we can define a function like

id : (A : Set) -> A -> A
id A x = x

well then we’re literally using the same symbol A for both the element of Set and the actual type that we use. This could be considered a little bit of a deceit because if I were to try and define my own type that acts like a universe I’d have to do something like

data U : Set where
   b : U
   _-->_ : U

<_> : U -> Set
< b > = Bool
< u1 --> u2 > = < u1 > -> < u2 >

where we have <_> as our denotation function that maps codes in U to types (alright so actually to elements of Set so they’re really just also codes, but ehhhhhhhh let’s go with the fiction for a second).

Whether or not there’s an explicit denotation that maps the codes to types is the difference between Tarksi and Russell style universes. Russell style is when there is the implicit pun between code and type. Tarski style has the explicit mapping between them, often called El in the literature because it gives you the type of “elements” of the set named by the code.

Now as far as I understand, there’s fundamentally no technical difference between these two presentations of universes, although this paper says that Russell universes should be considered a notational shorthand for Tarski universes. Is this claim universally true? Does anyone know?

Alright, all of this being said now we need to consider two ways of presenting the infinite hiearchy of universes: full-reflection vs. uniform construction. What they both have in common is that every level must be closed under all the basic type formers such as \Sigma and \Pi and +, e.g. there are code-level constructors that mean that for codes a and b that are mapped to types A and B respectively then \pi(a,b) is also a valid code and \pi(a,b) gets mapped to \Pi A B by the meaning function etc.

Now, I’ll just say a few words about the full-reflection approach because the author abandons it quickly, but basically it’s the idea that as we build the hierarchy we reflect equality judgments between types as equalities between the codes of the universe. Apparently, it’s simpler to not do that but I don’t entirely understand what that buys you at the moment. Instead, the author goes on to construct the hierarchy of universes and their meaning “functions” (U_n , T_n) inductively by having that, assuming (U_n, T_n) is already defined

  • U_{n+1} \text{ set} : a universe is always a type
  • \frac{x : U_{n+1}}{T_{n+1} \text{ set}} : elements of a universe are always mapped to types by the corresponding type-former that assigns codes to types
  • u_n : U_{n+1}
  • T(u_n) = U_n : this one and the above mean that there is always a code in a universe of level greater than 1 that corresponds to the previous universe
  • \frac{x : U_n}{t_n (x) : U_{n+1}} : there is a code that corresponds to the previous universe’s type former, and it takes codes of the universe down into codes in the current universe
  • $\frac{x : U_n}{T_{n+1}(t_n (x)) = T_n(x)} : this is the, well, commuting-diagram-like-thing that tells us that the applying the “internal” type former and then mapping that to a type is just the same as mapping it to a type directly.

So it looks like those last two rules give us cumulativity, but what else does it buy us? Is it ultimately optional? I think I’m realizing that I know less about the foundational questions of how universes work than I thought.

Alright well in either case we move along to talking about universe operators and super-universes in this next section.

So now we introduce the notion of a universe forming operator that is parameterized by a family of types with the rules

  • \frac{A \text{ set} \, \, \, (x : A) \vdash B \text{ set}}{U(A,(x)B) \text{ set}}
  • \frac{a : U(A,(x)B)}{T(A,(x)B,a) \text{ set}}

and we also introduce special projections for this universe given by

  • *(A,(x)B) : U(A,(x)B)
  • T(*(A,(x)B) : A
  • \frac{a : A}{l(A,(x)B,a) : U(A,(x)B)}
  • T(A,(x)B,l(A,(x)B,a)) = B(a/x)

Okay, so this is way of building a universe from a pair of a type and a family over said type. Now that might seem a little random at first except that, hey, our presentation of the inductive hierarchy is, at every level, a pair of a type and a family over this type which means that we can actually cast all of the rules of our inductive construction as an iteration of this single operation! We define then

  • U_{n+1} = U(U_n,(x)T_n)
  • T_{n+1}(a) = T(U_n,(x)T_n)(a)

and the “internal codes” are defined as

  • u_n = *(U_n,(x)T_n)
  • t_n(a) = l(U_n,(x)T_n,a)

and this satisfies the equations we want because it means that T_{n+1}(u_n) = U_n and that T_{n+1}(t_n(a)) = T_n(a). Cool!

Now that we have a single iterated operation, it’s natural to ask if there’s a way to formulate a universe that is closed under this universe creation operation just as we made a universe that was closed under dependent products, sums, etc. This will be our superuniverse and we’ll pick up on that next post.

One last thought, though, that these are a bunch of rules that kinda make sense to me but I’m really feeling iffy on the semantics of this and that maybe I should find some other papers to convince myself that all these rules are truly sound.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s