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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x539.google.com (mail-pg1-x539.google.com [IPv6:2607:f8b0:4864:20::539]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 59ca44e6 for ; Mon, 11 Feb 2019 17:20:48 +0000 (UTC) Received: by mail-pg1-x539.google.com with SMTP id p4sf8796217pgj.21 for ; Mon, 11 Feb 2019 09:20:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549905646; cv=pass; d=google.com; s=arc-20160816; b=USQDsVtclK8SKncoQ3iCnPbhDxt+//FS1lVwQDfkDRGY1LREL48aV1EeoEbA2x+xub Yf3+iKM8BqrYyoBRkKbqCf75jDdGEEVXUhxCNwPLtFgd8G6Ah1OdlfQq8wddeUp8sZSH 9oZ6755SfkwkkQy/lrYVT4o/jc7pPCH9dA2J4pASUdnxtcvPHVUy9hwkrl1MAZ7OhJSO UZb2oXRmU3MeIxAQxQqPoDxtftIjZ3xiMj9Hg2eXupnqxwbkZEkzP2vxfcAqg2pwMlai 9R7hSADf4QsFXah6nbWBGlPLU9//AdZpU/tPBYyy5223gQ8JV8xETrRpvm/FRNlKMx3x hB7g== 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-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=Dpe+X23jy2eDDuJ5l8cmCliPTnxuVLafKQZNXLLUbkQ=; b=nRiXfc/HzBWGS5oOMFnmqnFQk+faCuivUq6H2nD+wvxyOtnrDdBf67F9A9Ir0hY9o+ TUoDzLW7TrevMWcQgMrwe1v5tFAtX9lNA/rGMinPah/UBTk/XeWt/AHuhsu3GjFc0saf bE8l3CduBaFbgnbvWmqAy8HtAxp9DQts+6i3spyCH/dkYTzRgPFTtzjWgejmT48eNYnu 8DVSjxtYX3IJ9Nw7qUfrgk2TQgHE4Ztzy1ibKCovvqLpkBICuNMFfyyx7oOfx79fQq1C rgDV77bjXcDXd8YdZs/bGXkLg4mZElQaPRbeOFtn528mujtruBITejBMbuG9HwSmJcDT g5Cw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=FXb1rtQp; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Dpe+X23jy2eDDuJ5l8cmCliPTnxuVLafKQZNXLLUbkQ=; b=CtiUUJvcZ2B9+glk/xoYbWM7tMk8NBkf9w4zBTWcESnYwy8s0Zf4CY0BACVVK2EsuC L5AHqhlEJ9myGlVeMERZnLG1PgPrxM6yx580XQjJpPkSCmJxLGPZBClFXp20j8IQs0aB otvbEX7Llv6gkTiU//hXVDkNR8qg5+R2kwsaaUFgoooIhHN2PS4jzezF6gf+Eovs3Kuf f4sKhQ9pxmrVYUDpboYgk2oVPCePwXbYgyYG8pX3DH6vymazkunGS/cDOZP9evAd3ZQW sohlNJRo59vgo0mcPifW7Qo9mxNQcmEkHTrBsgxrGU4j+HDmxG04Cm8puOi6Qp/ztxJ4 tzEg== 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:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :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=Dpe+X23jy2eDDuJ5l8cmCliPTnxuVLafKQZNXLLUbkQ=; b=EFWZgAGHN1/sUiDtIedv854TO7g5MngCaG5ZpaOAYxhNoBS5caPADjqAO0gwlBQra6 Fzi+Ke8RyNgDtgdfbnFp/ML/kFn2tpciVloTKxnoElTWwPcAFaXbaihmkZPiblQMeq3X YXxkbsAfHq3iRcV6AkL+drAfY0pzaZS/RIudPFkXbOcuOS+cuV69pRvw4VLB+Dxa5W/q 2QGSCvsEsz6aoHpffT+o6gShlj+U9uD7JzKcGC1Rd785pW/ikoABmzsFZgcWYX+IA5n/ P5NkEWzVaqEXWFl4dTcyf+vzKYjnIXX0my8DORIiY9bTIHd8D0GhDlzm8y52JaNtnwBr IC7A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZeS33AmpcDlA/Bi4ViMyou3PUQPYgmy2viYTFGGaEieTVYktSN MtnTCGg/Ci8A7MM8KqQtEEg= X-Google-Smtp-Source: AHgI3IbaVSt/LENWdVHQRwlL2RyIg8A/PnMRY7d6ToLD64QwpOwfXee6VWext2IJpmic51WqUVMy9g== X-Received: by 2002:a17:902:1c1:: with SMTP id b59mr103463plb.3.1549905646530; Mon, 11 Feb 2019 09:20:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:56d1:: with SMTP id h78ls6484804pfj.4.gmail; Mon, 11 Feb 2019 09:20:46 -0800 (PST) X-Received: by 2002:aa7:800c:: with SMTP id j12mr13200069pfi.128.1549905646140; Mon, 11 Feb 2019 09:20:46 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549905646; cv=none; d=google.com; s=arc-20160816; b=o58CSlXBhlb5G+00zV1IDCbW7hcQQMeWEMc4+KMSDfnLotz7v+rx06i5g7xusC8PC0 aOx72J14YwO8uaGtPxDTMZqSiEaUG0mkvEL5MbVf+H0//uRC/yzNlo/Fw6s8E9t9DEmA w3v8u3y66Lnc6ZpMfz3/hZld0QmG1SmxY2Z4i9VGIv4++uAsL9hEzusIqQkpzZ1Q0grr LLBYTZmgB6/UehonqN2VYIar/skOWQIQGFlRvb0UnH1DpdtfdBF7fOLn8J/T9B/cVvA9 0P+Hcp+UQubdJu5qDqGkcMSECb4a3EFQ07c3KOYQkN/HpNOyfzhcsk0Z9v4MCZCq90RB lF0Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=9vLBz4m456NOUM7Tgi84iZFHmnw1J5A544aT4XllpeY=; b=BrLoxeQu6yc4kZrPN6xU1WaQmueyX1oGAhH0oNlop4IDKWHe1o0vrBwIW/zzZ3469Y mwkW+193wxhy0Ckgak/opPw4S09WwzZXLVSFuErGHg59RJEZ6bcutqddSIYK2Fe9zCQ5 Pbv9h1AkVbvbs+bWW7SC2u4K6uZlRMPK7hItXKk2bH6H/Ws2sjZPcSQKMq5GXF3V5BVa uNbuSjqepLcU8OtO6cuBzRt3j/wociLVZsExDCAQH5rrYHANXwsC18C7JmiMIAHlH+iV R1VcpUAqqqedd5sX1/7DTBNWDjn0mbKlA22vCks6ZHf4ztmmfjL6qCM4JoymfvHo4MIr 3PKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=FXb1rtQp; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc32.google.com (mail-yw1-xc32.google.com. [2607:f8b0:4864:20::c32]) by gmr-mx.google.com with ESMTPS id f6si478287plo.5.2019.02.11.09.20.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 09:20:46 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) client-ip=2607:f8b0:4864:20::c32; Received: by mail-yw1-xc32.google.com with SMTP id n12so4466637ywn.13 for ; Mon, 11 Feb 2019 09:20:46 -0800 (PST) X-Received: by 2002:a81:100a:: with SMTP id 10mr5957029ywq.341.1549905645157; Mon, 11 Feb 2019 09:20:45 -0800 (PST) Received: from mail-yw1-f48.google.com (mail-yw1-f48.google.com. [209.85.161.48]) by smtp.gmail.com with ESMTPSA id s68sm4132873ywd.85.2019.02.11.09.20.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 09:20:44 -0800 (PST) Received: by mail-yw1-f48.google.com with SMTP id x21so4469346ywx.11 for ; Mon, 11 Feb 2019 09:20:44 -0800 (PST) X-Received: by 2002:a81:7cd:: with SMTP id 196mr28837512ywh.255.1549905643974; Mon, 11 Feb 2019 09:20:43 -0800 (PST) MIME-Version: 1.0 References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> In-Reply-To: <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> From: Michael Shulman Date: Mon, 11 Feb 2019 09:20:30 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=FXb1rtQp; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , 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 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. On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri wrote: > > It looks like Jon is with you regarding definitional/substitutive equalit= y, since he considers Nuprl's subtitutive equality to be alpha conversion. = >From the old discussion about it, I had figured Nuprl's substitutive equali= ty 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 Androme= da than Nuprl. It has a difference between definitional equality (in Jon's = sense) and the (strict/exact) equality type for approximately the same reas= on as Nuprl. If the theory you're using is HTS, then there's also path type= s. So I gather path types are what you want to take as equality of referenc= e. Which is equality of sense? > > Regarding the paragraph I said was vague, my complaint really is that I d= on't know what you're getting at. I recommended strict or exact equality as= possible (informal) interpretations. This doesn't mean there needs to be s= omething called "strict equality" in the system definition, for example, it= means you recognize a strict equality notion when you see one. I don't kno= w how to recognize the kind of equality you were getting at in that paragra= ph. > > 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" 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). >> > >> > So I think you're misusing those terms. >> >> 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". >> >> > You seem to be downplaying the differences between these notions. Why? >> >> 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. > > -- > 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.