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.