Raghu, perhaps you want
  Set Universe Polymorphism.
  Definition univalence@{U U'} : Type@{U'} := forall X Y : Type@{U}, ...
or alternatively
  Universe U.
  Definition univalence := forall X Y : Type@{U}, ...
?

On Fri, Mar 9, 2018 at 12:00 AM N. Raghavendra <ra...@hri.res.in> wrote:

> At 2018-03-07T13:10:53-08:00, Martín Hötzel Escardó wrote:
>
> > This also has an ancillary Agda file with univalence defined from
> > scratch (without the use of any library at all). Perhaps somebody
> > should add a Coq "version from scratch" of this.
>
> I have kept my attempt at a Coq version at
>
>   http://www.retrotexts.net/just-univalence/toc.html
>
> However, I don't know how to define the univalence of a universe in Coq,
> that is, I don't know what to write for foo and bar in
>
>   Definition univalence (U : foo) : bar := baz.
>
> Remarks are welcome.
>
> Raghu.
>
> --
> N. Raghavendra <ra...@hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>