From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 30608 invoked from network); 17 Aug 2020 15:59:22 -0000 Received: from mail-pl1-x63c.google.com (2607:f8b0:4864:20::63c) by inbox.vuxu.org with ESMTPUTF8; 17 Aug 2020 15:59:22 -0000 Received: by mail-pl1-x63c.google.com with SMTP id g17sf10266848plg.10 for ; Mon, 17 Aug 2020 08:59:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1597679960; cv=pass; d=google.com; s=arc-20160816; b=kOwygiAMQKxUegxx6AoFrwaoyz2AByvlFXyOxI8dQZeRbgEeFjxScF5ET6TPFOLyoC 7Z8OeyI0+hsyv9utmdWvw0SeUEQllMWbDxsa9WjaRkS6EauzBziGrnqdwrKhLk+gaiNr ucvSRaDnhsbVNwtvpAecbtHUqJbF7a0qQ7bNdsHNUI82gpfcWu1ZifHTNKEiqyoMSh3r eb3UA5AWaytTBZB+9pU+sJuRK0xmlaev2mpkII7T27rHKwHUVkmwBhooERG4nl2Z2x40 QXU+Ip+skuONMXBOUx2hGCBnL3OjZ2kZ7cbo4IU3xPVWXhElj23syNTTbqGCxZxO1FJf RTjA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=6M+i24YwBtFarxpmjaV1+nlhTinTn3dqFwe7v0+36Y0=; b=YHqtAJemzfYx81hWpj/c27H5dtUvM1ndSEPcxY8sH7wjx1yrWrvwi8oC179PV6Y9rL yraxzhvWGR1kPJbA9uH6nfP/r2YkznZeYdFTl7pIbFYZidKHKmlnL4niSPgwiP+7Vw4f yZLxL4aWLvXTJynFtsOoqTkb0b/mf017H9ALOveNwCfgoTZz74aWgcELx7Nxx3VRGVR0 EBp1cxQfPfOE2Gu6moBMN2XFGuyl0FZJ8rr+1glFlvyJ6gQDZ3eWji2kinLOgVt4+4y+ +r5pB3I3w5l5cCBaIF6PDfq8qCiiK9To5a1qRclijuVvg83XQnTRIEYDoN8QBSsldzyc qrpw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b="bFaG/B+S"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=6M+i24YwBtFarxpmjaV1+nlhTinTn3dqFwe7v0+36Y0=; b=boiiwunujO5+FIZ6MqujU/RZQDb9YjHxBZWrFXP3gc6ldn+g5tOGnyyR7J2XBti4zi QrS15LhfnNfisqQp4eRwOyjLWOMvsRNSmh82sC3VIqzsAiKS4Cu2EQ77R/yJGSjCoBXa 35M9voNa3W8zRTeaazNKFHqhnJ6kRZEm+Mwmj5AMhEXx9/fseZp9n7tI9C6hvySoK5bw TzetQnKuLEbXghHyYdZ5TP/3B6vykzAoJ81GYka7MkkJfEbGbSpwpyC+t8LutKIrGX4g Shjkly5Zin6em5YcOCldGUWyuWrvIsQXk+Z6xyKPIplCnJ4ZdV4f5+WX64nETf2JZOxT 6/1Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=6M+i24YwBtFarxpmjaV1+nlhTinTn3dqFwe7v0+36Y0=; b=BO98+KmYPE5GO+xQYTPDFpteFYRyGYq4Smu+jt64UMjs2bboX4QmijchnwSWXgih3n J4ZcpNGjHFoXMNjHfsDJaiaYrrLtTntxi3VsugLO3dauc9LA07Is0RqKfTackEXTP/dQ rgd9W+DabwaNsVZx12u7DfOrFpdaLg9qiFcNOT7AEYvpuPP53/ITHtb9GdqkpNjMXujb fIp2KkK/wY0T2+3yCbllpQE3d+JrG2MXADnTcFR1Ufy68fyG1peh7OIhuPEQ1E/gVIP9 gOD/CnnzMOFRpCa7vEsKg0PSlBR1xvYr2huH1QV9voLlrz9BeTD+IQKtJfLcWEIcyHIq HJ3w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM53067ckdr3o1F7196qvERSv2lYrRdxymVEHZK2yNBr75TQMzTXM1 RAXcZL7vg7lKejr5jzpaik0= X-Google-Smtp-Source: ABdhPJz5jt16/oqbi4wSnIcSyviOoU2tmLF5Gljggc2aqvfDl/XPrdMQIgaM1TpmDkGgRJxinwqpxQ== X-Received: by 2002:a63:1748:: with SMTP id 8mr10691587pgx.207.1597679960226; Mon, 17 Aug 2020 08:59:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:5c82:: with SMTP id a2ls4682163pgt.3.gmail; Mon, 17 Aug 2020 08:59:19 -0700 (PDT) X-Received: by 2002:a63:315:: with SMTP id 21mr9695081pgd.103.1597679959695; Mon, 17 Aug 2020 08:59:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1597679959; cv=none; d=google.com; s=arc-20160816; b=N+Qy2uzZjeKBVkpvVphngSrWO68qoQX7j4434c9jwRx8VVjh9M30hyso9YCYafCCYJ UOMGm88R/ydFUbHyZwAkxG2ntDdJCj7OVNbq2fsw5vEa/GkOHdtIjg8g83iPWV8eeJ6B clS1WY/hnqd811bCiL3fQj9etl1TitcWkb4j/wqgPqmLQ4C38g5LmhE1WVuqdZGy7MVm wjKOy7fnkvtcnD9hQIJq2OWZH7J6zF3XawMhYqH3awfCtyaMhTS2lzc8zEmEBJfbcoEr GCh5ZcUur2wCbCL1tJ6q1lyZLFxnrEuEnqBu8rdyS+kr7+SaEBYwD92lfCCOY8rU5t8v cWPg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=uMmAAj4k4uY7rgsru22lnHZXJGNrfnrPgjq5ApB4d6c=; b=U9jxadzxYyHMmMsqCvd0Mdal3hS/ohCtEbAo38cPbeuaDLRxWaz5O+h+WvlQuLGh7h rf7GkeKIJ2D41mPvnC2kyddisYODF9b+vbqU3QKAsod/frS5FfvAhbubHuihCy/cEJf5 HBPg64zBMCJvf8trd2VGnS58PmDt1KxW3cRXuTm5nU205leDoB+J6LnbSHYq9r9auyT9 XjwkbdLfu+PwTv/am10Wuk41pRHOCnEdc3E8rawrFBcvLQI3XNb3qX2CbUOLku/de8vY zGIHuOaoA5K0JrPUSM3NOd1uwUfKAvzRhu2QgHut2kvwUl/IBY5Z4ocNXdCIQdburIMp ONhg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b="bFaG/B+S"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.edu Received: from mail-ot1-x331.google.com (mail-ot1-x331.google.com. [2607:f8b0:4864:20::331]) by gmr-mx.google.com with ESMTPS id t75si958499pfc.3.2020.08.17.08.59.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 17 Aug 2020 08:59:19 -0700 (PDT) Received-SPF: pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::331 as permitted sender) client-ip=2607:f8b0:4864:20::331; Received: by mail-ot1-x331.google.com with SMTP id x24so13822576otp.3 for ; Mon, 17 Aug 2020 08:59:19 -0700 (PDT) X-Received: by 2002:a05:6830:13:: with SMTP id c19mr11920490otp.65.1597679958613; Mon, 17 Aug 2020 08:59:18 -0700 (PDT) MIME-Version: 1.0 References: <02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn@googlegroups.com> In-Reply-To: <02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn@googlegroups.com> From: Jasper Hugunin Date: Mon, 17 Aug 2020 08:59:07 -0700 Message-ID: Subject: Re: [HoTT] Re: A definition of equivalence where the identity is a unit on both sides for composition To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000065f52a05ad14dac7" X-Original-Sender: jasperh@cs.washington.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b="bFaG/B+S"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::331 as permitted sender) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --00000000000065f52a05ad14dac7 Content-Type: text/plain; charset="UTF-8" Hi Alex, Thanks, that is all really cool stuff! It's neat that you can do a similar thing for equality, I hadn't thought that was possible, though it seems obvious to me when spelled out. I actually started off learning Coq trying to formalize an undergraduate group theory class, and got sidetracked by various ways of making associativity less annoying. I was exploring reflexive decision procedures, but it's wonderful to see other approaches to this problem. With regards to your proposed definition of A involutiveBiEquiv B, I don't believe that it is a true definition of equivalence, since biEquiv is not a mere proposition. The definitions with strictly involutive inversion I have seen generally introduce a type in the middle, so A involutiveEquiv B = (C : Type) x (C equiv A) x (C equiv B), which under univalence is equivalent to equiv but can only strictly satisfy one of the two unit equations for composition. Sincerely, - Jasper Hugunin On Mon, Aug 17, 2020 at 6:48 AM alexr...@gmail.com wrote: > Hi Jasper, > > I have also thought about these sort of structures a bit, and in fact this > sort of "trick" of decomposing something of passing in an equality also > works in a variety of situations where composition involves transitivity of > equality. For example, you might be interested in Martin Escardo's > version of this for equality > which contains a fair > bit of discussion on the topic. I have also done some work on this sort of > idea related to groups which can be found here > and > submitted a pull request to agda standard library with a similar idea to > this for quasi-inverses . > > With respect to the questions at the end, I'm afraid I am not aware of any > definition for which inverses are strict and I expect that (2) (at least in > it's full generality) is not possible as this would imply that > \infty-groupoids are equivalent to strict \infty-groupoids. For involution > you could perhaps do a similar trick that is done in category theory > libraries like agda-categories where you store the data for both > directions. More precisely, if we let your definition be called biEquiv > then you could let > > A involutiveBiEquiv B = A biEquiv B x B biEquiv A > > and then let inverting be given by swapping the order of the product. I > believe this should maintain the nice compositional properties of biEquiv > and adds involutive inverses for "free". > > Hope some of this was useful/interesting. > Alex > > On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu > wrote: > >> I was thinking about various definitions of equivalence, and the various >> equations we could ask them to satisfy up to definitional equality. (They >> are of course all the same when looking at propositional equality.) >> >> Looking at composition, all the definitions of equivalence I have seen >> before satisfy at most one of the two equations id o p = p or p o id = p >> (for p : A equiv B and _o_ composition). >> >> By adapting the definition by bi-invertible maps, we can get a definition >> of equivalence where both the above equations hold, and additionally we get >> definitional associativity (p o q) o r = p o (q o r). >> >> ----- >> >> Recall the bi-invertible map definition of equivalence is >> A equiv B = >> (f : A -> B) x >> (gl : B -> A) x >> (gr : B -> A) x >> (linv : forall a, gl(f(a)) = a) x >> (rinv : forall b, f(gr(b)) = b) >> Then the identity is (id, id, id, refl, refl). >> >> When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, >> rinv2), >> we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and >> rinv require path induction (essentially to compose instantiations of linv1 >> and linv2). Since path composition in an arbitrary type only satisfies one >> of the two unit equations definitionally, I don't believe it is possible to >> satisfy both id o p and p o id for this definition. >> >> However, we can modify the definitions of linv and rinv inspired by the >> symmetric coinductive definition of equivalence (that A equiv B = (f : A -> >> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). >> >> So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, >> a = gr b -> f a = b. >> >> (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are >> contractible, so this definition is equivalent to the bi-invertible map >> definition, and thus a real definition of equivalence.) >> >> Then for the identity, we take linv = rinv = id. >> Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o >> rinv2, and exploit the fact that the identity function is definitionally a >> two-sided unit for function composition. >> >> Q.E.D. >> >> ----- >> >> Has anyone seen this definition or other definitions with this property >> used before? >> >> This definition does not behave particularly nicely with respect to >> inversion. I know a few definitions with definitional involutive inversion, >> and most definitions seem to satisfy id^-1 = id, but I don't think I know >> any definitions where p^-1 o p = id or p o p^-1 = id. >> >> There is such a wide variety of possible choices with respect to the >> definition of equivalence, I am interested in what additional properties we >> can ask of it to narrow down the scope of a "good" definition, and what >> unavoidable trade offs exist. >> Some good properties I am thinking about are: >> 1) Decomposition into (f : A -> B) x isEquiv f >> 2) Definitional groupoid equations. >> Currently (1) seems to be incompatible with involutive inversion, but as >> shown here we can have both (1) and definitional equations for everything >> except inversion. Can we be more greedy? >> >> Sincerely, >> - Jasper Hugunin >> > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com > > . > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8Ev95e9eop-DSPgDD6e_tCbQJyxfG-qUt15HYgpZ-hgA%40mail.gmail.com. --00000000000065f52a05ad14dac7 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Alex,

Thanks, that is all really coo= l stuff! It's neat that you can do a similar thing for equality, I hadn= 't thought that was possible, though it=C2=A0seems obvious to me when s= pelled out.
I actually started off learning Coq trying to formali= ze an undergraduate group theory class, and got sidetracked by various ways= of making associativity less annoying. I was exploring reflexive decision = procedures, but it's wonderful to see other approaches to this problem.=

With regards to your proposed definition of A inv= olutiveBiEquiv B, I don't believe that it is a true definition of equiv= alence, since biEquiv is not a mere proposition. The definitions=C2=A0with = strictly involutive inversion I have seen generally introduce a type in the= middle, so A involutiveEquiv B =3D (C : Type) x (C equiv A) x (C equiv B),= which under univalence is equivalent to equiv but can only strictly satisf= y one of the two unit equations for composition.

S= incerely,
- Jasper Hugunin

On Mon, Aug 17, 2020 at 6:48 AM <= a href=3D"mailto:alexr...@gmail.com">alexr...@gmail.com <alexrice73@gmail.com> wrote:
<= blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l= eft:1px solid rgb(204,204,204);padding-left:1ex">
Hi Jasper,
=
I have also thought about these sort of structures a bit, an= d in fact this sort of "trick" of decomposing something of passin= g in an equality also works in a variety of situations where composition in= volves transitivity of equality. For example, you might be interested in Martin Escardo's version of this for equality which contains a f= air bit of discussion on the topic. I have also done some work on this sort= of idea related to groups which can be found here and submitted a pull request to agda standard library with a similar id= ea to this for quasi-inverses.

With respe= ct to the questions at the end, I'm afraid I am not aware of any defini= tion for which inverses are strict and I expect that (2) (at least in it= 9;s full generality) is not possible as this would imply that \infty-groupo= ids are equivalent to strict \infty-groupoids. For involution you could per= haps do a similar trick that is done in category theory libraries like agda= -categories where you store the data for both directions. More precisely, i= f we let your definition be called biEquiv then you could let
A involutiveBiEquiv B =3D A biEquiv B x B biEquiv A
<= br>
and then let inverting be given by swapping the order of the = product. I believe this should maintain the nice compositional properties o= f biEquiv and adds involutive inverses for "free".

=
Hope some of this was useful/interesting.
Alex

On = Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu wrote:
I was thin= king about various definitions of equivalence, and the various equations we= =C2=A0could ask them to satisfy up to definitional equality. (They are of c= ourse all the same when looking at propositional equality.)

<= div>Looking at composition, all the definitions of equivalence I have seen = before satisfy at most one of the two equations id o p =3D p or p o id =3D = p (for p : A equiv B and _o_ composition).

By = adapting the definition by bi-invertible maps, we can get a definition of e= quivalence where both the above equations hold, and additionally we get def= initional associativity (p o q) o r =3D p o (q o r).

-----

Recall the bi-invertible map definition o= f equivalence is
A equiv B =3D
=C2=A0 (f : A -> B) x=
=C2=A0 (gl : B -> A) x
=C2=A0 (gr : B -> A) x
=C2=A0 (linv : forall a, gl(f(a)) =3D a) x
=C2=A0 (rinv := forall b, f(gr(b)) =3D b)
Then the identity is (id, id, id, refl= , refl).

When composing (f1, gl1, gr1, linv1, rinv= 1) with (f2, gl2, gr2, linv2, rinv2),
we can take f =3D f1 o f2, = gl =3D gl2 o gl1, gr =3D gr2 o gr1, but linv and rinv=C2=A0require path ind= uction (essentially to compose instantiations of linv1 and linv2). Since pa= th composition in an arbitrary type only satisfies one of the two unit equa= tions definitionally, I don't believe it is possible to satisfy both id= o p and p o id for this definition.

However, we c= an modify the definitions of linv and rinv=C2=A0inspired by the symmetric c= oinductive definition of equivalence (that A equiv B =3D (f : A -> B) x = (g : B -> A) x forall a b, (f a =3D b) equiv (a =3D g b)).
So we take linv : forall a b, f a =3D b -> a =3D gl b, and r= inv=C2=A0: forall a b, a =3D gr b -> f a =3D b.

(Notice that (b : B) x (f a =3D b) and (a : A) x (a =3D gr b) are contract= ible, so this definition is equivalent to the bi-invertible map definition,= and thus a real definition of equivalence.)

Then = for the identity, we take linv =3D rinv=C2=A0=3D id.
Thus for com= position, we can take linv =3D linv2=C2=A0o linv1=C2=A0and rinv=C2=A0=3D ri= nv1=C2=A0o rinv2, and exploit the fact that the identity function is defini= tionally a two-sided unit for function composition.

Q.E.D.

-----

Has anyone= seen this definition or other definitions with this property used before?<= /div>

This definition does not behave particularly nicel= y with respect to inversion. I know a few definitions with definitional inv= olutive inversion, and most definitions seem to satisfy id^-1 =3D id, but I= don't think I know any definitions=C2=A0where p^-1 o p =3D id or p o p= ^-1 =3D id.

There is such a wide variety of possib= le choices with respect to the definition of equivalence, I am interested i= n what additional properties we can ask of it to narrow down the scope of a= "good" definition, and what unavoidable trade offs exist.
<= div>Some good properties I am thinking about are:
1) Decompositio= n into (f : A -> B) x isEquiv f
2) Definitional groupoid equat= ions.
Currently (1) seems to be incompatible with involutive inve= rsion, but as shown here we can have both (1) and definitional equations fo= r everything except inversion. Can we be more greedy?

<= div>Sincerely,
- Jasper Hugunin

--
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit h= ttps://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4= -cb29ca02abecn%40googlegroups.com.

--
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8Ev95e9eop-DSPgDD6e_tCbQJy= xfG-qUt15HYgpZ-hgA%40mail.gmail.com.
--00000000000065f52a05ad14dac7--