From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:7a0a:: with SMTP id v10-v6mr958920wmc.25.1526753358903; Sat, 19 May 2018 11:09:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:ea0e:: with SMTP id i14-v6ls1016868wmh.4.gmail; Sat, 19 May 2018 11:09:17 -0700 (PDT) X-Received: by 2002:a1c:d385:: with SMTP id k127-v6mr990504wmg.31.1526753357824; Sat, 19 May 2018 11:09:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1526753357; cv=none; d=google.com; s=arc-20160816; b=awBeNVRtBlp9zY0eK83sc6pl5diasqkkYdJUq6ieh1wN2X3zcTVb1brVadJ6VeK09K a/nny86kxrsBF8HFNMrhAVKQp1n89Uap3eauKWIii4STiVrMSi6ak8pp9oF2C1g+o42O ANY+UHRf+HPlT83T6T+ZVFW+l/iSyvOX7WwJ1nUExZezEDECIErWrAUP0j3XS9epw3C2 gx3BcoC1F67pi5JxdfEzfu+NPWgHR7dkJ25rcWMcCDDigRzF/S7ZLY6N5hqflaeZ4Ofg fuTU36CtYloMomK8Jj2wrqaNuOZus++QH1MvNna2ArcgNmvw8+4MFFCvPd3ff49idEUd yRRA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature :arc-authentication-results; bh=KFKtFF+K7nctQZywBCYPONBsoZCQd5yIuRA0zoaV5zg=; b=i23NS7qISLZOxAIjwieXpSXug3REMdMG7/+TeFPpHxg4A/mRNMCIZQtfAkl0xvgzIU xesJtIz7hrA8OKXhaJcocTmL/sCAdQz2w/Ykrp4dz9ACVNBw8j0UsPSJZyb0TPW28Iix iDUAxoH/sx+aOqNQQHVxW0zS28USO98a3KXNYo8SenMRXXAKGlruFde1GG6lo1mFfQ0j x2WFTSicfh5g8ciKzmZCB9uIj8fck18OLHvdCqNZFEfYslGlq78tk7oKIgLFQ90UbZww 7DFjmF34LywhCeFm8k5z4jqLeZga0jlL4paEVBGF30aAoblHtA2BOHRkiAmeAW9YWcCZ QuVQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=qbCwUVBs; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::233 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x233.google.com (mail-wm0-x233.google.com. [2a00:1450:400c:c09::233]) by gmr-mx.google.com with ESMTPS id w14-v6si245716wmf.1.2018.05.19.11.09.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 19 May 2018 11:09:17 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::233 as permitted sender) client-ip=2a00:1450:400c:c09::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=qbCwUVBs; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::233 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm0-x233.google.com with SMTP id o78-v6so20373243wmg.0 for ; Sat, 19 May 2018 11:09:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language; bh=KFKtFF+K7nctQZywBCYPONBsoZCQd5yIuRA0zoaV5zg=; b=qbCwUVBs8YaYOQeCmpvUSLFIcq4MjoKHjhRYuwei6nWjbsFOAHNyQKOYTTb4a/etFs NAYJzoTkaMmcsig2BK0UX0KpFPbmW81RgiCQ9pLnzCz4r1/DqpF7uENxxCNdCJ+Yjs9S 7NBG7sOYalbcY/fy6FuLVUgy0atdTZvloiRwuT4AVdxuseLNJdHcBbp7xsA03I1V8vK5 hMVIMMLmlxqpIGNMyjSZlAwuLboLu+gIjY03o+yBfV53jdLfP5u+ss4nQT2X2/LN00bK FEtgzfzo8siqwzMCcgeo22mq4zksnOdG6LT/81irCGRZLmZJVZwgTRKLu+o4+SaAsgX/ 1kEA== X-Gm-Message-State: ALKqPwfXCQ2Qvm4Pfr4qE7IvhaSBU3NOJ+qmspsQ+3E4HuN4qftJ1I1S ogkNUJne3wCZrTDy/r3u2CFXiksk X-Received: by 2002:a1c:800e:: with SMTP id b14-v6mr7411714wmd.143.1526753357283; Sat, 19 May 2018 11:09:17 -0700 (PDT) Return-Path: Received: from [192.168.0.5] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id m9-v6sm15883355wrf.72.2018.05.19.11.09.15 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 19 May 2018 11:09:16 -0700 (PDT) Subject: Re: [HoTT] Univalence <-> equivalence induction To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory References: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> From: Nicolai Kraus Message-ID: <29ef9804-139a-6eb9-241c-b75c02a14094@gmail.com> Date: Sat, 19 May 2018 19:09:15 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 MIME-Version: 1.0 In-Reply-To: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> Content-Type: multipart/alternative; boundary="------------92B52A197332F5AB3DA3D420" Content-Language: en-US --------------92B52A197332F5AB3DA3D420 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Interesting! At least I had not been aware of it. I think there's another very short way to see that "equivalence induction without computation rule" implies univalence. Recall the Capriotti/Licata/Orton-Pitts observation which says that ua + ua-beta (i.e. a function A~B -> A=B which is a section of A=B -> A~B) imply full univalence; see arXiv:1712.04890, 4.6. By distributivity of Pi and Sigma, we can write the type of pairs (ua,ua-beta) as a type family P indexed over equivalences: for types A,B and an equivalence e: A~B, we define P(A,B,e) := Sigma (p:A=B). id2equiv(p)=e. To inhabit P, we apply equivalence induction. It seems there are many such "coherification"-constructions in HoTT. -- Nicolai On 18/05/18 07:36, Martín Hötzel Escardó 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 > equivalence 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. --------------92B52A197332F5AB3DA3D420 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit Interesting! At least I had not been aware of it. I think there's another very short way to see that "equivalence induction without computation rule" implies univalence. Recall the Capriotti/Licata/Orton-Pitts observation which says that ua + ua-beta (i.e. a function A~B -> A=B which is a section of A=B -> A~B) imply full univalence; see arXiv:1712.04890, 4.6.
By distributivity of Pi and Sigma, we can write the type of pairs (ua,ua-beta) as a type family P indexed over equivalences: for types A,B and an equivalence e: A~B, we define P(A,B,e) := Sigma (p:A=B). id2equiv(p)=e. To inhabit P, we apply equivalence induction.
It seems there are many such "coherification"-constructions in HoTT.
-- Nicolai


On 18/05/18 07:36, Martín Hötzel Escardó 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:


Is this known? Some years ago it was claimed in this list that equivalence 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'.


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.

--------------92B52A197332F5AB3DA3D420--