[Agda] eta expansion

[Vladimir Voevodsky]

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?

Vladimir.