From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:f50e:: with SMTP id t14-v6mr523535wmh.27.1526648699698; Fri, 18 May 2018 06:04:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:99c8:: with SMTP id y66-v6ls2640732wrb.0.gmail; Fri, 18 May 2018 06:04:58 -0700 (PDT) X-Received: by 2002:adf:e3ce:: with SMTP id k14-v6mr894253wrm.7.1526648698544; Fri, 18 May 2018 06:04:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1526648698; cv=none; d=google.com; s=arc-20160816; b=gSCVQRZFKJtAn6T4zVe6uOB8ktsjKvrCNXzObKWcn/kL8UI5fBS4c4wEPkp+YRza6q k8QoNrVf3dR30rGjXJBG+dIk+N53F5JY4mMjTkNU44wv8pYBVjiqxLld4SbAXYfqDnxE BWJFJUakuIZKhJvM7vKCpLsDVLqfjQKRcPCeU13qEDPckehGEyCQESWLnlIC/FtyLkTg 9j4zejqpLelNGKG77RoTgpMiA3r8prw3OZYeVnClQqlGEFfQrPDjyrAYAHpINGCFvouf 0B/jSFNbv7SC3UWX6BAn4W/xfcy+I6piYLPi9UWSKJEa6HzxoeKsv0e5eyxMGGhPGW89 GZpw== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=p38uQmwr49os8YmLG9tOqTzSmyLVzm6w6SgQda9KlLg=; b=uKL7kqRShe98NHwknjsYzq8fX/LA2H4e431S7zOqv9e1VfkTg7oGxf6vWpEu8f3rBF Z29/2X8dn5BCmceuNTgC3rkhXmDTbYFb9sP0rv9JgiVd+LSypyAg6F+/9lpZQcPDOXvI o21YrebqTJAdlgPk+7/RIlVY4jWBW7cG4aNCGKaRzY2pVLgXG7/vJn6sYOsG1gJ0zWqj T5fOWTS+sdWW6NRJIJCycXc6UnqtzVlet6Iwu0W6XqPiEJu6nNWFZcHte1XBCPW9NOcP WugIkvDhI+lkjrSucQXlPKhTsGx3ximhZkfpW+7YSBZgaysOix3BQBud3d3RFuFHjp7S Sdug== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=SvUIx4s/; spf=pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c09::235 as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x235.google.com (mail-wm0-x235.google.com. [2a00:1450:400c:c09::235]) by gmr-mx.google.com with ESMTPS id m18-v6si488448wrh.0.2018.05.18.06.04.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 18 May 2018 06:04:58 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c09::235 as permitted sender) client-ip=2a00:1450:400c:c09::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=SvUIx4s/; spf=pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c09::235 as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm0-x235.google.com with SMTP id m129-v6so15002743wmb.3 for ; Fri, 18 May 2018 06:04:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=p38uQmwr49os8YmLG9tOqTzSmyLVzm6w6SgQda9KlLg=; b=SvUIx4s/DmpQZTBDwFIso4yRYv2xT7m4jgowAIrUenNAVs1XpPO9+Qg8yVnDuDxK+Q vlNFV/j7sTdnmoAtwZ3Yz59Bx9KgakNSQn4lHKcE/f+XERJHzlBQXP9oD9h/Z/O6vD1z 7sdOGvW0LxEJIw49iB02u9NQleIdxI3EaLhjye6dDx7pWZjtVuXKXPVfym6FhOWY4Yxs nOZURXCSXc8NtRB5WOGhCRzWtPUov0PaK8qHhxwf/mLFIYF4ZWI21KdfKCbkccc8WFLz ebf95fCB+tY2n2I+0AjNrTnV7Mz50YOFAtFQ88mIk2MP5722CgCtKiwV49vU8I2/EX7w JMEg== X-Gm-Message-State: ALKqPwcW5QjNpBJ5e9cqSJzHvQ9FIRbh3PxpMNWaCOF+11hblIrF6fzJ 1C/FhwgD1W9JM4I9HYCj7xHDjV9nKaCxgIZdW9NxdA== X-Received: by 2002:a1c:ee95:: with SMTP id j21-v6mr4564559wmi.16.1526648698012; Fri, 18 May 2018 06:04:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.223.178.174 with HTTP; Fri, 18 May 2018 06:04:57 -0700 (PDT) In-Reply-To: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> References: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> From: Egbert Rijke Date: Fri, 18 May 2018 09:04:57 -0400 Message-ID: Subject: Re: [HoTT] Univalence <-> equivalence induction To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000057a203056c7a997f" --00000000000057a203056c7a997f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Martin, I think it was known. I taught this in my intro to HoTT class this semester= : http://www.andrew.cmu.edu/user/erijke/hott/univalence.pdf Best wishes, Egbert On Fri, May 18, 2018 at 2:36 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < escardo...@gmail.com> wrote: > Equivalence induction says that in order to prove something for all > equivalences, it is enough to prove it for all identity equivalences for > all types. > > This follows from univalence. But also, conversely, univalence follows > from it: > > http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq > > Is this known? Some years ago it was claimed in this list that equivalenc= e > induction would be strictly weaker than univalence. > > To prove the above, I apply a technique I learned from Peter Lumsdaine, > that given an abstract identity system (Id, refl , J) with no given > "computation rule" for J, produces another identity system (Id, refl , J'= , > J'-comp) with > a "propositional computation rule" J'-comp for J'. > > http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html > > Martin > > -- > 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. > --=20 egbertrijke.com --00000000000057a203056c7a997f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Martin,

I think it wa= s known. I taught this in my intro to HoTT class this semester:
<= br>

On Fri, May 18, 2018 at 2:= 36 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo...@gmail.com= > wrote:
Equiv= alence induction says that in order to prove something for all equivalences= , it is enough to prove it for all identity equivalences for all types.
This follows from univalence. But also, conversely, univale= nce follows from it:





Martin

<= span class=3D"HOEnZb">

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



--
<= a href=3D"https://egbertrijke.com/" target=3D"_blank">egbertrijke.com
--00000000000057a203056c7a997f--