[Agda] Universe construction

[Dan Doel]

On Tuesday 11 January 2011 6:27:32 pm David Haguenauer wrote:
> I'm trying to get a grasp of the ways in which Agda users program with
> higher-level constructs than what the base language provides. It seems
> to me as though universe construction was a hot topic in Agda-related
> circles at some point in the past.
> 
> Are there any examples of significant developments making use of
> universe construction? Or reasons why not?

Universes go all the way back to Martin-Loef (at least). For his type theory, 
he starts with a bunch of type constructors and associated stuff, like:

  Π, Σ, W, +, I, N, N₀, N₁, ...

+ being binary sum, I being identity/equality types, and subscripted Ns being 
finite sets. That gets you a long way. However, none of these constructs have 
a way to eliminate *into* types, so you cannot define types by case analysis 
on values (and this, for instance, prevents you from proving that false is 
distinct from true as boolean values). To rectify this, he defines the 
primordial example of an inductive-recursive universe:

                s : U       s : U    t : T s → U
  --------    ----------    --------------------   etc.
  U : Type    T s : Type          π s t : U

This universe contains codes π, σ, w, +, n, n₀, n₁, ... (I don't have a better 
name for small +). Using this, we can define functions targeting codes by 
recursion, and since T interprets codes into types, we can define types by 
recursion. You can also go beyond this, and assume further universes U_(n+1) 
and interpretations T_(n+1), which have codes u_n for U_n, and t_n, lifting 
codes in U_n to codes in U_(n+1) (in addition to the others).

The ultimate generalization of this is to allow arbitrary inductive-recursive 
definitions in your language. Then you can define all these universes as a 
special case.

However, Martin-Loef used this style of definition to enhance the strength of 
his type theory to having large eliminations. Agda has this natively, 
essentially. There is already an infinite hierarchy of universes SetN, and we 
can write functions that target these universes, using the names of types 
directly, instead of codes as a proxy:

  f : Bool -> Set
  f true  = ⊤
  f false = ⊥

Using a more ML-like setup, this is:

  f : N₂ -> U
  f 1 = n₁
  f 0 = n₀

So, while it's interesting to use Agda's support for induction-recursion to 
play with the Martin-Loef sort of setup, it isn't as necessary, because Agda 
includes a lot of the features that these universes would otherwise add to the 
theory as built-ins.

The utility in Agda thus falls to other things. For instance, maybe you want 
to work with a specific subset of 'all types.' Then you can define a type of 
codes for exactly which types you want to work with, and an associated 
decoder. Or, as mentioned in the other reply you got, lots of types can 
theoretically fit into the "set of codes and a decoder into types" view. In 
fact, I believe this is how you get general indexed families (without the nice 
programming style) in something like ML type theory (or UTT), hence the "(ℕ, 
Vec A)" example.

-- Dan