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=-1.0 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-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8fcaf6f2 for ; Mon, 18 Feb 2019 20:23:55 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id b21sf11568532otl.7 for ; Mon, 18 Feb 2019 12:23:54 -0800 (PST) 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=f7W0uQ0Y3zXAW1hLlL+rCo8O9SIFzJW4EyGE/svwoX8=; b=DM6TxFB/HB2BUAYwNkgcGyrNywmbZO45H50WhI/GUrK668LJm94tQuDT/N8nYlLwWm GJVKeqLWCildXlkg/NqK8RvVmJE5bmCZ74EOTd63GKIY9RjDh/5crbmAxSknrsn94PE0 wbqfk+hOVsck02B5M5LQTqBwXy5RQBlzfKJ1X06EIoon3ES3BaBwDuef+NatSd9FbC14 o+Ntgxrgr+oxQChhXHjGNqaoQc78apKyVhykOD4bxPStcG/1WiMQdzH0JrlLZG1K2nJZ QSo9JFoRrp+7iLZ3uERzkMyFkDiDOrssBTIKSu4L191EPFVvmg39Zi4PBlY5E1bGaHS0 RbNA== 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=f7W0uQ0Y3zXAW1hLlL+rCo8O9SIFzJW4EyGE/svwoX8=; b=oCV+Woq1vCx2Sw3j2b/lqs4ILI7uc11KQVojgOeap6rB/XnZL6XC0r2hAh7YCHCksr z7RmqeaoC+AZBQziXQHiRDOpQO3GdhuGw0pOn61knFJslPes+VGVjHApKQbdmMyvRBd0 sgttAmYVOFeTKLJkO2CntCUBlus1CgS9hlZbslUYEKWcsatJa86kYpk46UFD7p3hvuWU B1SWPkzYZcXzc7zeIW3N1LbIPQWS5X+kTI+lotJliJvxTqLMfZOuP/pS5S1ClOxVEOic fCSEtweuSpXTc2dTw5uZ35AgEfNNJf1ffanIvWOcgK698Id6ywHXixLNwFYS6n06yB2n ds4Q== 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=f7W0uQ0Y3zXAW1hLlL+rCo8O9SIFzJW4EyGE/svwoX8=; b=PO2wQciGFyFnG1l1Ap2ABHHOvo+NYHHeIwhjATgxprUtXtGThwGFZ43iX8pBK0JZqz RioPJp/RF149xsQigXxII40hVtMLqmIG6x+E//1kYrFTWMiC2JAAOXjCSmsntXZodMRT ulOl746YV6pmGLoTDg/5ZQWIZfyB44im7KtrfQuK6ytTcZHGTxJTGBbrMk7jrXty6Ydw AughrmGj9diGqiyZZsoSctjKWZpSYUU2Sfm/KkfiSExt4uNiqeolqmE97H44UGDMhMrx 5hxrefOs8G4VtDHDoYPXfCyNXtzT5RVYYd6WncPRxX4OVUCHRdaJvJB0nsElo3TeXU7C NHZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYSwDDO94758ji4a4egRBYdXlW0ILJa7lCtL8qdrkeRYa/RI2qT WsiSA4A+6NRV0udCWzvWtPg= X-Google-Smtp-Source: AHgI3Iagu2IL79LqNxdQ+r1n/zzDbYfsTFKe3xL591EOIE2ZqmB4FrIBfHbgxZLRl584VT8uyYiQdw== X-Received: by 2002:aca:4b89:: with SMTP id y131mr271043oia.3.1550521434317; Mon, 18 Feb 2019 12:23:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:f3c5:: with SMTP id r188ls8335816oih.8.gmail; Mon, 18 Feb 2019 12:23:53 -0800 (PST) X-Received: by 2002:aca:5884:: with SMTP id m126mr271233oib.4.1550521433515; Mon, 18 Feb 2019 12:23:53 -0800 (PST) Date: Mon, 18 Feb 2019 12:23:52 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> <7c3967cd-6ea6-4008-908b-e80928240d66@googlegroups.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_734_459753196.1550521432881" 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_734_459753196.1550521432881 Content-Type: multipart/alternative; boundary="----=_Part_735_879256585.1550521432882" ------=_Part_735_879256585.1550521432882 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Sorry, I was being silly. Martin On Monday, 18 February 2019 19:22:23 UTC, dlicata wrote: > > Hi,=20 > > I=E2=80=99m confused =E2=80=94 does it even type check to ask pr=E2=82= =82 (x , y) =E2=89=A1 y ?=20 > > I would expect=20 > > x : A=20 > y : B(x)=20 > (x,y) : =CE=A3 A B=20 > fst (x,y) : A=20 > snd (x,y) : B(fst (x,y))=20 > > so if beta for fst is weak, then=20 > > pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y=20 > > is the best you could hope for. I.e., you have a path for the first beta= ,=20 > and a path over it for the second. =20 > > -Dan=20 > > > On Feb 18, 2019, at 12:37 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < > escardo...@gmail.com > wrote:=20 > >=20 > > On Friday, 8 February 2019 21:19:24 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote:=20 > > why is it claimed that definitional equalities are essential to=20 > dependent type theories?=20 > >=20 > > I've tested what happens if we replace definitional/judgmental=20 > > equalities in MLTT by identity types, working in the fragment of Agda= =20 > > that only has =CE=A0 and universes (built-in) and hence my =CE=A0 has i= ts usual=20 > > judgemental rules, including the =CE=B7 rule (but this rule could be=20 > disabled).=20 > >=20 > > In order to switch off definitional equalities for the identity type=20 > > and =CE=A3 types, I work with them given as hypothetical arguments to a= =20 > module=20 > > (and no hence with no definitions):=20 > >=20 > > _=E2=89=A1_ : {X : =F0=9D=93=A4} =E2=86=92 X =E2=86=92 X =E2=86=92 = =F0=9D=93=A4 -- Identity type.=20 > >=20 > > refl : {X : =F0=9D=93=A4} (x : X) =E2=86=92 x =E2=89=A1 x=20 > >=20 > > J : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 x =E2=89=A1 y = =E2=86=92 =F0=9D=93=A4)=20 > > =E2=86=92 A x (refl x) =E2=86=92 (y : X) (r : x =E2=89=A1 y) =E2=86= =92 A y r=20 > >=20 > > J-comp : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 x =E2=89= =A1 y =E2=86=92 =F0=9D=93=A4)=20 > > =E2=86=92 (a : A x (refl x)) =E2=86=92 J x A a x (refl x) = =E2=89=A1 a=20 > >=20 > > =CE=A3 : {X : =F0=9D=93=A4} =E2=86=92 (X =E2=86=92 =F0=9D=93=A4) =E2= =86=92 =F0=9D=93=A4=20 > >=20 > > _,_ : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} (x : X) =E2= =86=92 Y x =E2=86=92 =CE=A3 Y=20 > >=20 > > =CE=A3-elim : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} {A : = =CE=A3 Y =E2=86=92 =F0=9D=93=A4}=20 > > =E2=86=92 ((x : X) (y : Y x) =E2=86=92 A (x , y))=20 > > =E2=86=92 (z : =CE=A3 Y) =E2=86=92 A z=20 > >=20 > > =CE=A3-comp : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} {A : = =CE=A3 Y =E2=86=92 =F0=9D=93=A4}=20 > > =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y))=20 > > =E2=86=92 (x : X)=20 > > =E2=86=92 (y : Y x)=20 > > =E2=86=92 =CE=A3-elim f (x , y) =E2=89=A1 f x y=20 > >=20 > > Everything I try to do with the identity type just works, including=20 > > the more advanced things of univalent mathematics - but obviously I=20 > > haven't tried everything that can be tried.=20 > >=20 > > However, although I can define both projections pr=E2=82=81 and pr=E2= =82=82 for =CE=A3, and=20 > > prove the =CE=B7-rule =CF=83 =E2=89=A1 (pr=E2=82=81 =CF=83 , pr=E2=82= =82 =CF=83), I get=20 > >=20 > > p : pr=E2=82=81 (x , y) =E2=89=A1 x=20 > >=20 > > but only=20 > >=20 > > pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y=20 > >=20 > > It doesn't seem to be possible to get pr=E2=82=82 (x , y) =E2=89=A1 y w= ithout further=20 > > assumptions. But maybe I overlooked something.=20 > >=20 > > One idea, which I haven't tested, is to replace =CE=A3-elim and =CE=A3-= comp by=20 > > the the single axiom=20 > >=20 > > =CE=A3-single :=20 > > {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} (A : =CE=A3 Y = =E2=86=92 =F0=9D=93=A4)=20 > > =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y))=20 > > =E2=86=92 is-contr (=CE=A3 =CE=BB (g : (z : =CE=A3 Y) =E2=86=92 A z= )=20 > > =E2=86=92 (x : X) (y : Y x) =E2=86=92 g (x , y) = =E2=89=A1 f x y)=20 > >=20 > > I don't know whether this works. (I suspect the fact that "induction=20 > > principles =E2=89=83 contractibility of the given data with their compu= tation=20 > > rules" is valid only in the presence of definitional equalities for=20 > > the induction principle, and that the contractibility version has a=20 > > better chance to work in the absence of definitional equalities.)=20 > >=20 > > One can also wonder whether the presentation taking the projections=20 > > with their computation rules as primitive, and the =CE=B7 rule would=20 > > work. But again we can define =CE=A3-elim but not =CE=A3-comp for it.= =20 > >=20 > > In any case, without further identities, simply replacing definitional= =20 > > equalities by identity types doesn't seem to work, although I may be=20 > > missing something.=20 > >=20 > > Martin=20 > >=20 > >=20 > >=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com = .=20 > > > For more options, visit https://groups.google.com/d/optout.=20 > > --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_735_879256585.1550521432882 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Sorry, I was being silly. Martin

On Monday, 18 Febr= uary 2019 19:22:23 UTC, dlicata wrote:
Hi,

I=E2=80=99m confused =E2=80=94 does it even type check to ask =C2=A0pr= =E2=82=82 (x , y) =E2=89=A1 y ?

I would expect=20

x : A
y : B(x)
(x,y) : =CE=A3 A B
fst (x,y) : A
snd (x,y) : B(fst (x,y))

so if beta for fst is weak, then

pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y

is the best you could hope for. =C2=A0I.e., you have a path for the fir= st beta, and a path over it for the second. =C2=A0

-Dan

> On Feb 18, 2019, at 12:37 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3= <= escardo...@gmail.com> wrote:
>=20
> On Friday, 8 February 2019 21:19:24 UTC, Mart=C3=ADn H=C3=B6tzel E= scard=C3=B3 wrote:
> =C2=A0why is it claimed that definitional equalities are essential= to dependent type theories?
>=20
> I've tested what happens if we replace definitional/judgmental
> equalities in MLTT by identity types, working in the fragment of A= gda=20
> that only has =CE=A0 and universes (built-in) and hence my =CE=A0 = has its usual=20
> judgemental rules, including the =CE=B7 rule (but this rule could = be disabled).
>=20
> In order to switch off definitional equalities for the identity ty= pe
> and =CE=A3 types, I work with them given as hypothetical arguments= to a module
> (and no hence with no definitions):
>=20
> =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 =C2=A0 =C2=A0-- Identity type.
>=20
> =C2=A0 refl : {X : =F0=9D=93=A4} (x : X) =E2=86=92 x =E2=89=A1 x
>=20
> =C2=A0 J : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 x =E2= =89=A1 y =E2=86=92 =F0=9D=93=A4)
> =C2=A0 =C2=A0 =E2=86=92 A x (refl x) =E2=86=92 (y : X) (r : x =E2= =89=A1 y) =E2=86=92 A y r
>=20
> =C2=A0 J-comp : {X : =F0=9D=93=A4} (x : X) (A : (y : X) =E2=86=92 = x =E2=89=A1 y =E2=86=92 =F0=9D=93=A4)
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =E2=86=92 (a : A x (refl= x)) =E2=86=92 J x A a x (refl x) =E2=89=A1 a
>=20
> =C2=A0 =CE=A3 : {X : =F0=9D=93=A4} =E2=86=92 (X =E2=86=92 =F0=9D= =93=A4) =E2=86=92 =F0=9D=93=A4
>=20
> =C2=A0 _,_ : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93=A4} (x = : X) =E2=86=92 Y x =E2=86=92 =CE=A3 Y
>=20
> =C2=A0 =CE=A3-elim : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93= =A4} {A : =CE=A3 Y =E2=86=92 =F0=9D=93=A4}
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 ((x : X) (y : Y x) =E2= =86=92 A (x , y))
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 (z : =CE=A3 Y) =E2=86= =92 A z
>=20
> =C2=A0 =CE=A3-comp : {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93= =A4} {A : =CE=A3 Y =E2=86=92 =F0=9D=93=A4}
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 (f : (x : X) (y : Y x)= =E2=86=92 A (x , y))
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 (x : X)
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 (y : Y x)
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=E2=86=92 =CE=A3-elim f (x , y) = =E2=89=A1 f x y
>=20
> Everything I try to do with the identity type just works, includin= g
> the more advanced things of univalent mathematics - but obviously = I
> haven't tried everything that can be tried.
>=20
> However, although I can define both projections pr=E2=82=81 and pr= =E2=82=82 for =CE=A3, and
> prove the =CE=B7-rule =CF=83 =E2=89=A1 (pr=E2=82=81 =CF=83 , pr=E2= =82=82 =CF=83), I get
>=20
> =C2=A0p : pr=E2=82=81 (x , y) =E2=89=A1 x
>=20
> but only
>=20
> =C2=A0 =C2=A0 =C2=A0pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p = =E2=81=BB=C2=B9) y
>=20
> It doesn't seem to be possible to get pr=E2=82=82 (x , y) =E2= =89=A1 y without further
> assumptions. But maybe I overlooked something.
>=20
> One idea, which I haven't tested, is to replace =CE=A3-elim an= d =CE=A3-comp by
> the the single axiom
>=20
> =C2=A0 =CE=A3-single :
> =C2=A0 =C2=A0 =C2=A0 {X : =F0=9D=93=A4} {Y : X =E2=86=92 =F0=9D=93= =A4} (A : =CE=A3 Y =E2=86=92 =F0=9D=93=A4)
> =C2=A0 =C2=A0 =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y)= )
> =C2=A0 =C2=A0 =E2=86=92 is-contr (=CE=A3 =CE=BB (g : (z : =CE=A3 Y= ) =E2=86=92 A z)
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0=E2=86=92 (x : X) (y : Y x) =E2=86=92 g (x , y) =E2=89=A1 = f x y)
>=20
> I don't know whether this works. (I suspect the fact that &quo= t;induction
> principles =E2=89=83 contractibility of the given data with their = computation
> rules" is valid only in the presence of definitional equaliti= es for
> the induction principle, and that the contractibility version has = a
> better chance to work in the absence of definitional equalities.)
>=20
> One can also wonder whether the presentation taking the projection= s
> with their computation rules as primitive, and the =CE=B7 rule wou= ld
> work. But again we can define =CE=A3-elim but not =CE=A3-comp for = it.
>=20
> In any case, without further identities, simply replacing definiti= onal
> equalities by identity types doesn't seem to work, although I = may be=20
> missing something.
>=20
> Martin
>=20
>=20
>=20
>=20
> --=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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.go= ogle.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 http= s://groups.google.com/d/optout.
------=_Part_735_879256585.1550521432882-- ------=_Part_734_459753196.1550521432881--