[Agda] complex indices

[Brandon Moore]

> Yes but I think the return type in my example was Set.
> Note, for example, that this is allowed:

>  bar : Bool → Set1
>  bar b = Set

>  data foo : let x = true in bar x where
>    baz : foo

Here bar computes down to Set.

More generally, it works if there are also
some arguments. This can be useful for abbreviating
complicated definitions. It's probably more useful
for abbreviating constructor types rather than the
type of a new data type, but this does typecheck:

module test where
open import Data.Nat

Rel : Set → Set₁
Rel A = A → A → Set

data Term : Set where

data NStepReduction : ℕ → Rel Term where