[Agda] eta expansion

[Dan Licata]

On Mar09, 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?
> 
> Vladimir.

I don't think one is required to have this property (El does not have to
be injective).  For example, here is an inductive-recursive universe
with two names for Bool:

  mutual
    data U : Set where
      bool1 : U
      bool2 : U
      pi    : (A : U) -> (El A -> U) -> U

    El : U -> Set
    El bool1 = Bool
    El bool2 = Bool
    El (pi A B) = (x : El A) -> El (B x)

-Dan