Continuing where we left in On Universes in Type Theory, we were just getting to the start of defining super-universes. So recalling last time that we had defined an operator for defining universes from a type-family and showed that we could recover the normal universe hierarchy from it as a principled way of defining the inductive hierarchy without needing to have an external indexing (I think?). In order to make a super-universe, we define a new universe as a pair that is closed under all the normal type formers *and* the operator for forming universes from type families. This means that we introduce a new code that is mapped to by whenever and for all and a new code t(a,(x)b,c) for , , and where we have that . The author points out that this super-universe is thus a closed inductively defined structure that has a well defined elimination rule! Cool, okay, so that seems like one of things that’s a big deal here: there’s a more natural notion of induction once we don’t have explicit universe levels. Also, all of the codes in the universes that we normally had in our hierarchy are injected into so, hey, great we haven’t lost anything here.

How, though, does this interaction with having something like an “open” universe where rather than just saying that we’re closed under all the type formers we have a notion of inductive data type mechanism like what we have in Coq, Agda, or even in the formulation of HoTT. I’ll admit there’s something strange to me about this distinction between “open” and “closed” universes in that to my brain the actual *power* of the inductive data type mechanisms is well-defined and thus it’s not like we don’t “know” what all the types are, I suppose it’s more like whether or not all the inductively defined datatypes are inherently enumerable, in a sense? I guess this is one of those moments where there’s distinctions that I’ve heard as lore, like the fact that closed universes are not compatible with the univalence principle, but I don’t understand the pragmatic differences on a truly technical level. I suppose the two main things that occur to me is that you can’t have an elimination rule over the universe unless it’s “closed”, but as far as univalence goes in order to have a closed universe then it would also have to be a higher inductive type that includes all the possible paths between codes, but by univalence the paths between codes are given exactly by the weak-equivalences between types, so maybe this would force some kind of type with an infinite number of introduction rules and that’s where it all falls down?

Alright, back to the paper now the author introduces the notion of a transfinite universe. The basic idea of this section is that we want to define an operator on families that we can “iterate” using the universe construction operator that we considered earlier. What we’ll ultimately do is have a type that’s the total space of a family indexed over and use this to iterate our operator on families an arbitrary number of times. First we consider the type which is the type of all codes for families over . Now this is where the notation got a little confusing for me so I’ll translate it into something I find easier, where the first projection of the sigma is given by and the second projection of the sigma is given by . So now we define as notational shorthand where , i.e. that it’s the base point of the family, and then is a shorthand for the actual fiber over the base point.

At this point, we define our operator over families . What is this doing? Well if we look at it in terms of the and defined above then we get that

okay, so this means that we can repeatedly apply this operator to a code to get the code for a family that corresponds to to building off of the base family with the universe constructor times to get a new universe.

That all being said, then we can then can use *one last time* in order to then define the transfinite universe with base family as . Okay, cool, so the reason why the super-universe let us build this type is that we had a code corresponding to the universe construction operator in the super-universe.

I think I’m going to stop here for now, and maybe move onto reading some other papers while I try to get more familiar with the ideas of proof-theoretic strength that are important to the results of the rest of the paper.