> Perhaps somebody should add a Coq "version from scratch" of this.

If you just want a straightforward transcription of the Agda code, I've
made one here:
https://gist.github.com/JasonGross/c6745e6d3ffbab3ee7034988c1b5b904

Feel free to adapt it as you desire, and use it with or without crediting
me.
The only "design decisions" of note are:
1. Making sigma types a record with primitive projections and eta is needed
to get Coq's "compute" to use projections in the normal form, rather than
"match"
2. I used "Opaque J" so that running reduction wouldn't print "match"
statements on the Id type.
3. I added a definition "isUnivalentAt" defined so that "isUnivalent := (X
Y : U) -> isUnivalentAt X Y", because I wanted to only pass universes in
the definition of isUnivalent, in a way that induced minimal clutter
4. I added some notations in "Module Short." to suppress printing of types,
to match your normal form with types elided.

-Jason

On Wed, Mar 7, 2018 at 4:10 PM Martín Hötzel Escardó <
escardo...@gmail.com> wrote:

> I have often seen competent mathematicians and logicians, outside our
> circle, making technically erroneous comments about the univalence axiom,
> in conversations, in talks, and even in public material, in journals or the
> web.
>
> For some time I was a bit upset about this. But maybe this is our fault,
> by often trying to explain univalence only imprecisely, mixing the
> explanation of the models with the explanation of the underlying theory
> (MLTT, identity types, universe), with none of the two explained
> sufficiently precisely.
>
> There are long, precise explanations such as the HoTT book, for example,
> or, the formalizations in Coq, Agda and Lean.
>
> But perhaps we don't have publicly available material with a
> self-contained, brief and complete formulation of univalence, so that
> interested mathematicians and logicians can try to contemplate the axiom in
> a fully defined form.
>
> Here is an attempt to rectify this:
>
>   https://arxiv.org/abs/1803.02294
>
> 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.
>
> There is also a web version of this (
> http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html) to try
> to make this as accessible as possible, with the text and the Agda code
> together.
>
> M.
>
> --
> 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.
>