[Agda] Re: eta expansion

[Peter Hancock]

On 20/03/2013 13:27, Altenkirch Thorsten wrote:
>
>
> What interests me is that you are using a universe, albeit a sacred
> universe of Agda privileged with a silent decoding function.
>
> The universes in Agda are open

That's precisely why they are (or the first one is) so useful
to represent the ground family (Set,El) of a logical framework.
One very badly does not want El to be defined by recursion.

One also badly needs throughout mathematics universes that are
*least* closed: for example the Borel-sets.  Why on earth should
one deprive oneself of the right to define the smallest universe
closed under such and such?  Nobody forces you to use the recursor.

  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.

About univalence, the impression I get is this.  There is a perfectly
good binary operation on sets, namely WE(A,B).  Voevodsky recommends
defining equality on Sets to be this relation.  Nothing will go wrong,
and equality will behave as expected, and even better.

It seems crucial that Set is open.  I wouldn't recommend it for
closed universes in Set.

Hank