From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.1.147 with SMTP id 141mr16040079itk.28.1520473088921; Wed, 07 Mar 2018 17:38:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.189.76 with SMTP id x73ls899747ite.4.canary-gmail; Wed, 07 Mar 2018 17:38:07 -0800 (PST) X-Received: by 10.36.176.68 with SMTP id b4mr15585927itj.8.1520473087944; Wed, 07 Mar 2018 17:38:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520473087; cv=none; d=google.com; s=arc-20160816; b=gzG3AJ0alC6tNhvWiHhkSRSjSzVxjAhnCRK7VlwukE2v8DdBeMHNdbW1+HcOCgQEYM OwUdbckSuJd+N7DaJYNebRy0V/C67aHhzX6HXGs1hzpWaVzX4HadljyNmKOo7XkbDFmT OrH1KyKqrZAKymNon5VDaTXjtAAa0S4KclVtGcA+T4Xe46VS+GIBN60oeo0NJKFdBLWx Bc2Y4E9ot+jKaMCkEGf942hc+ITg3U2EAhYLcWGTEBOBeFK9nh4u5UvZFV4KlDVKzfNq z/XUxKmm8mYDbRYEn0zXpdXCNqJcFswi/3Wp1gxw+UGcann28FCMWcRP2LjburY45X6w qHRA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=d7wrCa6gd5GwqCt0LXJ3s8yu2/SnwTkv4ExWO0kglps=; b=ZqGN2tzqNTFvYmFHOsr2Dvbou0jZjupP1NpWwdiycqzrHIUtNe6qzmy9Sl4z7C5OFb nVJBJqWR9ceI1PjIJHGntt1PZc/Okut+jEzRXQT10CQJu4SB1PrvyJnIH/2210ehPFqx tATEX94nBqbA9j7tBv6r3OcTr8om0+fCiNGTafkfUpHDaUKEk/WAqO9gndxcY3MRzRy6 Ack83PgCvRut4KYzhREkHkaSI9HyYFArpxW0h42Dm5i0WAIwqSGj2H3qeRg3Blv7bULG 5Vbg1Vk2XoRiw9Y/u57SVV9GfV4aRkwwDELcV9CnYe+Ep1FC7VDSw6wO0Fg+d4qzd+Zq vFQQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ojLF+yFa; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::241 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x241.google.com (mail-qk0-x241.google.com. [2607:f8b0:400d:c09::241]) by gmr-mx.google.com with ESMTPS id w89si2315270ioe.5.2018.03.07.17.38.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Mar 2018 17:38:07 -0800 (PST) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::241 as permitted sender) client-ip=2607:f8b0:400d:c09::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ojLF+yFa; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::241 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qk0-x241.google.com with SMTP id w142so5050235qkb.8 for ; Wed, 07 Mar 2018 17:38:07 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=d7wrCa6gd5GwqCt0LXJ3s8yu2/SnwTkv4ExWO0kglps=; b=ojLF+yFapQUS2zY9M64293feP1sZ0Ee2ItEDewybobKSZS7/YQQun0gKDD3+FvG+Ef nWSVmGxndJRVHi27/9+F7JUcyRzUobrd6koN8cmlRRjfJ9un0xgymtAD6jWcVYnMc9Dg 7UElcoWZsO/eX5rxaKGOvpZj2OurLqWL+aLZTRO4WA3ah/4aVhSg6w/JEs0YQMMF2cBa Ecb8CCNrzXRu3JdwWn5zQaRpu1+hjVVl3JDhwH9USvLPjkYwseVwoM2piTpnMdV+wgZW PmYBwRhx00VoibNR/4GmYBmobVTN0DWC2FGZk0+B0zagvJBVhGzFJBHK9rvKH6ocoqGN svew== X-Gm-Message-State: AElRT7EqRi5DEiMRF0TzD95Noa/gix+ELxsVQ6HquUQXekJkiXZzTym6 AQC6lEY8bpMfZaktXkpBCelfts0MZ/udijKgISLt2A== X-Received: by 10.55.137.132 with SMTP id l126mr37555775qkd.15.1520473087473; Wed, 07 Mar 2018 17:38:07 -0800 (PST) MIME-Version: 1.0 References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> In-Reply-To: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> From: Jason Gross Date: Thu, 08 Mar 2018 01:37:57 +0000 Message-ID: Subject: Re: [HoTT] Univalence from scratch To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c072d7644fec10566dcbabf" --94eb2c072d7644fec10566dcbabf Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > 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 :=3D (= 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=C3=ADn H=C3=B6tzel Escard=C3=B3 < 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 t= he > 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 Co= q > "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. > --94eb2c072d7644fec10566dcbabf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
> Perhaps somebody s= hould add a Coq "version from scratch" of this.

If y= ou just want a straightforward transcription of the Agda code, I've mad= e one here: https://gist.github.com/JasonGross/c6745e6d3ffbab3ee703498= 8c1b5b904

Feel free to adapt it as you desire, and use it = with or without crediting me.
The only "design decisions" of n= ote 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&quo= t; statements on the Id type.
3. I added a definition "isUniv= alentAt" defined so that "isUnivalent :=3D (X Y : U) -> isUniv= alentAt X Y", because I wanted to only pass universes in the definitio= n 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=C3=ADn H=C3=B6tzel Escard=C3=B3 <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 materi= al, in journals or the web.=C2=A0

For some time I was a = bit upset about this. But maybe this is our fault, by often trying to expla= in univalence only imprecisely, mixing the explanation of the models with t= he explanation of the underlying theory (MLTT, identity types, universe), w= ith none of the two explained sufficiently precisely.=C2=A0

<= /div>
There are long, precise explanations such as the HoTT book, for e= xample, or, the formalizations in Coq, Agda and Lean.

<= div>But perhaps we don't have publicly available material with a self-c= ontained, brief and complete formulation of univalence, so that interested = mathematicians and logicians can try to contemplate the axiom in a fully de= fined form.

Here is an attempt to rectify this:

This also has an ancillary Agda file with univalence defined from scratc= h (without the use of any library at all). Perhaps somebody should add a Co= q "version from scratch" of this.=C2=A0

= There is also a web version of this (http://www.cs.bha= m.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html) to try to make this a= s accessible as possible, with the text and the Agda code together.

M.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--94eb2c072d7644fec10566dcbabf--