[Agda] Induction-recursion, indexing and universes.

[Dan Doel]

Greetings,

After reading some of Peter Dybjer's work on (induction and) induction-
recursion, I was inspired to fool with some universes in Agda. To my surprise, 
I was able to construct a hierarchy of universes quite like the one I 
implemented by hand to experiment with my understanding of Agda's universe 
polymorphism, and the construction fits entirely in Set, to boot (induction-
recursion is, as I'm sure many know, quite powerful).

But, I hit a few snags along the way, and have an associated question or two. 
First, I decided to try adding descriptions of inductive datatypes a la 
Epigram 2 (although I used the simpler definition from Peter Morris' paper). I 
already had W-types, but I'm greedy (and I don't think it's possible to 
successfully define observational equality mutually with the universe; this 
may be related to the late-instantiation-of-metavariables issue, I'm not 
sure). Distilled to its essence, my approach looked like:

  data Desc (U : Set) (T : U -> Set) : Set where
    arg : (s : U) (f : T s → Desc U T) → Desc U T

  data Mu (U : Set) (T : U → Set) (D : Desc U T) : Set where
    -- we don't need constructors to blow up

  mutual
    data U : Set where
      mu : Desc U T → U

    T : U → Set
    T (mu D) = Mu U T D

but this gets complaints about U not being strictly positive, due, I believe 
to the U in Mu U T D. So, that was a bust (T also won't pass the termination 
checker).

Another idea I had along the way, was that it's less than satisfying to define 
the hierarchy using a universe formation operator like so:

  module Form (U : Set) (T : U → Set) where
    mutual
      data U' : Set where
        u  : U'
        t  : U → U'
        1' : U'
        -- etc.

      T' : U' → Set
      T' u     = U
      T' (t s) = T s
      T' 1'    = ⊤
      -- etc.

which lets us establish the hierarchy as:

  mutual
    U : ℕ → Set
    U zero    = ⊥
    U (suc n) = U' (U n) (T n)

    T : (n : ℕ) → U n → Set
    T zero    ()
    T (suc n) s  = T' (U n) (T n) s

This works, but for instance, it includes (n + 1) unit types in every level; 
one via 1', and n via cumulativity (universe 0 contains 1'; 1 contains 1' and 
t 1'; 2 contains 1', t 1' and t (t 1'); ...). A more satisfying definition of 
the hierarchy would be to define an indexed family:

  mutual
    data U : ℕ → Set where
      1₀ : U 0
      u  : (n : ℕ) → U (suc n)
      t  : {n : ℕ} (s : U n) → U (suc n)
      Π  : {n : ℕ} (s : U n) (f : T s → U n) → U n
      -- etc.

    T : {n : ℕ} → U n → Set
    T {0}     1₀    = ⊤
    T         (u n) = U n
    T {suc n} (t s) = T s
    T         (Π s f) = (S : T s) → T (f S)
    -- etc.

Of course, this doesn't work, again due to complaints about strict positivity, 
and U appearing on the right-hand side of T. But it isn't in principle absurd. 
In induction-recursion, we assume that we have constructed s : U, and thus 
have license to use T s when building additional elements. Here, our 
definition (I think) satisfies the invariant that for T {suc n} s only relies 
on s : U (suc n) and U n already being defined. So, we might conceivably be 
able to find criteria for definitions where T is allowed not just to do 
recursion over a mutually defined U, but over an index n of U n.

Then it occurred to me that I had a paper by Peter Dybjer and Anton Setzer 
entitled Indexed Induction-Recursion, and lo and behold, it talks about 
exactly this idea, and lay out what sort of definitions are acceptable (and 
even mention that Agda 1 apparently had a form of it). At least, I'm 
relatively sure the content of their paper would allow my definition, as it 
seems similar to one of their examples of IIRDs.

In fact, I think indexed induction-recursion would actually solve the problem 
with inductive descriptions as well (unless it falls into the same hole as 
mutually defined observational equality), as we could write a definition like:

  mutual
    data U : ℕ → Set where
      1₀ : U 0
      u  : (n : ℕ) → U (suc n)
      t  : {n : ℕ} (s : U n) → U (suc n)
      d  : (n : ℕ) → U (suc n)
      μ  : {n : ℕ} (D : Desc n) → U n
      -- etc.

    T : {n : ℕ} → U n → Set
    T {0}     1₀      = ⊤
    T         (u n)   = U n
    T {suc n} (t s)   = T {n} s
    T         (d n)   = Desc n
    T         (μ D)   = Mu D
    -- etc.

    data Desc : ℕ → Set where
      arg : ∀{n} → (s : U n) → (T s → Desc n) → Desc n
      -- etc.

    data Mu {n : ℕ} (D : Desc n) : Set where
      -- whatever

Which appears to be an admissible IIRD, no longer has U and T in the types of 
Desc and Mu, and no longer has a T that will fail the termination checker.

So (assuming I've understood IIR), has there been any thought given to 
extending Agda's induction-recursion to indexed induction-recursion? I must 
admit, the theory looks much more difficult than what I've gleaned of normal 
induction-recursion from Peter Dybjer's other papers (although, the IIR paper 
seems to focus a lot more on the actual semantics, where the IR papers focused 
on axiomatizing the admissible definitions), so perhaps it's too much pain for 
too little gain. But it'd be an interesting tool to have available.

Cheers,
-- Dan