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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 16615 invoked from network); 17 Aug 2020 13:48:15 -0000 Received: from mail-yb1-xb39.google.com (2607:f8b0:4864:20::b39) by inbox.vuxu.org with ESMTPUTF8; 17 Aug 2020 13:48:15 -0000 Received: by mail-yb1-xb39.google.com with SMTP id a14sf18310341ybm.13 for ; Mon, 17 Aug 2020 06:48:15 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=3GYbDFNPoxO73+JIAXV15cj3Pr+e/5EX7B/Wj3hkPu0=; b=H3x9SI7jWNyk6m5Qo1FT1pFONcfREfrWAONf3s+L+2bppIIVz7r3T6uBndd8snmzGM gW6IUpDpESZuzlzHf5GRMQ/Vo8SKnAIFG4cLw6PGya8gHnrMKeL9Vl1EQX9HXIMwCD/E vukJKFdy7pKxA+Wn6Dus5Jd4f6DgC9lLuZwZm+RlfcXoAYFxSyJdMzg8xiGa90NVKRFz HlY19CIN1M8MTq6DnqLrdtSVUMh0lLWI61HId0XGTz3ot3NtxKOKajBXYLIrhxkvLUPD gjezxHX2PMgLCrNzzMG3i+Z2D7sjNepCnoh4t5UYxvdZiISf9y5J/cC5qGpxu944ck6u s+Mg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=3GYbDFNPoxO73+JIAXV15cj3Pr+e/5EX7B/Wj3hkPu0=; b=XZ9HRBP3odBp9SwifsNqAgBrlw4wlDhe0l01Cmx3v/7/j5CHaOUriZnOKUstTzqNSB 9PDdpELy19odwcPBdgksiUm7plh2GxiiFZvPBoYgI8GwDMkIco2hik9urpF2bHf5erFW nVVXEA5TIoeztJMZ9MuBEHQMvGPcAKAxGpGWNJ46OHqokhLBjjgA5at56nlnUbtGaIip OR3ZPVlrYy3kUz2vxx/msvWhXM0xqKSUhlXhi10ZJyf04edNueokmiTqFlJv6Ayejt8D IkupsSHg+h2A0DQ0TrdHHR1E7e7RI++EKZCHwN4YX5Ap6B4vz2QDe4cy6cdWqPcyOaqF w18A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=3GYbDFNPoxO73+JIAXV15cj3Pr+e/5EX7B/Wj3hkPu0=; b=LkmK1LcJKQ68Lg1jcfa90rIaLfB2cBRAyPuOsOkq777t/1BMeyRxbpOuLfi4qNNial +qPkINd1WRkAPWDJX4vB8X5OGgIgExH+0AkKcivq112ZASMPqNn5pwb5fbmYy98GTqqv wY/rlucppSVF3kg5j1yPYkYACq97CISUTAsph5E9hi18bT3sAPf0jAvqeZouQ7zEc7xk CuSqNtA8XeQcbXAa4L7fwmFfmA3WZfU/ZY1IKXi4RwNwSdPVEWUpCTeFGwXRzaSQcMq8 xREg0gdeq9H4iSCMcwx54ss9YQ+/WE8bOhLWTwh6pg/Wnzj5l/9gryUtmg69fuMlQlmK fYzQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530kDYSj5ZZZQLPJOpBRVgkA88eIn6NyRcdyHwgKkNRu52LQ/yc/ qAbqelTYaenldaE3TziI/EA= X-Google-Smtp-Source: ABdhPJyNIF6t8udCFkTepHhkpl/ZAZdXADUkrVGzfs/nnNPvPNjQODVBdgttVcd7YwZLLcNSP5AHRA== X-Received: by 2002:a25:dac2:: with SMTP id n185mr20888104ybf.396.1597672093435; Mon, 17 Aug 2020 06:48:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:5755:: with SMTP id l82ls6736292ybb.5.gmail; Mon, 17 Aug 2020 06:48:13 -0700 (PDT) X-Received: by 2002:a25:b46:: with SMTP id 67mr19396966ybl.46.1597672092893; Mon, 17 Aug 2020 06:48:12 -0700 (PDT) Date: Mon, 17 Aug 2020 06:48:12 -0700 (PDT) From: "alexr...@gmail.com" To: Homotopy Type Theory Message-Id: <02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: A definition of equivalence where the identity is a unit on both sides for composition MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_398_1504883453.1597672092010" X-Original-Sender: alexrice73@gmail.com 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: , ------=_Part_398_1504883453.1597672092010 Content-Type: multipart/alternative; boundary="----=_Part_399_871536398.1597672092010" ------=_Part_399_871536398.1597672092010 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_399_871536398.1597672092010 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Jasper,

I have also thought about these so= rt of structures a bit, and in fact this sort of "trick" of decomposing som= ething of passing in an equality also works in a variety of situations wher= e composition involves transitivity of equality. For example, you might be = interested in Martin Escardo's version of this for equality which contains a fair bi= t of discussion on the topic. I have also done some work on this sort of id= ea 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 expec= t 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 t= heory libraries like agda-categories where you store the data for both dire= ctions. More precisely, if we let your definition be called biEquiv then yo= u could let

A involutiveBiEquiv B =3D A biEquiv B = x B biEquiv A

and then let inverting be given by s= wapping the order of the product. I believe this should maintain the nice c= ompositional 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.washingto= n.edu wrote:
=
I was thinking about various definitions of equivalence, a= nd the various equations we=C2=A0could ask them to satisfy up to definition= al 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 =3D p or p o id =3D p (for p : A equiv B and _o_ composition).

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

-----

Recall the bi-= invertible map definition of 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 i= dentity is (id, id, id, refl, refl).

When composin= g (f1, gl1, gr1, linv1, rinv1) 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 an= d rinv=C2=A0require path induction (essentially to compose instantiations o= f linv1 and linv2). Since path composition in an arbitrary type only satisf= ies 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=C2= =A0inspired by the symmetric coinductive definition of equivalence (that A = equiv B =3D (f : A -> B) x (g : B -> A) x forall a b, (f a =3D b) equ= iv (a =3D g b)).

So we take linv : forall a b, f a= =3D b -> a =3D gl b, and rinv=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 contractible, so this definition is equivalent to th= e 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 composition, we can take linv =3D linv2=C2=A0= o linv1=C2=A0and rinv=C2=A0=3D rinv1=C2=A0o rinv2, and exploit the fact tha= t the identity function is definitionally a two-sided unit for function com= position.

Q.E.D.

-----

Has anyone seen this definition or other definitions= with this property used before?

This definition d= oes not behave particularly nicely with respect to inversion. I know a few = definitions with definitional involutive inversion, and most definitions se= em 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 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 una= voidable trade offs exist.
Some good properties I am thinking abo= ut 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 m= ore greedy?

Sincerely,
- Jasper Hugunin<= br>

--
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://groups.google.c= om/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googl= egroups.com.
------=_Part_399_871536398.1597672092010-- ------=_Part_398_1504883453.1597672092010--