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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yw1-xc3a.google.com (mail-yw1-xc3a.google.com [IPv6:2607:f8b0:4864:20::c3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cb3838ff for ; Mon, 11 Feb 2019 18:45:25 +0000 (UTC) Received: by mail-yw1-xc3a.google.com with SMTP id j64sf8311820ywg.22 for ; Mon, 11 Feb 2019 10:45:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549910724; cv=pass; d=google.com; s=arc-20160816; b=t10vK2CfM1PH1mql2QJFGShd1bHhSjKVd0FHxFi8od7u3oLU551qrcZw3DQfBJJZ8p MPOfEPwj4W84GEt7faXcHebRZvqFJYAVYYpIsoERMMlg60adLusCYY9+4QLITzdzyt8a vjmUpLWbKxW5Z8pSxeWpL6f6hZgCehlNBPvVyCrIhS+pWeCbvNlk3kJSI0NpdqTVe5hc X9X4FcMX3/OGwNA4WQlwUkYNzxev/GBQlVgHlz6ZpN208dnw8RqYg2uZHNkSZ4e2qbCE SbYg/bDJnxqTlNSlzPyWpTYZC7+bgAqrQEZi8JM+rHWFRttJXWfo+26sL75LINz0FM4j qzCA== 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:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature:dkim-signature; bh=w2CTZDp68kVN85Rg3U+bCdrRFuUc8WkJFVoaXKOnU8Q=; b=P520q2tlxAXro7YMLalwCZz3X9NGYqRfjFiBM2d8Mwx5mBEy8wwfecOBzpmB7Ksmj+ oxGa24Rb4Ui0P0FTjCvQ0aPTdEKfsNb6ghUb0dMe9hDjBwS25UVhLsA1JcfAkW+H/lO2 0ThC+Uj7Cd4/BONGvXUZ9LSZSg5ZB7cuYc6OKFeB5k8oefZDr2SGoQITJPVQVqYjqcX+ 99UgNjN5c8pmPVCfat0qxfWZ3a3JoORGaEdSmOvS9Dqgm7nRSXId0O3crOfAnVIQi2yQ fXHgL76kxZIXsAHozoFgSw3B45W6fpiuwid2HSRZphAV9hfBSIgxxbQByiV2s8lzmBHH yxqQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=skzvEi8y; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=axhkrz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=w2CTZDp68kVN85Rg3U+bCdrRFuUc8WkJFVoaXKOnU8Q=; b=QObvlo9OM6gLPz2iguxIyboo3bglcVLnMx8SWASNWINbpQ0+qczsMGqNLb0fxeJmGS KO/S8YNZg9MxxlHeptgCVtju8CuuIq4NOchG092CXJJKcmsBzVEgs4glEnMQfs55b+zz 1AXHoRbQ5x57fStF1bWSOXwozWTuZKGE6EO5HkeK7CeVxgKchMJvhfmYxzq70MRwtiRi NHCbeD+GkpmESyn+zcVo+Yw81gExljQfiz3J6+Rfc+dJZmbrbok5YZzP2P4RRjfMkRHp 9O8g2pxkpSTdDAdMqQPBQlxgYWmbIiJA3F5lMsD7iZTtKdAnyul+VHm/I+rzJPzujIQ1 Rsuw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=w2CTZDp68kVN85Rg3U+bCdrRFuUc8WkJFVoaXKOnU8Q=; b=Yd/vkOeuqEwbgKcX5ksU43APlq6KATF/VLp8E31uHHfj4xZuSkhtbeyOKn201jHxl1 VUOfkxLMj68kXMvRkoq/5uJDydxNH1bfZ3wkdyu5q9n1ObRiQIhJQJpMhzgdJ/dpOSIv X3VN/jVVXTNHN6YLdAJZTYy06r5GitC9eCwZkZzmI2sV7PYvCVMvSVvTaRN2b4JYpz4K Y2mOOyN4+hTH9XbVuF3OwP8qH9O2f9FAkoLL2OEvlp2IJZusXLQP0bLbGUfyMIEkMiiM ZUJ0KlBAPmlrHT7eR0xXcrf1ghb10XPzbLCGS0fBLigv3sPIUHOh8hz15tnQY6ZKryaW Vl+g== 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:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references: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=w2CTZDp68kVN85Rg3U+bCdrRFuUc8WkJFVoaXKOnU8Q=; b=Gdg0wgdd/pXWqYpP2zr5UMeaEumjnTjMSAZCPm3togn2SQGqJVPFse5C4roJnT4Iv8 IUq+gKr19NlYInW86OzKzHEVR4XXZd3o5Wzuo4sqofBVUDVRUtt062M2Ie5G46kF9KYL tgz1rJYqHcNIyIgYWXJ+wj5Ura2ZNUAAyB9yMV/H/GMyUnVy27aMjyHjYZwYVqYbga97 BwSudxERHiEpTWaD9huS9YYe+QWSpBcF5UmBJTY1DfQcR5fDgV3I4ml3QuvMHNatYI/s VQBfXVKChV+XdKy9qcwK0rmzI8bHh2dPtljs/1u5d2fGqfvx9LD/BCQpWGI/n6xZhkhC xqMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZBqHaByQBWi8ns/AvtmRYCyBYnjf72aeGQAFzl6+ycAcUx8BKP JtDA6nZDwcceEPYI2GfFCLk= X-Google-Smtp-Source: AHgI3IZYQeovAHiUdTEYfdItmivoEcgTf4KiukY/1MTbXK2GE+bllVg++s/pvPuK5FhWNLUVciR+6Q== X-Received: by 2002:a25:8042:: with SMTP id a2mr338102ybn.2.1549910724128; Mon, 11 Feb 2019 10:45:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:4281:: with SMTP id p123ls1381328yba.14.gmail; Mon, 11 Feb 2019 10:45:23 -0800 (PST) X-Received: by 2002:a25:870a:: with SMTP id a10mr3472016ybl.97.1549910723755; Mon, 11 Feb 2019 10:45:23 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549910723; cv=none; d=google.com; s=arc-20160816; b=yjOQaXujbjyj/0PjmfIiV1uLD3qfg0wa8j76junsF5ssasAwG1oyHKBmIV5/z99Hbx 3cjEmnnmv0TP/F6NAbxyVbZ8PEVv7HxB4RjUgdxeLR8EW2271t6q430heDaXTXfy8wuM Q7Eo9Zh/03sVQAGuZVsqKWYE/W5HYKlrsthDz9AePb0lBSUe6mIch+IrsEbDXWqgyiBz IrfAxQeK/XqQTEFrulsip5IEZ7xgT4O2kQxBNyZpHNC0l+R43kkKObur9Ob+SN9eQGaV 8hKWKyAfKvEcZvf3AJUuRqDqNGy1rLHRuNZVE5ef8J7xsX3E+k4Gqnb4OLwlGgqAyNxJ LkKQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=sJ/tWMtUb19aB5lZDC1SZ3M42dtCOF0M0vHASlB///M=; b=IpXHjC5TP/HMi8Ie1kpy8cJ6UkkMWR07pt1ihlpb9xt1BD9DIUD/AwWtvEH+dV9JCS ZYC8Pk7RQPy393J6VVZanRind0mb3/irmJE9mZQ7LrJPPDSTggNwyHMun2AWnCJ7TrJc NU77VGSk3uJCX4YxL8+j3lSO02OGCxllij/Ncx/tJvjCwxlKTfKtmkmYLTpo4Jy5giEM gljcqiRc0AAEIYmtTvlFEQ/0rXSbOOSCz0Xv5PJFxZ0QDsFgkBMu2Ggfbf+xfaAfcr3X Z+NL0xNdqQtNs9y/SZ39tY8aZIPBvJIQwYNlljpbx3uOwx57iDQEbpacZIW34iDhak6z 3kYg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=skzvEi8y; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=axhkrz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw1-xc31.google.com (mail-yw1-xc31.google.com. [2607:f8b0:4864:20::c31]) by gmr-mx.google.com with ESMTPS id h130si551044ywa.4.2019.02.11.10.45.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 10:45:23 -0800 (PST) Received-SPF: pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::c31 as permitted sender) client-ip=2607:f8b0:4864:20::c31; Received: by mail-yw1-xc31.google.com with SMTP id f65so4586858ywc.8 for ; Mon, 11 Feb 2019 10:45:23 -0800 (PST) X-Received: by 2002:a81:b147:: with SMTP id p68mr30922793ywh.352.1549910723415; Mon, 11 Feb 2019 10:45:23 -0800 (PST) Received: from [10.212.21.180] (cusd34.chapman.edu. [206.211.155.34]) by smtp.gmail.com with ESMTPSA id 127sm4120027ywl.1.2019.02.11.10.45.21 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 10:45:22 -0800 (PST) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] Re: Why do we need judgmental equality? From: Alexander Kurz In-Reply-To: <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk> Date: Mon, 11 Feb 2019 10:45:20 -0800 Cc: Michael Shulman , Matt Oliveri , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com> References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk> To: Thorsten Altenkirch X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: axhkrz@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=skzvEi8y; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=axhkrz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , Hi Thorsten, "When we talk about mathematical objects we think about typed entities" I agree, but does it follow that types and not objects come first? For example, 0 can simultaneously be the empty set, a natural number, an in= teger, a boolean, etc etc The importance of the "etc etc" is that this list is not fixed in advance. = It can change during mathematical course. This seems to indicate to me that objects come first and types later. Another example happens when I say that the dual category has the same obje= cts and arrows with domain and codomain reversed. The same object then belo= ngs to different categories.=20 Do you think that type theory provides enough flexibility to model this asp= ect of mathematical discourse conveniently? All the best, Alexander > On 11 Feb 2019, at 10:17, Thorsten Altenkirch wrote: >=20 > I have got something else against NuPRL. It explains Type Theory via unty= ped objects which are then typed. In my view there is no reason why we nee= d to explain typed things via untyped objects. When we talk about mathemati= cal objects we think about typed entities, and the formalism of type theory= should reflect this. It is not that we find an untyped object on the stree= t and then try to find out which type it has. We are thinking of a type fir= st and then we construct an element. >=20 > Thorsten >=20 > =EF=BB=BFOn 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on be= half of Michael Shulman" wrote: >=20 > FWIW, I think the only thing I have against NuPRL "in principle" is > that it seems to be closely tied to one particular model, which is the > opposite of what I want my type theories to achieve. I say "seems" > because then someone says something like Jon's "Nuprl's underlying > objects are untyped -- but that is not an essential part of the idea", > providing an instance of the problem I have with NuPRL "in practice", > which is that every time I think I understand it someone proves me > wrong. (-:O >=20 > Can you explain the difference between "definitional" (whatever that > means) and "strict" equality in Andromeda? Of course there is the > technical difference between judgmental equality and the equality > type, but that doesn't seem to me to be a "real" difference in the > presence of equality reflection, particularly at the purely > philosophical level at which a phrase like "equality of sense" has to > be interpreted. As far as I know, even beta-reduction has no > privileged status in the Andromeda core -- although I suppose > alpha-conversion probably does. >=20 >=20 > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri wrote= : >>=20 >> It looks like Jon is with you regarding definitional/substitutive equali= ty, since he considers Nuprl's subtitutive equality to be alpha conversion.= From the old discussion about it, I had figured Nuprl's substitutive equal= ity was the equality type. I guess I'll avoid that term. >>=20 >> So I'll ask a more concrete question. You seem to be more open to Androm= eda than Nuprl. It has a difference between definitional equality (in Jon's= sense) and the (strict/exact) equality type for approximately the same rea= son as Nuprl. If the theory you're using is HTS, then there's also path typ= es. So I gather path types are what you want to take as equality of referen= ce. Which is equality of sense? >>=20 >> Regarding the paragraph I said was vague, my complaint really is that I = don't know what you're getting at. I recommended strict or exact equality a= s possible (informal) interpretations. This doesn't mean there needs to be = something called "strict equality" in the system definition, for example, i= t means you recognize a strict equality notion when you see one. I don't kn= ow how to recognize the kind of equality you were getting at in that paragr= aph. >>=20 >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: >>>=20 >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri wrote: >>>> As a form of extensional type theory without any "built-in" implementa= tion proposal, it seems like HTS has no notion of "proof object" in Jon's s= ense, which seems to be formal, checkable proofs. It's not that you couldn'= t come up with one, it just isn't specified. So I don't think HTS has any "= definitional equality", in Jon's sense. But it seems like HTS' exact equali= ty was considered substitutive nonetheless. In fact, it seems to me like wh= at Vladimir meant by "substitutional" was that it doesn't cause coercions. = Either because it's definitional, or because it's subsumptive (my term, fro= m another message in this thread). >>>>=20 >>>> So I think you're misusing those terms. >>>=20 >>> Well, after many years I still have not managed to figure out how >>> NuPRLites use words, so it's possible that I misinterpreted what Jon >>> meant by "proof object". But if you interpret what I meant in ITT, >>> where I know what I am talking about, then it makes sense. In ITT the >>> relevant sort of "witness of a proof" is just a term, so "not >>> perturbing the proof object" means the same thing as "not causing >>> coercions". >>>=20 >>>> You seem to be downplaying the differences between these notions. Why? >>>=20 >>> Maybe things are different in computer science, but in mathematics it >>> often happens that there are things called "ideas" that are, in fact, >>> vaguer than anything that can be written down precisely, and can be >>> realized precisely by a variety of different formal definitions with >>> different formal properties. The differences -- even conceptual >>> differences -- between these definitions are not unimportant or >>> ignorable, but do not detract from the importance of the idea or our >>> ability to think about it. Indeed, the presence of multiple formal >>> approaches to the idea with different connections to different >>> subjects make it *more* important and provide us *more* options to >>> work with it formally. I am thinking of for instance all the >>> different constructions of a highly structured category of spectra, or >>> all the different definitions of (oo,1)-category. >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 > --=20 > You received this message because you are subscribed to the Google Gro= ups "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.google.com/d/optout. >=20 >=20 >=20 >=20 >=20 > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment.=20 >=20 > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored=20 > where permitted by law. >=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.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. For more options, visit https://groups.google.com/d/optout.