Re: [HoTT] Univalence from scratch

[Martin Escardo <escardo...@googlemail.com>]

On 08/03/18 01:37, Jason Gross wrote:
>  > 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

Thanks, Jason. I am sending you a private message with further discussion.

Best,
Martin


> 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 <mailto: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
>     <mailto:HomotopyTypeThe...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout.
>