[Agda] Re: eta expansion

[Martin Escardo]

On 20/03/13 13:27, Altenkirch Thorsten wrote:

> The universes in Agda are open hence they don't admit an induction
> principle unlike the closed universes defined by induction-recursion. As
> a consequence all you can do a with type in a universe is extensional
> you cannot investigate how are the built. This is reflected by the
> univalence principle.

I agree with the view that universes are open ended. We know that they 
are closed under certain constructions, but I don't want to say (or 
think) that they are the least thing closed under those operations. Of 
course, in the models, if you care about them, the universes will be 
less open ended, and in some cases they can be defined as the 
least-thing. But although I like models for several reasons, I also like 
to take type theory as a foundational system (competing with set 
theory), where my model is just a mental, intuitive one, and in this 
view my universe may grow if I please, and more than that, it may have 
things I am not aware of. Moreover, like all types, universes may have 
plenty of non-syntactically-definable stuff. A weakening of univalence 
is that any two isomorphic types have the same properties (or, put in 
another way, any property of types is extensional, in that it has the 
same value for any two isomorphic types). Univalence is the proper way 
of stating that.

Of course, I am not forbiding any one of working with inductively 
defined universes (and codes for the elements of the universe), and in 
fact this can be done in Agda, and for some purposes I may wish to use 
such inductively defined universes (maybe as HIT's as propoposed 
earlier). But this is another universe, different from Set0, Set1, Set2, 
... (the terminology Set for universes is probably not very good, 
because its elements may not be hsets, but this is what Agda syntax has).

Martin