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 29485 invoked from network); 16 Aug 2020 19:08:51 -0000 Received: from mail-pl1-x640.google.com (2607:f8b0:4864:20::640) by inbox.vuxu.org with ESMTPUTF8; 16 Aug 2020 19:08:51 -0000 Received: by mail-pl1-x640.google.com with SMTP id t19sf2858067plr.19 for ; Sun, 16 Aug 2020 12:08:51 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1597604926; cv=pass; d=google.com; s=arc-20160816; b=qNrwQL5MhSLr+ik86qpumEy6xOABxKHIYZAkfcyvSlyhbNT/XUF3or0m2BMbVhFqZG iO0PhYr9TA1LspjjKZbQ8tTetzCJR+FQG2ALy/PYRDHfnXEemjgfYDfdahhyNaizOmPZ I+i+85VZXqVpSbD4d3d5fScuP/ab2gTMTqhxcNpd0NELkvrqUeO7B5aaPEcbGXhchNYk 4GlrMl84JUcu+eZSJ9agK0SmKpPwu6Wq7xbw/8dg1Ufh5FKdwgA2yCn/d+HiWPB1PZD1 gc0xTwcnYeATTjU8kki5YtMG4qizzx/7X2ATDe2lGkSClOlJePHAVs80abUs2fA0E7TP pV7Q== 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 :mime-version:sender:dkim-signature; bh=Vy7WuE+JDs6odOlaNHJY4cSejnA/10mU/ZtWfeDEXuA=; b=VasbqFNU8kyJSGKeAYxs0rdhf/s2quAol1pm6MXiFDCaLYpIeBVVoNkA+5QLpFOrHF ZX+dUEuXSU6qd7OU5oeGVlufVpH5XbAlRNG0fisFI3CxoH2EQIAXPcKJAK6+Bt3OcycT 3oJFZNxE6QH1HrARnR/XezC+FWSMVGaQIrTloSgM4IXnZmz6COVaySr8XBTovlKJxyG9 u56lFqg2G9kVTb3KBGMpSqkEbK7EqaVn0DIcORynlrWVzDDhNIy+b1W+hga2Tw7X0anT EEKNwkQLZUS/wNKcnwBz+0SGs8ulSkqXRE4A4PYjfSlhVtyJwh6Go25yGqyh3qrbUUMA XbMQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b="SyU2/dAy"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::c31 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: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=Vy7WuE+JDs6odOlaNHJY4cSejnA/10mU/ZtWfeDEXuA=; b=q/Wdfo+EheMSjehZKgUdcOhcGRKf0Yc1LeXn4SR2lk9BOnwbsUJvpRuYjGXc0kYXWT vIN8t5z0Oet+D5yAcgN7DvLREfPRV9zQcLAYCVAmU7Zkz5L5ZGMGtImdBGvbJ8GwREF4 BsUv1E5CgaYluXtZ0ygEA0J7PWSI51oQxqobeNAaAUsfFwcwy2bgp+9IWcTAMcDM/0fX 3CEoXdQUQBT+/rZwQudRui/Wc6RzqVudLOAYvEhIv3puwR+n1y46/csz4geyX7dVtB1D 1v2zViBjqdFpbpzkpL7MXBK7cAJlZMiw9X+mne5LVuxdrqSJiC9XIxN5ejVsrE0VT6Xj xLeA== 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: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=Vy7WuE+JDs6odOlaNHJY4cSejnA/10mU/ZtWfeDEXuA=; b=tL4Dx+wzXKJyVIwTSz71kXWXM/9RRTYTnQm+ZEP8ROAx6YiuZ9qjI95IZa2rYvLTUk mONcnd/gHqNYJ5B4tmBu2hBQBMSuVr3+ymliHl9ads4/IIAkuxGOVopbqiXF4wprGAI3 tIdlweCKz3byJ3Rs/vsyhPXp+6KRzEH24WMDZtq+1+ED+LWihjuxkZ2khEngL86B/3rQ JnpliGaMv9EudNr/aIVTjn77CloQsk7QdnYsmOptLraTk7rzVJpBYB7gd18l+MeoqErz 9moT6wefbf5K/keCQwkQKDt9Fqmon3FHnQ5Ldhl20VA6xf7//K3HmSLnRdIcpT7Qc8ie fSPg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5325TnTldTCDfuv5adoi1PiwvukLY3reefZwjvjxbqhBJQIlf+7x NuShz5IvxwvSzdEKH3rHqrE= X-Google-Smtp-Source: ABdhPJxLWUWVp+R1t+VDUN16hgrTSMqd72NT2W7+Piy8N7gj56SYBY3sMFu9fpi7ywcAEBHpcGO+7A== X-Received: by 2002:a62:8001:: with SMTP id j1mr9115865pfd.45.1597604925963; Sun, 16 Aug 2020 12:08:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:7593:: with SMTP id q141ls4934887pfc.0.gmail; Sun, 16 Aug 2020 12:08:45 -0700 (PDT) X-Received: by 2002:a63:af51:: with SMTP id s17mr7917329pgo.286.1597604925582; Sun, 16 Aug 2020 12:08:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1597604925; cv=none; d=google.com; s=arc-20160816; b=ILWELQImcPsMZyZGEG66dcMgKnYMK7s4F3GUG+DXlrLnXrFuQPrG5lq1PXcPQJl0y+ cUv2/IZr2AlWMrzov9ZAaujUhhpFGmyYfb8ejhDrqC8P5kWT4bVRNctFaYCFTNv+FTDm rmlRPZINm4QM0MtR5uNP4923JQAuGB8htJaF44aGBMBa38aGyzGi6o452tuzHesFJRxV 2y+IzeYnO0jfKL7Iu8nl6sarYFXvMTf7ef1K3Ingalia6noR0GhEo9mc7bAerAfsGZMY akrweWxZRO7lMkpOF20cPJv+U8kVnU+0zf2CLGD/Bb9n5oVTOC8u1ya9Wfvi/tq/dKG9 xroQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=7u/Mgw//9TbL311T9EDJjLxXhhNCEgfKBwewPNR2x5Y=; b=gMAvAr15c8/GXofnqgW8Z6REmR1IJ12RvIwSJBkVhirJ2MU4+55JTG4NuHDKyUhH/o Bc9jp2hOh8KFc/uu1jb7cdpBiMjoOBijeWFH858H5MvB42quFPj6hiTNRVi8OUBw6zXW Faffnpd2PEXjGpC0563gyCpVElqVGHAspFJ1D5uNlnwrKL2onBPKc+CwehMIPKcFesaF jbbVLfQvM9qMMjgI6jmTpo6EhXDC0jX3uM7gwkyj9DPBSt6TFbWuccCwhf6qe1f09gv4 pvJEP6WipctetoRId5j5EbSwWgiNjTbx5ToVIdf5k9fLTDKvvUjn+nhp0dpTCuaNCgMP pPnw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b="SyU2/dAy"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::c31 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-oo1-xc31.google.com (mail-oo1-xc31.google.com. [2607:f8b0:4864:20::c31]) by gmr-mx.google.com with ESMTPS id s14si845987pgj.1.2020.08.16.12.08.45 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 16 Aug 2020 12:08:45 -0700 (PDT) Received-SPF: pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::c31 as permitted sender) client-ip=2607:f8b0:4864:20::c31; Received: by mail-oo1-xc31.google.com with SMTP id x1so2981470oox.6 for ; Sun, 16 Aug 2020 12:08:45 -0700 (PDT) X-Received: by 2002:a4a:4150:: with SMTP id x77mr8563832ooa.21.1597604924562; Sun, 16 Aug 2020 12:08:44 -0700 (PDT) MIME-Version: 1.0 From: Jasper Hugunin Date: Sun, 16 Aug 2020 12:08:32 -0700 Message-ID: Subject: [HoTT] A definition of equivalence where the identity is a unit on both sides for composition To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000000536b305ad03625b" 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="SyU2/dAy"; spf=pass (google.com: domain of jasperh@cs.washington.edu designates 2607:f8b0:4864:20::c31 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: , --0000000000000536b305ad03625b Content-Type: text/plain; charset="UTF-8" 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/CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS%2BJxQGw%40mail.gmail.com. --0000000000000536b305ad03625b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9Qo5jTP7bMsHkQGgBp9y46ic= J1m1bB0qiSiHUS%2BJxQGw%40mail.gmail.com.
--0000000000000536b305ad03625b--