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-vk1-xa39.google.com (mail-vk1-xa39.google.com [IPv6:2607:f8b0:4864:20::a39]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 771069c5 for ; Mon, 11 Feb 2019 21:50:20 +0000 (UTC) Received: by mail-vk1-xa39.google.com with SMTP id y72sf191084vky.14 for ; Mon, 11 Feb 2019 13:50:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549921818; cv=pass; d=google.com; s=arc-20160816; b=RzbKNuutIfRXYCdEUNsuD9lEERrAnBjV+Wwkg5zBo4dJpIqniKWzYItk+lTv8kWTTS RmAerIV+6Jdn+FY2FxBHaj1PhFQtBGsCoUC9+fQlpf+rz00GTpxDVwcQLh1A5qZimc2M TWDiyl5uT0nETBYyVU5Yjtg+QIgTWYO3zBM/juamnoPmAxIuXQzc61KDd4X9PBiF5sxR BPx52W8Y+8axNkMbwS7SyuJ7bN25l97fcC1/MWN3z7zhv60iJbsPrbw90Dt8QokfEe0w NbZfuavWK/cbSRMLwM6gX/DNB6/wJDLrcRj+6Hq8rvipO7Jx8/HUClgoGhB/IAfK3dO2 0lsA== 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=o7asdnSMfLOThhXEgyobPQ7IkRJSGcawcCJi+Kp2VSk=; b=pctl5tqjO2Ro/LbE0zfPLj3lLnq3ZgJ7ZHL+46mhbJmwUDKjPkiFM4RuiSrjdBZ2Nv XjJrbAdmO+d67bDfN31J/0EuFwKbhZvrskXFbVnD4uzSezgGlBowFY8sUeG7Uugu0jYw irNgihsD1kvsGtSRsOUAjKEJA8I/i+fJaaPprEVqMiHf4KN4F+YZLIfA5SinMW4dS49m FIwCPRkqy85SRfc5TywgJ/UQM4qIZCvwvYtu7/ajuYUn6GCWlCdxrh+akXU8Whop84z0 5tvvHEdqAsFw0GCCMSTS2VSn7NEoM0mw9fw3nDD/dPmcYOeq2iEsUxmBq3Y02sla/48t fNOg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MEyE0s1+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 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=o7asdnSMfLOThhXEgyobPQ7IkRJSGcawcCJi+Kp2VSk=; b=KriReMjo0zj6XGvfnTmqfHWagpE/Dv3a311CSWMFw9zYn78+Nz7c/q8SxG8XQKGcid oMlBHJJNQVbJSnjcPDQWed9shVxEvbYiNKppjG+R+mitIi62/Zh53JlJKNpabXaUZ7iK sQutFpdAt0xRP7UIKieTDLkLYoytLDcCVRD+ZCkHQUD0OO4zTlhyVn95OHgQKnt51ZF1 dE4wMRy7vMhtFnQMNB+mfQ1ZmETZ6lwNj0JmrUBhLeVHxBQDp/mwtEeIw9riJy0R0EeE u+TGlqGf5MihVdRDXyEsF7n8sX5ldFVMjBzH+71PwCcb3Ck3E2k/o+H+GViBNbUDmYc7 qnvw== 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=o7asdnSMfLOThhXEgyobPQ7IkRJSGcawcCJi+Kp2VSk=; b=fSX+RbBOl9YcXyp4GdWF8/7nuLHlL11VvVBsfFO5noN20ZItsx3f5A7kjMOUb3xu8D o95EwhD0UcB57NNrhL+d7F7rXM5N2vSGM/hLMUQaDvTWBb1U8bZiq+drbMBMGT5I5sRZ U4EWaC79xC3wmqoS/vXYHHK5EgWD7DUkHCV49fZGzBvy1CCKMJUFVbUv7QO3oHZbWiJd PEMt6ARkJIRRJt/CdJPQXQ3jl/iH4Ghq8HsmGEKknhr73Dxejy0wUBAGioFLV1BNV7ER X9y3mceRTEp+lZoaN5OcOgojbugkE1WQQwRe9AhMeDkdiJt3gM1Q6T+EiEEk52zUmsp5 VEqQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY1hnQFBGhe+JtMcm7bZnuHmoPS2vh0E1kgssoOfPyStiq18q4u ZzcA5bUsEDg78St3K6Q/t88= X-Google-Smtp-Source: AHgI3IaJxyb7tR6k6n7Y83PwYQv7iO1GyoTnRmLbgV3jgrd0jW0V3kAb9K0ZNZA+bxgqg7ojb4KgGQ== X-Received: by 2002:a67:64c1:: with SMTP id y184mr683vsb.7.1549921818671; Mon, 11 Feb 2019 13:50:18 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:3255:: with SMTP id r21ls1474285uan.3.gmail; Mon, 11 Feb 2019 13:50:18 -0800 (PST) X-Received: by 2002:ab0:2008:: with SMTP id v8mr297090uak.20.1549921788381; Mon, 11 Feb 2019 13:49:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549921788; cv=none; d=google.com; s=arc-20160816; b=j+M1yOt4e/xzXzNVSMgSMv0x5NjNG54wmMSeeRFpBoOSMeAPEpXeIUm3YiHir8CmRd uElTcG+zkg034nRGDN301el8XkZT+GLFoGfgtKBP/w3e/AAJaPSsh9CWmjtr1DFEPUum KPSHFowXBLpCUqu9hdssLMX117MU3Gc8CmhPG3n4mY/YQrsxY9SIF/x6Hg6EIDHy6ySO hD0VCLqyQOwCbb0BTVU96E6jSzrTAcN0IP9q4vI52Q16doc2oIilU3Ta8DUi/BiFoGpl JBgK/LdyTzFmeF+lZS/3BMUMtcrHESAs/nGoMarbPij7o8MFxmrem5RvxgOYxhvZb51c +5FA== 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=XWPGUdS2R6OI84QzQUPNWWjVv7NXVwHh/CNgbhd1yk8=; b=G+sLYZWWOsWM5haAfmz//Nx5WDuWHmDVamTHq3ejm94QjWYBWpDlEy2arFkp5udex5 yp/Ipm28nVOHelpxnBqQTBwKPuhkEse8qv/JIfkRFvGGkh8aFAL0xGlyJpEGX+v9DRPv bKrTJlh1CRjZuACXt4+donfmwwuEyvFyHpzPi3pxa8HtXp9V2HIxwRgSeZ6VkBkKqgyR 7YaX9eJMZvtH3w3r6gsCWjZGVst0eR0x9itlKxu/olrKr6SfotXluc5XsnmJKoTbI/BS h8dZikZUoxxS1vL+E2dujFNLW5MUTpzuQ5OWrGIpfdgppys4haCeDPicZuaGnVt0PdzO 067A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MEyE0s1+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb32.google.com (mail-yb1-xb32.google.com. [2607:f8b0:4864:20::b32]) by gmr-mx.google.com with ESMTPS id x65si896459vkg.2.2019.02.11.13.49.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 13:49:48 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) client-ip=2607:f8b0:4864:20::b32; Received: by mail-yb1-xb32.google.com with SMTP id j189so190893ybj.9 for ; Mon, 11 Feb 2019 13:49:48 -0800 (PST) X-Received: by 2002:a25:d254:: with SMTP id j81mr287700ybg.71.1549921787882; Mon, 11 Feb 2019 13:49:47 -0800 (PST) Received: from mail-yb1-f179.google.com (mail-yb1-f179.google.com. [209.85.219.179]) by smtp.gmail.com with ESMTPSA id o76sm2568438ywo.106.2019.02.11.13.49.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 13:49:46 -0800 (PST) Received: by mail-yb1-f179.google.com with SMTP id j189so190944ybj.9 for ; Mon, 11 Feb 2019 13:49:46 -0800 (PST) X-Received: by 2002:a25:4e8a:: with SMTP id c132mr287159ybb.458.1549921786464; Mon, 11 Feb 2019 13:49:46 -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> <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> In-Reply-To: <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> From: Michael Shulman Date: Mon, 11 Feb 2019 13:49:33 -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=MEyE0s1+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 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: , Well, I can't tell exactly what Jon meant by "I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'.". If he meant that an entire typing judgment "M:A" is only "definitionally equal" to a typing judgment "N:B" if *the very same derivation tree* of M:A counts also as a derivation of N:B, then in the ordinary presentations of *any* ordinary type theory I don't think any two judgments that differ by anything more than alpha-equivalence would be considered "definitionally equal". Look for instance at appendix A.2 of the HoTT book: coercion along judgmental equality is a rule that alters a derivation tree. What it doesn't alter is the *term*, and since Jon also said "In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi" I assumed that his "proof objects" in a MLTT-like theory would refer to the terms rather than the derivation trees. Regardless of what Jon meant, it seems to me that insofar as "definitional equality" is distinguished from all these other kinds of strict equality, it should refer to pairs of terms (i.e. bits of syntax that denote something in a model) that are *equal by definition*. For instance, (\lambda x. x^2)(3) is equal by definition to 3^2, because \lambda x. x^2 denotes by definition the function that takes its argument and squares it. I think this is roughly the same as what I would mean by "equality of sense", although the latter is a primarily philosophical concept and as such cannot be pinned down with mathematical rigor. AML programs do not denote something in a model, and I can't think of any sense in which two of them could be "equal by definition". A judgmental, strict, exact, or substitutional equality might include only definitional equalities, as in ordinary ITT, or it might include other non-definitional ones, as in ETT with reflection rule. So I would say that Andromeda with its reflection rule does not include a "definitional equality" as a distinguished notion of the core language. However, when using Andromeda as a logical framework to implement some object language, one might assert a particular class of substitutional equalities in the object language that are all definitional. On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri wrote: > > Jon's definitional equality is based on proof objects. The Andromeda term= s aren't proof objects, since you can't check just a term. So the fact that= Andromeda terms don't have coercions for strict equality doesn't do anythi= ng for definitional equality. I would guess AML programs should be consider= ed the relevant proof objects. I'd say definitional equality in Andromeda i= s pretty interesting, since algebraic effect handlers let you locally add n= ew automation for equality. But it can't be as rich as strict equality (if = you have e.g. induction on nats). And globally, it sounds like it's just al= pha conversion. > > On Monday, February 11, 2019 at 12:20:46 PM UTC-5, 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 "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 equa= lity, since he considers Nuprl's subtitutive equality to be alpha conversio= n. From the old discussion about it, I had figured Nuprl's substitutive equ= ality 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 Andr= omeda than Nuprl. It has a difference between definitional equality (in Jon= 's sense) and the (strict/exact) equality type for approximately the same r= eason as Nuprl. If the theory you're using is HTS, then there's also path t= ypes. So I gather path types are what you want to take as equality of refer= ence. 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 equality= as possible (informal) interpretations. This doesn't mean there needs to b= e something called "strict equality" in the system definition, for example,= it means you recognize a strict equality notion when you see one. I don't = know how to recognize the kind of equality you were getting at in that para= graph. > > -- > 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.