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-yb1-xb3e.google.com (mail-yb1-xb3e.google.com [IPv6:2607:f8b0:4864:20::b3e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ad9272b4 for ; Tue, 12 Feb 2019 02:09:08 +0000 (UTC) Received: by mail-yb1-xb3e.google.com with SMTP id o8sf751974ybp.1 for ; Mon, 11 Feb 2019 18:09:08 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549937347; cv=pass; d=google.com; s=arc-20160816; b=qc39h8kS/egU2fCfjWmBkxYLobduoLZ78VzVPgLePo/pRBIlpotJ7gtVf1K/GQIuEU gAZRwRH9E6yg5VISvoUDDhHGs7tvTRKZT9hv0PHPMJSvDDLyVojyM3LOBW52UZHZG0pk oXhyPUQ9jtT4Irc9c9IUloFe2MotX7nj8hYJFIIRYNmwAUuqKuPDJ9Q7CgN6IAKp7K61 g6XwwRavu0P+kdD53zzDpzTXv2q7Oa7M9MYo1iShLHmgQ0sQCSQafMstxEn1G6tzMSuA reLm779tf8p0rOSr+NQQGPZeX9sFrTNix4u7jTBuuUmtmXOaAIvGtro6jOyct3TjDLbY V1OA== 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:content-language:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:sender:dkim-signature:dkim-signature; bh=qiWRGjK0g5xPxkHw8mOH4aHXGQe7aj0vwygrk0QswSk=; b=u2b84xVM5xLJZ9zC3kbznDonJjZ8gCxJsXON7dXwKi4l4aFbYQ241A+aku1JthxFfZ V6sTp9jCrtK5n1f2SvIrN8Zwd581zq2zxePK32SmTWgx+A/PfoKSLYtyEz6PU87+h60N EofKUuexzoaODO+WL51IzIMlqdwshHrNYPBvudA4iL/L6yCV95YTbGa7WyrrBx/wOPsk HGEB3WI3/yVyqIS2FFm1enMtquBFGdx770R+FPOOBA9TXeGUko9JF31kMzqRkKljDjQU IOgnMbvg0Scj+ucLGu/27oTuERKrGgZpwcGHnt23jOBo08UNSxEtKP92BLweBMySBUHO NNoQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WN4w0FVJ; spf=pass (google.com: domain of jacques.carette@gmail.com designates 2607:f8b0:4864:20::136 as permitted sender) smtp.mailfrom=jacques.carette@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:subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=qiWRGjK0g5xPxkHw8mOH4aHXGQe7aj0vwygrk0QswSk=; b=hXnA/ba+WtklxmXJOrOrK9pTxznSpZrDgKR99AX+vWRwudfpaAir9EkgrfpBsjF5M4 Lv8OPBcW71F1TV78sNm1xxZwdL6Y+lZb6LU34ecoA/FIIZA+IxU6YkxQWfJ95d+61mnr ZP4Bit0+PFFA8Rl/8AMRoX5Ab9M6melQX+tz8k/5VuD+NoFtJYdtFsnWavxsGc2v9GeI 6vrHPC/P6qQVMMsmY33YLXb7orT/OdhVD/EzcmMx7Uuw6A60b88SAWqyl0hhPOpfekR3 UpcyPJ/33bQ9z7TKzi9GAHWj1GSs1ADchqKxcyJB2znGNsZTpJQAYjbvEEa5XR40bCyX n4Dg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=qiWRGjK0g5xPxkHw8mOH4aHXGQe7aj0vwygrk0QswSk=; b=dyb2dlkm3kctdmaqHbZf/3J9dcFxGpPmVId+iFdhCZhrHVHnAgAYna4iT0Bd+azCGm A50nj7ult6+ipkfQwDoMv49vtHznbOCSuOXjskzX6oGn0jO09QuXg7lxKqHBkBIt3KfB mxbbCKBZnnw/CJMUWSo+fVUqG3MYL+Uczb+KkBmEZSP3NBFuYnnIBMG3hlaVLWQmPCbL QdoN84gFECHnCo89jcN3aodcWZOn41Zpnq8ypyFLp8DZ9tsArD+PMypF58CbymxrudFc 7BpY4jkfkVM1OHTrp/HDETej8o/BWan1rdSHPCBzy0Zc4uRKiMBl5v6B0SXqE/8ceODj CZBg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:cc:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language: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=qiWRGjK0g5xPxkHw8mOH4aHXGQe7aj0vwygrk0QswSk=; b=MABkNDg6RnM1joJvdzEuLXq3FyZOdBUHuB0PUn4E59Szelt0Y5Bvj91fLx/rTu/MKj /TViNCiiTYmg+6Vtqlj4s9/TAYJFo60WKoymUOaBvRlEOuzyYdWPhhliWrEaLW8DEm+6 1CXvMNyD5Ss7N7Jb3miBXiyXavBldHwhQdyCt+5YSPLh+Y40x+2xb2i7WX3KVYAaqw9i G2uBAId7grd8Wf6DsCJYu+fSkLecai3sZ8WViRbJzHZc23AcMDQSYTe7F4KZr8isFvHn D/zcqhsd9eIcjBKFLyHC5NFElA3V6F38LWyfobZ2au0tl/FuxvcdzA8eaHyKrFYdmxZP rtBQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuae3kTctv0ZnBKgby4/5znoUSJFU4VnzeAO37Je/0X8M3BSfZf9 p27FLerZFD75ZKK8rxd1T+A= X-Google-Smtp-Source: AHgI3IYc7ke2NZenAoh9DzLwKjjyvDAttYEszQNaOy9Cged34T5itbRGX30iR/rFqfDkW3O3nCNAzQ== X-Received: by 2002:a0d:d8d6:: with SMTP id a205mr10489ywe.6.1549937347005; Mon, 11 Feb 2019 18:09:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:3891:: with SMTP id f139ls3412066yba.0.gmail; Mon, 11 Feb 2019 18:09:06 -0800 (PST) X-Received: by 2002:a25:24d0:: with SMTP id k199mr612919ybk.96.1549937346693; Mon, 11 Feb 2019 18:09:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549937346; cv=none; d=google.com; s=arc-20160816; b=usmky3mhPHrGQWPrMdZU35SWh0gJ7uR4za4hBVURMBn0rf+n+I5/bjwUFLvwpyJSkd DTBEmph7Z6Bw5pzv4xi1i7r/7iuL7BrDgHLWsjG4NCcjI0ujloA0rlFQTmo0w3AkHCEB wIC8U+KdjHtqPAwG2QVPq4TZH9My6MyN0eKQ0A2yyrHGuBX1fT/M3I2WxJVwRB4Hk9kh tYi3yvuMRu+ITwgI3QMfnkybEIQrq54WsOyubZtHXL8MvrZm5d8uIvS0yHrAWjj2b/BL f3uzMzT9sN9BPx4KPRW0bSmuiPNnKfT1ZKX8yfs9Vm+KoF8fWTgZ10JNBV0cSHR3A/gN X2JA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :dkim-signature; bh=wt758/tF7MVbJ0M5S6dDETV5hps5LZQQzEoGe4iFD1w=; b=H+W67ToDjeojmnhLcDpQym6i5XvXXzv2uX4bk0c0A5q/Wd6uveVSrtRtOhT7ALxwFH Dgd7QckUmz/s95socfptETg1FVVpAhj7xg58neUFb+un8uTQ3yAdZuErGDWcl1ftBvN+ U0+mgupTuVAimHdYWXBjmCbmq63pZUlMaasqDKcsirFsnd7R1pHGZNArVnc+uTjs/onq Ytc4mQLV2Tr6uKRRr4c1NHsDsvX1ayczasnuW8mepx/kRd5ZN2heFVSoy79SgNaTCtpa tXyEzNz+zoaUgnOfLbrUbeu1QLOcrxaxEGP8j1lEPOPTletodyqqCYV8QKovn9Y4Zzst hf8g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WN4w0FVJ; spf=pass (google.com: domain of jacques.carette@gmail.com designates 2607:f8b0:4864:20::136 as permitted sender) smtp.mailfrom=jacques.carette@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x136.google.com (mail-it1-x136.google.com. [2607:f8b0:4864:20::136]) by gmr-mx.google.com with ESMTPS id i189si499735yba.2.2019.02.11.18.09.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 18:09:06 -0800 (PST) Received-SPF: pass (google.com: domain of jacques.carette@gmail.com designates 2607:f8b0:4864:20::136 as permitted sender) client-ip=2607:f8b0:4864:20::136; Received: by mail-it1-x136.google.com with SMTP id r11so3474753itc.2 for ; Mon, 11 Feb 2019 18:09:06 -0800 (PST) X-Received: by 2002:a24:9f87:: with SMTP id c129mr662252ite.114.1549937345682; Mon, 11 Feb 2019 18:09:05 -0800 (PST) Received: from MacBook-Air-2.local (CPE00fc8d220633-CM00fc8d220630.cpe.net.cable.rogers.com. [174.116.130.236]) by smtp.gmail.com with ESMTPSA id j14sm5239092ioa.5.2019.02.11.18.09.04 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 18:09:04 -0800 (PST) Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Thorsten Altenkirch , Alexander Kurz Cc: Michael Shulman , Matt Oliveri , Homotopy Type Theory 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> <6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com> <5643E581-EE54-4CFE-BF75-A3AC274ABA16@nottingham.ac.uk> From: Jacques Carette Message-ID: Date: Mon, 11 Feb 2019 21:09:03 -0500 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:60.0) Gecko/20100101 Thunderbird/60.5.0 MIME-Version: 1.0 In-Reply-To: <5643E581-EE54-4CFE-BF75-A3AC274ABA16@nottingham.ac.uk> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Content-Language: en-US X-Original-Sender: jacques.carette@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WN4w0FVJ; spf=pass (google.com: domain of jacques.carette@gmail.com designates 2607:f8b0:4864:20::136 as permitted sender) smtp.mailfrom=jacques.carette@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: , Some of you might already have seen the interesting discussion "Set=20 theories without junk theorems" at MO https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems that is very much about these accidents of representation. Jacques On 2019-02-11 17:58 , Thorsten Altenkirch wrote: > I think it is rather misleading to think that 0 and the empty set have so= mething in common because in set theory they are represented by the same co= nstruction {}. This is rather an accident of representation, it is like say= ing that the number 49 and the letter 'a' have something in common because = they are both represented by the same bit sequence. > > Indeed, I think having access and being able to talk about the accidental= representation of objects as you can do in set theory is detrimental becau= se it stops abstraction and this is precisely one of the main advantages of= type theory. > > Thorsten > > =EF=BB=BFOn 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on be= half of Alexander Kurz" wrote: > > Hi Thorsten, > =20 > "When we talk about mathematical objects we think about typed entiti= es" > =20 > I agree, but does it follow that types and not objects come first? > =20 > For example, 0 can simultaneously be the empty set, a natural number= , an integer, a boolean, etc etc > =20 > The importance of the "etc etc" is that this list is not fixed in ad= vance. It can change during mathematical course. > =20 > This seems to indicate to me that objects come first and types later= . > =20 > Another example happens when I say that the dual category has the sa= me objects and arrows with domain and codomain reversed. The same object th= en belongs to different categories. > =20 > Do you think that type theory provides enough flexibility to model t= his aspect of mathematical discourse conveniently? > =20 > All the best, > =20 > Alexander > =20 > > On 11 Feb 2019, at 10:17, Thorsten Altenkirch wrote: > > > > I have got something else against NuPRL. It explains Type Theory v= ia untyped objects which are then typed. In my view there is no reason why= we need to explain typed things via untyped objects. When we talk about ma= thematical 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 th= e street and then try to find out which type it has. We are thinking of a t= ype first and then we construct an element. > > > > Thorsten > > > > On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on beha= lf of Michael Shulman" wrote: > > > > 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 "se= ems" > > because then someone says something like Jon's "Nuprl's underly= ing > > objects are untyped -- but that is not an essential part of the= idea", > > providing an instance of the problem I have with NuPRL "in prac= tice", > > which is that every time I think I understand it someone proves= me > > wrong. (-:O > > > > 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 equali= ty > > 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. > > > > > > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri wrote: > >> > >> It looks like Jon is with you regarding definitional/substitutive= equality, since he considers Nuprl's subtitutive equality to be alpha conv= ersion. From the old discussion about it, I had figured Nuprl's substitutiv= e equality was the equality type. I guess I'll avoid that term. > >> > >> So I'll ask a more concrete question. You seem to be more open to= Andromeda than Nuprl. It has a difference between definitional equality (i= n Jon's sense) and the (strict/exact) equality type for approximately the s= ame reason as Nuprl. If the theory you're using is HTS, then there's also p= ath types. So I gather path types are what you want to take as equality of = reference. Which is equality of sense? > >> > >> 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 equ= ality as possible (informal) interpretations. This doesn't mean there needs= to be something called "strict equality" in the system definition, for exa= mple, it means you recognize a strict equality notion when you see one. I d= on't know how to recognize the kind of equality you were getting at in that= paragraph. > >> > >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman= wrote: > >>> > >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri = wrote: > >>>> As a form of extensional type theory without any "built-in" imp= lementation proposal, it seems like HTS has no notion of "proof object" in = Jon's sense, 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 ha= s any "definitional equality", in Jon's sense. But it seems like HTS' exact= equality was considered substitutive nonetheless. In fact, it seems to me = like what Vladimir meant by "substitutional" was that it doesn't cause coer= cions. Either because it's definitional, or because it's subsumptive (my te= rm, from another message in this thread). > >>>> > >>>> So I think you're misusing those terms. > >>> > >>> Well, after many years I still have not managed to figure out ho= w > >>> NuPRLites use words, so it's possible that I misinterpreted what= Jon > >>> meant by "proof object". But if you interpret what I meant in I= TT, > >>> where I know what I am talking about, then it makes sense. In I= TT the > >>> relevant sort of "witness of a proof" is just a term, so "not > >>> perturbing the proof object" means the same thing as "not causin= g > >>> coercions". > >>> > >>>> You seem to be downplaying the differences between these notion= s. Why? > >>> > >>> Maybe things are different in computer science, but in mathemati= cs 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 for= mal > >>> 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 spect= ra, or > >>> all the different definitions of (oo,1)-category. > >> > >> -- > >> You received this message because you are subscribed to the Googl= e 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. > > > > -- > > You received this message because you are subscribed to the Goo= gle Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from i= t, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > > > > > This message and any attachment are intended solely for the addres= see > > and may contain confidential information. If you have received thi= s > > message in error, please contact the sender and delete the email a= nd > > attachment. > > > > Any views or opinions expressed by the author of this email do not > > necessarily reflect the views of the University of Nottingham. Ema= il > > communications with the University of Nottingham may be monitored > > where permitted by law. > > > > > > > > > > -- > > 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 G= roups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, se= nd an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > =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. > > 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 > where permitted by law. > > > > --=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.