[Agda] Universes à la Tarski and induction-recursion

[Dan Doel]

Greetings,

Not long ago, I was gearing up to explain induction-recursion somewhere, and I 
happened upon an (I think) interesting observation, so I thought I'd share it 
here.

It's common (I think) to suggest that the prototypical example of induction-
recursion is Martin-Löf's universe à la Tarski. And indeed, we can define a 
universe with the same codes. In Agda, it looks like:

  mutual
    data U : Set where
      n     : U
      fin   : ℕ → U
      _+_   : U → U → U
      i     : (s : U) → T s → T s → U
      π σ w : (s : U) → (T s → U) → U

    T : U → Set
    T n         = ℕ
    T (fin k)   = Fin k
    T (s + t)   = T s ⊎ T t
    T (i s x y) = x ≡ y
    T (π s f)   = (x : T s) → T (f x)
    T (σ s f)   = Σ (T s) (\x → T (f x))
    T (w s f)   = W (T s) (\x → T (f x))

However, I happened to look back at a set of Martin-Löf's lecture notes from 
the 80s, and I noticed the following: there are no elimination rules given for 
U. And in this sense, the above inductive-recursive universe diverges from the 
original formulation.

Without the elimination rule, the universe behaves much like the built-in 
universes in Agda. For instance, we know that if:

  f : (A : Set) → A → A

then f must be the identity function. We don't know this, however, for:

  f : (a : U) → T a → T a

for the above inductive-recursive universe. f could inspect its first 
argument, and do different things based on its value. However, with the 
original U given by Martin-Löf, we again know that f must be the identity 
function, because no inspection of U is possible. In other words, functions 
(other than T) must be parametric in arguments of type U.

I don't really have any moral to end this up with. I just thought it was 
interesting that the prototypical example of induction-recursion doesn't 
actually appear to match up precisely with actual i-r.

Thoughts?

-- Dan