[Agda] eta expansion

[Peter Hancock]

On 09/03/2013 12:31, Vladimir Voevodsky wrote:
>
> On Mar 9, 2013, at 2:10 AM, Peter Hancock wrote:
>
>> 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.
>
> Univalent universe should probably be defined as a higher
> inductive-recursive type. If one uses a straightforward
> inductive-recursive construction of a universe how does one ensure
> that two definitionally equal type expressions define the same point
> in the universe?

Induction recursion does not forbid different syntax for the semantically same thing (eg set).
Dan Licata made this point.  It might be good to define
syntactical equality so that this didn't happen, or there is
a normal form theorem, if possible.

May I ask a naive question that puzzles me?  In type theory, there is no
constructor making types A = B from types A and B.  There is only
the type a =_A b between objects of type A.  So how to express the univalence axiom
in type theory?  If I understand it, this says that
a certain map f : A = B -> .. has contractible fibres.  But we don't have
equality between types, only between objects in types.  Even to write down
the univalence axiom, we need a binary type-constructor, or to define a
type as an object u : U in a universe (U,T) having some kind of normal form theorem.

Peter