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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 73d23e46 for ; Mon, 11 Feb 2019 19:27:25 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id q11sf15070otl.23 for ; Mon, 11 Feb 2019 11:27:24 -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=HQdb8lJPKsbUhjwecQ4KTSpTy6WyhVyuj6WlaHc6sqc=; b=TBv2fnJSmx8VjNURlmywtYYUjP3DqLM2gpWt5W2h/C0nCZUzMHwDMpf4w+JtA1Yj4m jtGN+wQ0YjkrIkBz2CONQgehq7lEkttcyPUqi8/RT/SeEhoEhr5dqeBoMz0wIj5eqhhf VH+Av5SgeSos6vZMS4JAYzCOKxfYOCCky3yjtA9tJk1sI2Qlnoc6NjCgbERK0Nq6b/Lm /K6/GYyJ2h4EK/69Z9mq0CwT7956jWRrkoUHoAqsddn1Z5G7y19/OA5JYOXofUyLToVr 2EGcvTdnmFAnMm2duLbB3PDOuJc8e3DgWjtah9DvOGhE1a8cvpwAsHCtvW5aRBaiSXKd 4ygQ== 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=HQdb8lJPKsbUhjwecQ4KTSpTy6WyhVyuj6WlaHc6sqc=; b=Icdtn/Xg9iYt6FFIu3yJEdzfuYmGg14s1icX4tArPYMM1no29Uf4jHB12bjWyeg5AR SCKkWUUBZkgPzdIzFcKO1L77dplvxSlHh3hO4FwF+9mxrNGsfyAN0pna1YmUdXHAm5b1 9WQ+blNuz2Mo8EvIkAKXy5VMzajy0TkGjV68PTXBihmsEWaJ+bWNziZInaZ08vC0dO/W ZXXwOySzbLx7jDUaJhIERF4G731xY0/njUa7PeH9R1ASQXnRyM57Uf4Ucd1s+gBdPDC6 3qjJz6T+ZafRTfQeTfDG8ks3se/jGxEhV8CCIrh0tGmJn5L6ND2NpBeUewVxayxB4BFg LLfg== 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=HQdb8lJPKsbUhjwecQ4KTSpTy6WyhVyuj6WlaHc6sqc=; b=MZFNrfRikjcvPoe5S3RV0fSuL+PCgnnuMV/A6ZqhNRaZbFrs+8h19yfpYbMskZpcHC bHYZ21zjoFhF5vzMNQxoFVhr8bQcWK2+hp5Xd+PqeguNpp5KpAEXYUiJOuI82DwNn99W w6GTj9pffmgEqocyLWRRS1asRg0EckKCpKlsi/df2XPEX195SKJ/NTh+9sc8oB82Fyuc CGqlNo3Jvu0XEbgOVVXM3iu4KvABija5dkOSm1AqhYlwj13l20MYQrFhWiXVKbSCYSyb /xk4HuhlmcMcS5ZPt9N2/SNyU6NEIzlIFoAeUp1xQ/1Xb43sdAQGuPkfgnNFTN50zS31 FJVQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaIC+ueRjAjJmuUL4F3vsx/qqK9BfVvdPaP3PRl3UuxzXHgObwl 2icaclVzNuYJZsmAXuBz6Jw= X-Google-Smtp-Source: AHgI3IaoiCJzMdiQ9714SFBRmEeymO4G3ovjXAnWoBVq85jmtcc3sh8SZ3kZJJjulxi5VzoEzbUsJw== X-Received: by 2002:a9d:19a4:: with SMTP id k33mr331152otk.5.1549913244297; Mon, 11 Feb 2019 11:27:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6485:: with SMTP id g5ls8467124otl.6.gmail; Mon, 11 Feb 2019 11:27:24 -0800 (PST) X-Received: by 2002:a9d:da3:: with SMTP id 32mr502891ots.3.1549913243900; Mon, 11 Feb 2019 11:27:23 -0800 (PST) Date: Mon, 11 Feb 2019 11:27:23 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1357_238374263.1549913243137" X-Original-Sender: atmacen@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_1357_238374263.1549913243137 Content-Type: multipart/alternative; boundary="----=_Part_1358_763669374.1549913243137" ------=_Part_1358_763669374.1549913243137 Content-Type: text/plain; charset="UTF-8" Jon's definitional equality is based on proof objects. The Andromeda terms 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 anything for definitional equality. I would guess AML programs should be considered the relevant proof objects. I'd say definitional equality in Andromeda is pretty interesting, since algebraic effect handlers let you locally add new 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 alpha 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 > equality, since he considers Nuprl's subtitutive equality to be alpha > conversion. From the old discussion about it, I had figured Nuprl's > substitutive 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 (in > Jon's sense) and the (strict/exact) equality type for approximately the > same reason as Nuprl. If the theory you're using is HTS, then there's also > path 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 equality > as possible (informal) interpretations. This doesn't mean there needs to be > 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 > paragraph. > -- 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. ------=_Part_1358_763669374.1549913243137 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Jon's definitional equality is based on proof objects.= The Andromeda terms aren't proof objects, since you can't check ju= st a term. So the fact that Andromeda terms don't have coercions for st= rict equality doesn't do anything for definitional equality. I would gu= ess AML programs should be considered the relevant proof objects. I'd s= ay definitional equality in Andromeda is pretty interesting, since algebrai= c effect handlers let you locally add new automation for equality. But it c= an't be as rich as strict equality (if you have e.g. induction on nats)= . And globally, it sounds like it's just alpha conversion.

On Mo= nday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote:FWIW, I think the only thing I have a= gainst 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. =C2=A0I say "= seems"
because then someone says something like Jon's "Nuprl's un= derlying
objects are untyped -- but that is not an essential part of the idea&qu= ot;,
providing an instance of the problem I have with NuPRL "in practic= e",
which is that every time I think I understand it someone proves me
wrong. =C2=A0(-:O

Can you explain the difference between "definitional" (whatev= er that
means) and "strict" equality in Andromeda? =C2=A0Of course th= ere is the
technical difference between judgmental equality and the equality
type, but that doesn't seem to me to be a "real" differen= ce in the
presence of equality reflection, particularly at the purely
philosophical level at which a phrase like "equality of sense"= ; has to
be interpreted. =C2=A0As 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 <atm...@gmail.com> wr= ote:
>
> It looks like Jon is with you regarding definitional/substitutive = equality, since he considers Nuprl's subtitutive equality to be alpha c= onversion. From the old discussion about it, I had figured Nuprl's subs= titutive 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= (in Jon's sense) and the (strict/exact) equality type for approximatel= y the same reason as Nuprl. If the theory you're using is HTS, then the= re's also path 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 t= hat I don't know what you're getting at. I recommended strict or ex= act equality as possible (informal) interpretations. This doesn't mean = there needs to be something called "strict equality" in the syste= m 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 yo= u were getting at in that paragraph.

--
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_1358_763669374.1549913243137-- ------=_Part_1357_238374263.1549913243137--