[Agda] eta expansion

[Peter Hancock]

A word are two about (2), touching also on (1).

> (2) Inductive "data" types take us well beyond what we can do with
> W-types in MLTT. This is good, but on the other hand not well
> understood, and not guaranteed to be consistent. It would be good to
> have a pragma W that only allows data definitions that can be
> (automatically) translated to W-types (and/or well-understood
> generalizations). Id types should be treated separately, as well as
> Sigma types (?). I don't believe in the generality of the "data"
> concept that allows Id, Sigma and W, and many more things, under the
> same umbrella.

Induction-recursive definition (a la Dybjer-Setzer) subsumes W-types.
It is a strictly stronger principle.  Insofar as one can "justify" these things,
it is constructively justified -- perhaps the most convincing thing one
can say is that it can be modelled in quite weak systems of set-theory,
namely Kripke-Platek set theory plus a (recursively) Mahlo cardinal.
(No one has ever written this down.  It should also be said that some
of the details of induction-recursion are a matter of mild controversy.
On the other hand, if you think carefully about IR, once you see what
it is, the principle makes good intuitive sense.  Anton Setzer and
Reinhard Kahle have published an attempt to justify yet stronger principles than
induction-recursion.)

Using induction recursion, one can define universes, by far extending the
omega-tower of universes that people find so totemic.  For example, one
has the superuniverses of Erik Palmgren, iterations of that idea, and
universes of universe operators of higher type, ad infinitum.

The universes one gets from IR support eliminators that allow one to
distinguish (codes for) isomorphic types.  I do not know if this
should be considered to shed rain on Voevodsky's parade.  I doubt it.

Discussions about universes are bedevilled by a widespread misunderstanding
of the difference between universes that are *sets*, and *the* universe of
sets.  Funnily enough this misunderstanding does not really occur in
the context of conventional epsilon-based set-theory, where the concept arose.

Induction-recursion is a tricky idea. Yet, it is a *single* principle, in its
own way quite elegant, that subsumes *all* the zoo of data types that we
have learned to love and/or loathe in type-theory.  It ought to be more
widely known.  By the way, it is far from a new principle.  Arguably, the
first published example of its use occurred in the early 70's (in a normalisation
proof by Martin-Lof).

Hank