From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1ab5482a for ; Thu, 12 Sep 2019 01:45:39 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id l15sf9710123oic.13 for ; Wed, 11 Sep 2019 18:45:39 -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=x654tNdsn7V9HonrPfxJQIlF5wXeWwuUBPvDIbq+Zsc=; b=jCRKI26k+jOcMZN2xDVIK4iojCpeaMfAkJ0bBQ8Rh2/x+0RFYtTR9eLGo+d7ep0iTg yQzDPRSlTRqBmUq1U2mGF8YOFhOqSM2zgvlmDzFv7Paargy5JCoShXzQSIBrI++sI/NX bux5IeAYERwJ0EA+hOx+GmhaIQtFZI5e8lROiiNv1sBFhGZeJFXz3t6oN+xDdGOa0dU3 J39OnKq91CEv9E0R/eNqNkNCxrW6DiydheFin4b3oG0bA/0oVvo/7VF/bOkEGPdJp0Ug oJNwscv+r9obk7DjEts/KMD5zr3BFIpQm0fvltPKV9kkrMXIwnrhvAtaB9RjXTaVvIWB C7bQ== 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=x654tNdsn7V9HonrPfxJQIlF5wXeWwuUBPvDIbq+Zsc=; b=OLi3eKhQGKCUwBVyZUjBYjQknKXEJhIlNsJCaMcVJpzZ+H1L/KV37wMPmQWj9WnbvR W6pgKiBe+hoy51qO7fyU4WSOBvE2HaPyJIhb7AdH9hAZkhlAZFF7JVKUPNvKZ8RRAXBg wi4RF1kMDWvmxH0jkrHSSzXnVPPFBa/ewMQ3gVh2x9GI7UNiTMzmBcvzUSjdjzcZIxsE vYNikj579djBn4HTefYtWXTNn53x8D0l80N2AVmBo7khOIaeR9FRHVrzX9InZbU+H3iQ DBvTNH3KJBODiWYhIX3g//j8EakSLM7bgQZPbN2G1R1tWVyxCT5fZ4bAmhqXshApnW6W oI9Q== 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=x654tNdsn7V9HonrPfxJQIlF5wXeWwuUBPvDIbq+Zsc=; b=eWu0VX1hCWYFA/9Yp1phNdzFiwWfK0ogKYpJqzRm59c11ioiAbKTKO9QuX0vRQYnwa qtV1ij2FTpBNNUv8a4RtO0hzjLwdZ32DECEVgOxbiQeJXNVxg3h7h7Z5MBB335zKt4iD xlNB8opu7gJh0LVv3090jA7SfrRkIhhD/p8Vhjhue2KPp9sYVokQxwpyzbuUjXz36Xha bk2g1eC2FPQIa8BSfTbsgPxP/xCIYsskN+/oi+XSxef44CNpJS2wepHKiJswX0Yba7Yt 9Vi0VykA5F4oMtCi8IqGKRxdMkcpfB9krwkqEvBMMjFpIyHbB7xkb/Hqhd7oG3of6QVB 7OnA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXcpiWWnZAaR2XzQNMMfCCHexdUhIaxhBhm50h2l7/2JVm5ZQ07 cEN1wI8GQ6j7USn+zjDr2D8= X-Google-Smtp-Source: APXvYqzxJlIMYbqVFPSAUBPi8e+Y2ErX2gXyPZTsQNh6In6bDpUMPgF58Wks5RIC9UDiBO+OxvP2Gw== X-Received: by 2002:a05:6808:85:: with SMTP id s5mr6652369oic.158.1568252737011; Wed, 11 Sep 2019 18:45:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4798:: with SMTP id o24ls3502804oic.12.gmail; Wed, 11 Sep 2019 18:45:36 -0700 (PDT) X-Received: by 2002:aca:4d08:: with SMTP id a8mr6823809oib.39.1568252736346; Wed, 11 Sep 2019 18:45:36 -0700 (PDT) Date: Wed, 11 Sep 2019 18:45:34 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <142000b0-e2e8-42cb-9201-4d2dcbec3de7@googlegroups.com> In-Reply-To: References: <50f257f8-f6a0-410e-9f32-512ebcef1e05@googlegroups.com> <68F509C8-C1BC-40B9-BE23-B930C801AF1D@ias.edu> <4957EC32-97FE-4383-AA07-C1ADF4EAF243@ias.edu> <435F59BF-DD90-43E0-926A-D197D38B94B4@ias.edu> Subject: Re: [HoTT] Definitions of equivalence satisfying judgmental/strict groupoid laws? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_65_1425252939.1568252734507" X-Original-Sender: escardo.martin@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_65_1425252939.1568252734507 Content-Type: multipart/alternative; boundary="----=_Part_66_1331457600.1568252734507" ------=_Part_66_1331457600.1568252734507 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 17/08/2019 01:14, Jason Gross wrote: > Resurrecting this thread from many years ago, because I was thinking > about it again recently, it seems to me that although { f & > isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) =3D e > judgmentally, it doesn't satisfy the rule that sym id =3D id > judgmentally. (In particular, I am not sure what relational equivalence > to use for the identity equivalence which does not change judgmentally > when I flip the order of its arguments.) Is there a version of > equivalence which simultaneously satisfies that the inverse of the > identity is judgmentally the identity, and that inverting an equivalence > twice judgmentally gives you what you started with? > > -Jason I am not sure this answer will be of the kind you are expecting. First I will consider the identity type and then the equivalence type using the same idea. I will use "=3D" for definitional equality. (1) If you have some identity type (_=E2=89=A1_, refl , J) with _=E2=89=A1_ : {X : =F0=9D=93=A4} =E2=86=92 X =E2=86=92 X =E2=86=92 =F0= =9D=93=A4 refl : {X : =F0=9D=93=A4 } (x : X) =E2=86=92 x =E2=89=A3 x J : (X : =F0=9D=93=A4) (A : (x y : X) =E2=86=92 x =E2=89=A1 y =E2=86=92= =F0=9D=93=A4) =E2=86=92 ((x : X) =E2=86=92 A x x (refl x)) =E2=86=92 (x y : X) (p : x =E2=89=A1 y) =E2=86=92 A x y p then you can define another identity type (_=E2=89=A1'_ , refl' , J') by x =E2=89=A1' y =3D =CE=A3 (z : X), (z =E2=89=A1 x) =C3=97 (z =E2=89=A1 = y) (which is equivalent to the diagonal fiber of (x,y) and also to x =E2=89=A1= y (both in pure MLTT)) refl' x =3D x , refl x , refl x J' X A f x y (z , p , q) =3D =CE=B3 z x p y q where =CF=86 : (x y : X) (q : x =E2=89=A1 y) =E2=86=92 A x y (x , refl x ,= q) =CF=86 =3D J X (=CE=BB x y q =E2=86=92 A x y (x , refl x , q)) f =CE=B3 : (z x : X) (p : z =E2=89=A1 x) (y : X) (q : z =E2=89=A1 y) = =E2=86=92 A x y (z , p , q) =CE=B3 =3D J X (=CE=BB z x p =E2=86=92 (y : X) (q : z =E2=89=A1 y) = =E2=86=92 A x y (z , p , q)) =CF=86 so that J' X A f x x (refl' x) =3D f x definitionally using the original J's computation rule. For this new identity type, we can define =E2=89=A1'-sym : {X : =F0=9D=93=A4 =CC=87 } {x y : X} =E2=86=92 x =E2= =89=A1' y =E2=86=92 y =E2=89=A1' x =E2=89=A1'-sym (a , p , q) =3D (a , q , p) so that =E2=89=A1'-sym (refl' x) =3D refl' x and =E2=89=A1'-sym (=E2=89=A1'-sym p') =3D p', both definitionally. (2) Similarly we can define an equivalence type _=E2=89=83'_ from an equiva= lence=20 type _=E2=89=83_ by X =E2=89=83' Y =3D =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=89=83 X) =C3=97 (Z= =E2=89=83 X) with the analogous identity equivalence and symmetrization operation so that the definitional equalities you want hold. This is related to the relational definition of equivalence as follows. The type X =C3=97 Y =E2=86=92 =F0=9D=93=A4 of type-valued relations is in canonical bijection with the "slice type" =CE=A3 (Z : =F0=9D=93=A4), Z =E2=86=92 X =C3=97 Y by a well-known construction, and in turn to =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=86=92 X) =C3=97 (Z =E2=86=92 Y). When you restrict to relations R such that for all x:X and y:Y the types =CE=A3 (x : X), R x y and =CE=A3 (y : Y), R x y are contractible, the type =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=86=92 X) =C3= =97 (Z =E2=86=92 Y) gets restricted to =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=89=83 X) =C3=97 (Z =E2=89=83 X) by the canonical equivalence (X =C3=97 Y =E2=86=92 =F0=9D=93=A4) =E2=89=83 =CE=A3 (Z : =F0=9D=93=A4), (= Z =E2=86=92 X) =C3=97 (Z =E2=86=92 Y). (3) If you want composition of identifications to be definitionally associative with refl definitionally neutral on both sides, you can consider the alternative identity type defined by x =E2=89=A1'' y =3D (z : X) =E2=86=92 (z =E2=89=A1 x) =E2=86=92 (z =E2= =89=A1 y) which is again equivalent to the original identity type x =E2=89=A1 y (whic= h amounts to Yoneda), refl'' x =3D (z : X) =E2=86=92 =CE=BB (p : x =E2=89=A1 z) , p because composition of identifications is given by function composition, which is definitionally associative with the identity function as its definitionally neutral element (assuming the =CE=B7 rule). (Exercise: write down J''.) (4) I don't know how to get the definitional equalities of (1) and (3) together by a suitable modification of the identity type. The constructions (1) and (3) are kind of dual. Martin On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky > wrote: > >> In general no. But their model is essentially syntactic and more or less= =20 >> complete. Or, to be more precise, I would expect it to=20 >> be more or less complete.=20 >> >> V. >> >> >> On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine > > wrote: >> >> On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky > > wrote: >> >>> The question is about how you interpret this operation for the univalen= t=20 >>> universe. If there is an interpretation of such an operation then there= is=20 >>> a way to define equivalences between types in an involutionary way. >>> >> >> I don=E2=80=99t follow why this should be the case. This shows that the= re is=20 >> some notion of equivalence *in the model* (i.e. constructed in the=20 >> meta-theory) which is strictly involutive. But there is no reason that= =20 >> this notion need be definable in the syntax of the object theory, is the= re? >> >> =E2=80=93p.=20 >> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout. >> >> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout. >> > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/142000b0-e2e8-42cb-9201-4d2dcbec3de7%40googlegroups.com. ------=_Part_66_1331457600.1568252734507 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

On 17/08/2019 01:14, Jason Gross wrote:
> Resurrecting this thread from many years ago, because I was thinking<= /div>
> about it again recently, it seems to me that although { f &a= mp;
> isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = =3D e
> judgmentally, it doesn't satisfy the rule that sym= id =3D id
> judgmentally.=C2=A0 (In particular, I am not sure= what relational equivalence
> to use for the identity equival= ence which does not change judgmentally
> when I flip the orde= r of its arguments.)=C2=A0 Is there a version of
> equivalence= which simultaneously satisfies that the inverse of the
> iden= tity is judgmentally the identity, and that inverting an equivalence
<= div>> twice judgmentally gives you what you started with?
>=
> -Jason


I am not sur= e this answer will be of the kind you are expecting.

First I will consider the identity type and then the equivalence type
using the same idea.

I will use "=3D&= quot; for definitional equality.

(1) If you have s= ome identity type (_=E2=89=A1_, refl , J) with

=C2= =A0 =C2=A0 _=E2=89=A1_ : {X : =F0=9D=93=A4} =E2=86=92 X =E2=86=92 X =E2=86= =92 =F0=9D=93=A4

=C2=A0 =C2=A0 refl : {X : =F0=9D= =93=A4 } (x : X) =E2=86=92 x =E2=89=A3 x

=C2=A0 = =C2=A0 J : (X : =F0=9D=93=A4) (A : (x y : X) =E2=86=92 x =E2=89=A1 y =E2=86= =92 =F0=9D=93=A4)
=C2=A0 =C2=A0 =C2=A0=E2=86=92 ((x : X) =E2=86= =92 A x x (refl x))
=C2=A0 =C2=A0 =C2=A0=E2=86=92 (x y : X) (p : = x =E2=89=A1 y) =E2=86=92 A x y p

then you can defi= ne another identity type (_=E2=89=A1'_ , refl' , J') by


=C2=A0 =C2=A0 x =E2=89=A1' y =3D =CE= =A3 (z : X), (z =E2=89=A1 x) =C3=97 (z =E2=89=A1 y)

(which is equivalent to the diagonal fiber of (x,y) and also to x =E2=89= =A1 y
(both in pure MLTT))


=C2=A0 =C2=A0 refl' x =3D x , refl x , refl x


=C2=A0 =C2=A0 J' X A f x y (z , p , q) =3D =CE=B3 z x = p y q
=C2=A0 =C2=A0 =C2=A0where
=C2=A0 =C2=A0 =C2=A0 = =CF=86 :=C2=A0 (x y : X) (q : x =E2=89=A1 y) =E2=86=92 A x y (x , refl x , = q)
=C2=A0 =C2=A0 =C2=A0 =CF=86 =3D J X (=CE=BB x y q =E2=86=92 A = x y (x , refl x , q)) f

=C2=A0 =C2=A0 =C2=A0 =CE= =B3 : (z x : X) (p : z =E2=89=A1 x) (y : X) (q : z =E2=89=A1 y) =E2=86=92 A= x y (z , p , q)
=C2=A0 =C2=A0 =C2=A0 =CE=B3 =3D J X (=CE=BB z x = p =E2=86=92 (y : X) (q : z =E2=89=A1 y) =E2=86=92 A x y (z , p , q)) =CF=86=

so that

=C2=A0 =C2=A0 J&= #39; X A f x x (refl' x) =3D f x

definitionall= y using the original J's computation rule.

For this new identity type, we can define

<= div>=C2=A0 =C2=A0 =E2=89=A1'-sym : {X : =F0=9D=93=A4 =CC=87 } {x y : X}= =E2=86=92 x =E2=89=A1' y =E2=86=92 y =E2=89=A1' x
=C2=A0= =C2=A0 =E2=89=A1'-sym (a , p , q) =3D (a , q , p)

=
so that

=C2=A0 =C2=A0=E2=89=A1'-sym (refl= ' x) =3D refl' x

and

<= div>=C2=A0 =E2=89=A1'-sym (=E2=89=A1'-sym p') =3D p',=

both definitionally.

(2) Simil= arly we can define an equivalence type _=E2=89=83'_ from an equivalence= type _=E2=89=83_ by

=C2=A0 =C2=A0 X =E2=89=83'= ; Y =3D =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=89=83 X) =C3=97 (Z =E2=89=83 X)

with the analogous identity equivalence and symmetr= ization operation
so that the definitional equalities you want ho= ld.

This is related to the relational definition o= f equivalence as
follows. The type

=C2= =A0 =C2=A0X =C3=97 Y =E2=86=92 =F0=9D=93=A4

of typ= e-valued relations is in canonical bijection with the "slice type"= ;

=C2=A0 =CE=A3 (Z : =F0=9D=93=A4), Z =E2=86=92 X = =C3=97 Y

by a well-known construction, and in turn= to

=C2=A0 =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=86=92= X) =C3=97 (Z =E2=86=92 Y).

When you restrict to r= elations R such that for all x:X and y:Y the types

=C2=A0 =CE=A3 (x : X), R x y

and

=C2=A0 =CE=A3 (y : Y), R x y

are contract= ible, the type =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=86=92 X) =C3=97 (Z =E2=86= =92 Y) gets restricted to

=C2=A0 =CE=A3 (Z : =F0= =9D=93=A4), (Z =E2=89=83 X) =C3=97 (Z =E2=89=83 X)

by the canonical equivalence

=C2=A0(X =C3=97 Y = =E2=86=92 =F0=9D=93=A4) =E2=89=83 =CE=A3 (Z : =F0=9D=93=A4), (Z =E2=86=92 X= ) =C3=97 (Z =E2=86=92 Y).

(3) If you want composit= ion of identifications to be definitionally
associative with refl= definitionally neutral on both sides, you can
consider the alter= native identity type defined by

=C2=A0 =C2=A0x =E2= =89=A1'' y=C2=A0 =3D (z : X) =E2=86=92 (z =E2=89=A1 x) =E2=86=92 (z= =E2=89=A1 y)

which is again equivalent to the ori= ginal identity type x =E2=89=A1 y (which
amounts to Yoneda),

=C2=A0 =C2=A0refl'' x =3D (z : X) =E2=86=92 = =CE=BB (p : x =E2=89=A1 z) , p

because composition= of identifications is given by function
composition, which is de= finitionally associative with the identity
function as its defini= tionally neutral element (assuming the =CE=B7 rule).

=C2=A0 (Exercise: write down J''.)

(4) = I don't know how to get the definitional equalities of (1) and (3)
together by a suitable modification of the identity type. The
constructions (1) and (3) are kind of dual.

Mar= tin

On Thu, Nov 13, 2014 at 12:59 PM Vlad= imir Voevodsky <vlad...@ias.edu> wrote:
In general no. But their model is essenti= ally syntactic and more or less complete. Or, to be more precise, I would e= xpect it to=C2=A0
be more or less complete.=C2=A0

V.


On No= v 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <p.l.l...@gmail.com> wr= ote:

On Thu,= Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vlad...@ias.= edu> wrote:
The question is about how you interpret this operation for the univalen= t universe. If there is an interpretation=C2=A0of such an operation then th= ere is a way to define equivalences between types in an involutionary way.<= br>

I don=E2=80=99t f= ollow why this should be the case.=C2=A0 This shows that there is some noti= on of equivalence *in the model* (i.e. constructed in the meta-theory) whic= h is strictly involutive.=C2=A0 But there is no reason that this notion nee= d be definable in the syntax of the object theory, is there?

=
=E2=80=93p.=C2=A0

--
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.
For more options, visit https://groups.google.com/= d/optout.

--
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.
For more options, visit https://groups.google.com/= d/optout.

--
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.co= m/d/msgid/HomotopyTypeTheory/142000b0-e2e8-42cb-9201-4d2dcbec3de7%40googleg= roups.com.
------=_Part_66_1331457600.1568252734507-- ------=_Part_65_1425252939.1568252734507--