From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.3.202 with SMTP id z10mr20863013qtg.35.1520584246667; Fri, 09 Mar 2018 00:30:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.200.44.152 with SMTP id 24ls3662599qtw.0.gmail; Fri, 09 Mar 2018 00:30:46 -0800 (PST) X-Received: by 10.200.20.154 with SMTP id l26mr20019902qtj.26.1520584246157; Fri, 09 Mar 2018 00:30:46 -0800 (PST) Received: by 10.55.44.6 with SMTP id s6msqkh; Thu, 8 Mar 2018 02:04:11 -0800 (PST) X-Received: by 10.223.132.68 with SMTP id 62mr2366528wrf.25.1520503451311; Thu, 08 Mar 2018 02:04:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520503451; cv=none; d=google.com; s=arc-20160816; b=l0FQzZs+JQ0vTzBDdh5Hue/QYFIS67rjUrbzGCfU/ceXBZ7HKac9OoF18Opb1KVMGU SWVRsiUFa2nwmKSw37a0LOR7ToKz3p0BX2ac7umw1HO3ksFX20yczTgxNx07zIyKbSTz uHfhXYwVNk1VZzlI4pBRsQQEXmYHA5O7poTaBEw3ZQxf4Us+5koVBnu3EwG4P0OUBpNt FsHbylY1qyXFr83S2zcq5ZA7dYiuR8rTnrS5yoGZBDUR9E5VO+0OcBNjEJgtkGKk1kpH hNZfTJfaJTdt3zm85+lbZepyrWLiEvGxFOGZdknQ52fg4I9ENgWDk8NWFMlMazAIQn+6 q+vg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :arc-authentication-results; bh=Kh11vcVmLQdAf5b0ZOa7wkwOuxJNUCmg+2o/vz0l83w=; b=cTdoo6XqB/6vO+olfp6hdi08hKqYnrzVAMJn9xaS222l8VtjPzs9MO4N0NiuT23oTr sQSIO3hXEBf1vsS2Q6+avh8Y154R+zF5ngjbTCtUBlr5jmADSE11+3x7+kxOQplkd9wa tCst4sRmVcvm/QOxrOT/Er+NmSIN4QY0I2JpcXQojRSpvUDhkCHn9B3j2hiExpQ0fIPs PDzQUEJHFWy8NY+Zvr9risXIpGzLZ9zdHwDDmLit+TN4DAVcsy4UGb2oy3c4tkhGOj4R zJH7DwxLhmD/nrHW3nNRHJTsfi7adrCmZW+161YPiRjfIehjBLPO1m4OBpjA278ypzc0 fteg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id g206si499612wme.2.2018.03.08.02.04.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Mar 2018 02:04:11 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun61.bham.ac.uk with esmtp (Exim 4.89) (envelope-from ) id 1etsPD-0002hW-Md; Thu, 08 Mar 2018 10:04:11 +0000 Received: from dynamic200-210.cs.bham.ac.uk ([147.188.200.210]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1etsPC-0001fG-G2 using interface auth-smtp.bham.ac.uk; Thu, 08 Mar 2018 10:04:10 +0000 Subject: Re: [HoTT] Univalence from scratch To: Jason Gross , =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> From: Martin Escardo Message-ID: <8516ef65-386c-6056-c870-0c706d832d6f@googlemail.com> Date: Thu, 8 Mar 2018 10:04:02 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) 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ó > > 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. >