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-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5674b5a3 for ; Mon, 18 Feb 2019 17:37:30 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id b21sf11214475otl.7 for ; Mon, 18 Feb 2019 09:37:29 -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=DB0HC3txSjLd7FWdB5tTXSyctHyavWTUMpM6BMIRJTU=; b=KrTORAvvH3UFLZXhLzgNK/5aDkRbizpd7ObV3vfb49JU5LwNm5TZ9wKmEc4sE2jaql UW0mROKIWfHza5lvBjc+BGZzxiYw6vLaIAfNVhaHCseZGoA05XZzqEoyttFT+j3XpXLH SgE/L7KgMww+T3dFDnXO/jFK+7wXxXsGny4k/TfU1bfw2dD3ZCQ4YSX8MgrWKAGUkSdy nAErn61eJOH3vXTAgJ072UVDplEWzqkTodVAhKpODANRZ0G4sAfxsNmypNKn5FnowkgI r6MUU70XaN1CKGBrRh7yhs/X1gi7/tvG3NVuciDs5tUyUNUe6KG3vug/ByARrtif4nrm 4d5A== 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=DB0HC3txSjLd7FWdB5tTXSyctHyavWTUMpM6BMIRJTU=; b=ohFaQu4cs/zgeXW1LfN8G6soRwTrdu4WYxMnVCx0Rxcg4H/i3gbAB//5DmGuxoXLgn 8TzRMxB46MQZdnMqxQAzZqPNfilPsYkvMyt8o9KttyHC2LqhkrGCCvz0+d2EgL+BzBBf R8yWAKQHtFIB2EoAIvDlvsjGyQV0wtuHUOM4Pf57//iXY4EhuEFLz7FCo2SVm4E/0J4d Dxv4OUDlPIyfFo7EaGytIlKQnCQkYdpHnYefzJJmgTu8ODr5OGtQZZmLI/8GyRgyohwf 8vkrzuAS7l6vbV860ZcTXIRHNw4WdYciYdPtPMtRp6f86+rFg6DfBeJwTm9W12PCyO0j 1pfg== 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=DB0HC3txSjLd7FWdB5tTXSyctHyavWTUMpM6BMIRJTU=; b=ovbMB1mpiPaKtgi/Q9wZyk39IBXfEV3MHTHZqOgLKiB/ZL7pkgAT+NCYmy+Ad+fhXb f+rhKtEz9AMXNac+yoIkXhDUnVuL7h1w5x2HpSOfV3hpdc70z36vBDQa/w830rQ0/jNT QnZsh9SVBQnuYk4kUA13bldRt5+P/ysrA6PjYkGkKxVHGcOE59kRDRmc+F4IK2Pa7G7c 9Cghijzz2W1qrUYPpSdC7gKlWAPXF8L1SyjxfHYCw5YezNsld1S0tXKCHGF7fE4v+Nrf hv5li8T/0Ion8LXndI1opM2GkhhKZ49pTCi3K6oqxO3cNBwo1kv6E69O1iaDRY8KrGwa c66A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYlIMBr8EbVYbhPY510RkHPNgSyrdrDT3n6zVfpnYi8JqPNAyLL Oi/Oe/n02ikh2ZO2nmqJqUM= X-Google-Smtp-Source: AHgI3IY5oyZ+AwaHoksA7jjz78WEUAsO4Xn4hCKxsmv3pX7Rwyyx3ksGkZuQ8qoBuruJXEQAT09d0w== X-Received: by 2002:aca:5bd7:: with SMTP id p206mr275177oib.2.1550511448781; Mon, 18 Feb 2019 09:37:28 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3d54:: with SMTP id k81ls8495308oia.1.gmail; Mon, 18 Feb 2019 09:37:28 -0800 (PST) X-Received: by 2002:aca:5592:: with SMTP id j140mr263069oib.5.1550511448070; Mon, 18 Feb 2019 09:37:28 -0800 (PST) Date: Mon, 18 Feb 2019 09:37:27 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <7c3967cd-6ea6-4008-908b-e80928240d66@googlegroups.com> In-Reply-To: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_701_1068833723.1550511447401" 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_701_1068833723.1550511447401 Content-Type: multipart/alternative; boundary="----=_Part_702_817869744.1550511447402" ------=_Part_702_817869744.1550511447402 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Friday, 8 February 2019 21:19:24 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote: > > why is it claimed that definitional equalities are essential to dependen= t=20 > type theories? > I've tested what happens if we replace definitional/judgmental 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 its u= sual=20 judgemental rules, including the =CE=B7 rule (but this rule could be disabl= ed). In order to switch off definitional equalities for the identity type and =CE=A3 types, I work with them given as hypothetical arguments to a mod= ule (and no hence with no definitions): _=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. refl : {X : =F0=9D=93=A4} (x : X) =E2=86=92 x =E2=89=A1 x 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) =E2=86=92 A x (refl x) =E2=86=92 (y : X) (r : x =E2=89=A1 y) =E2=86=92 = A y r 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) =E2=86=92 (a : A x (refl x)) =E2=86=92 J x A a x (refl x) =E2= =89=A1 a =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 _,_ : {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 =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} =E2=86=92 ((x : X) (y : Y x) =E2=86=92 A (x , y)) =E2=86=92 (z : =CE=A3 Y) =E2=86=92 A z =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} =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y)) =E2=86=92 (x : X) =E2=86=92 (y : Y x) =E2=86=92 =CE=A3-elim f (x , y) =E2=89=A1 f x y Everything I try to do with the identity type just works, including the more advanced things of univalent mathematics - but obviously I haven't tried everything that can be tried. 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 p : pr=E2=82=81 (x , y) =E2=89=A1 x but only pr=E2=82=82 (x , y) =E2=89=A1 transport Y (p =E2=81=BB=C2=B9) y It doesn't seem to be possible to get pr=E2=82=82 (x , y) =E2=89=A1 y witho= ut further assumptions. But maybe I overlooked something. One idea, which I haven't tested, is to replace =CE=A3-elim and =CE=A3-comp= by the the single axiom =CE=A3-single : {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) =E2=86=92 (f : (x : X) (y : Y x) =E2=86=92 A (x , y)) =E2=86=92 is-contr (=CE=A3 =CE=BB (g : (z : =CE=A3 Y) =E2=86=92 A z) =E2=86=92 (x : X) (y : Y x) =E2=86=92 g (x , y) =E2= =89=A1 f x y) I don't know whether this works. (I suspect the fact that "induction principles =E2=89=83 contractibility of the given data with their computati= on rules" is valid only in the presence of definitional equalities for the induction principle, and that the contractibility version has a better chance to work in the absence of definitional equalities.) One can also wonder whether the presentation taking the projections with their computation rules as primitive, and the =CE=B7 rule would work. But again we can define =CE=A3-elim but not =CE=A3-comp for it. In any case, without further identities, simply replacing definitional equalities by identity types doesn't seem to work, although I may be=20 missing something. Martin --=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_702_817869744.1550511447402 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Friday, 8 February 2019 21:19:24 UTC, Mart=C3=ADn = H=C3=B6tzel Escard=C3=B3 wrote:
=C2=A0why is it claimed that definition= al equalities are essential to dependent type theories?

I've tested what happens if we replace d= efinitional/judgmental
equalities in MLTT by identity types, work= ing in the fragment of Agda=C2=A0
that only has =CE=A0 and univer= ses (built-in) and hence my =CE=A0 has its usual=C2=A0
judgementa= l rules, including the =CE=B7 rule (but this rule could be disabled).
=

In order to switch off definitional equalities for the = identity type
and =CE=A3 types, I work with them given as hypothe= tical arguments to a module
(and no hence with no definitions):

=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.

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

=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

=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 (r= efl x)) =E2=86=92 J x A a x (refl x) =E2=89=A1 a

= =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

=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

=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

=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)
<= div>=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

Everything I try to do with the ident= ity type just works, including
the more advanced things of unival= ent mathematics - but obviously I
haven't tried everything th= at can be tried.

However, although I can define bo= th 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

=C2=A0p : pr=E2=82=81 (x , y) =E2=89=A1 x

but only

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

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 overlook= ed something.

One idea, which I haven't tested= , is to replace =CE=A3-elim and =CE=A3-comp by
the the single axi= om

=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)

I don't know whether this works. (I suspect the fact that "induc= tion
principles =E2=89=83 contractibility of the given data with = their computation
rules" is valid only in the presence of de= finitional equalities for
the induction principle, and that the c= ontractibility version has a
better chance to work in the absence= of definitional equalities.)

One can also wonder = whether the presentation taking the projections
with their comput= ation rules as primitive, and the =CE=B7 rule would
work. But aga= in we can define =CE=A3-elim but not =CE=A3-comp for it.

In any case, without further identities, simply replacing definition= al
equalities by identity types doesn't seem to work, althoug= h I may be=C2=A0
missing something.

Mart= in



--
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_702_817869744.1550511447402-- ------=_Part_701_1068833723.1550511447401--