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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 52383bd6 for ; Mon, 11 Feb 2019 20:12:01 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id 4sf211172otg.3 for ; Mon, 11 Feb 2019 12:12:00 -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=OfTbMh6V5AEoFqCBLDuRHXhwU25t0njAjPC7XK3TUc8=; b=Ov8JUHzXTT3u9b1zO95hsaY+vpz04dqh/C8VVX2R8XtF+W6LqBj/Bae4C7sfcZn3/k nGH1NnAkMQOOKweQ/O6LLihXo8D4Y0uexT4aA3ZVxc2ahGSpsqlOTm3T6GHNPItzJLAQ jShS5xeFtFfWlko9Jx0ebUBKd/OYRtv03rQ752KW23PxcpHn4DQPpkMm3OJo5HCU4b+h bjGakFCn8OoPfjNhquuUDSwM6pn3kBhi3c8Nqeq04kfCSCDLL9x/7JRnfuc8xaE9iYm5 pzLx3DH1P+NWTY76455ZUMbWjRMM6IYPwA7YgWBTYU5V/hHX/hnHoglhsHXxhVOKJN17 rwyA== 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=OfTbMh6V5AEoFqCBLDuRHXhwU25t0njAjPC7XK3TUc8=; b=Skdt0/KBPSp9JZp8NdQFcL2zmbah+oYaV77UJGm+JC/amPXeCog9Axb9pgumTRBy2v f1PC7rOrERjFPdlCT1wadFLjyqCsrVaGzIaUik1p5THsUJ8RyE7FF5v4PsvEPSX2miGO mkGkhJC6EZg96vlNgnGraioa2qmUqoj8b5rE0roC4Cv1PDq1Bv78FHL4aaKG/HPy7KIZ VidnrqGrREi7S9yuLpARNkyl6MDjTMC7HvGyqw2IlqmO8V3jtkMQQNMnIJHXa5L9ZsdT H4muT4/GHBlzMU6I8HWZLYAO5Nzk1KxMYIPMcsUaEgwvsEhRsHeelf3i+R5eVKXSrjbw TzYQ== 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=OfTbMh6V5AEoFqCBLDuRHXhwU25t0njAjPC7XK3TUc8=; b=cCPKHaqS6cYy+CIb0ZverEa9H48mH4ogZb59flNzi2soUkSlAY6DYnuItAODhBYEj3 Ugx8eRLHq1V60y8Z+gdigzMzjsDwI9jpfTD0Ou77ig77rZU9XA5rXSKlgpFhyEY3iihE 3s+gyN0OAk1FNQxRV/wlp4G9OJhVVQF0+9pjAFsX4BW/WXEo1NXJ36yKiFk19XQOipn9 bsD6rJouG0SDLORso/BT6tSyYLGbCQA45wRlmtNi2b6yXrw/e79JWdkKqw7FVVuWKMTJ iiwTohsay3ZMjP6dYMlVOUQZQ4tldQ7hhFdTzjdTlyL2ON3XKjlYFMsJz1/Y2HEysHWG eHdQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZ8VhGsfyrmAkey3OyTtlN8FxHdDDoXRh3RVJdvxSsr8ME6kaj3 ADQxonXL8NFiFxtqjNiuiW4= X-Google-Smtp-Source: AHgI3IYNG5L3YEL0cLYxtzdpaAeh7v2TSJCugu5TR7lZ7BMwYOKMkdnQ5adTteXvZ9ICki9EMvPirQ== X-Received: by 2002:a54:4d86:: with SMTP id y6mr5183oix.0.1549915919860; Mon, 11 Feb 2019 12:11:59 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2c62:: with SMTP id f89ls8794888otb.2.gmail; Mon, 11 Feb 2019 12:11:59 -0800 (PST) X-Received: by 2002:a9d:19a4:: with SMTP id k33mr334752otk.5.1549915919003; Mon, 11 Feb 2019 12:11:59 -0800 (PST) Date: Mon, 11 Feb 2019 12:11:58 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <04b2d9c0-83e5-4a60-a5a0-8adde80d5a5b@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_1356_783582909.1549915918368" 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_1356_783582909.1549915918368 Content-Type: multipart/alternative; boundary="----=_Part_1357_1725453936.1549915918368" ------=_Part_1357_1725453936.1549915918368 Content-Type: text/plain; charset="UTF-8" You'll have to ask Jon about what "idea" Nuprl's intrinsic untypedness is "not an essential part of". I'd say the most important thing about Nuprl is dependent refinement typing. In particular, Nuprl is extrinsic dependent typing, since the intrinsic type system is trivial. That turns out to be very interesting too, but makes the approach less broadly applicable. I have some outlandish views about Nuprl. I don't consider its PER semantics to be a model, in the usual sense of model theory. It's proof-theoretic semantics. It's a semantic justification of some proof principles. Kind of like a strong normalization proof for ITT. You can point out that it's technically a realizability model. But I'd say that's because the terms are realizers. *What are they realizing?* That would be a model. The model theory of Nuprlish systems is currently virtually nonexistent. Somebody ought to fix that. There's a set-theoretic semantics (actually two, and they are different... sort of) for an old version of Nuprl. That's it, AFAIK. 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. > -- 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_1357_1725453936.1549915918368 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
You'll have to ask Jon about what "idea" Nup= rl's intrinsic untypedness is "not an essential part of". I&#= 39;d say the most important thing about Nuprl is dependent refinement typin= g. In particular, Nuprl is extrinsic dependent typing, since the intrinsic = type system is trivial. That turns out to be very interesting too, but make= s the approach less broadly applicable.

I have some outlandish views= about Nuprl. I don't consider its PER semantics to be a model, in the = usual sense of model theory. It's proof-theoretic semantics. It's a= semantic justification of some proof principles. Kind of like a strong nor= malization proof for ITT. You can point out that it's technically a rea= lizability model. But I'd say that's because the terms are realizer= s. *What are they realizing?* That would be a model. The model theory of Nu= prlish systems is currently virtually nonexistent. Somebody ought to fix th= at. There's a set-theoretic semantics (actually two, and they are diffe= rent... sort of) for an old version of Nuprl. That's it, AFAIK.

= On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote:FWIW, I think the only thing I h= ave 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. =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.

--
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_1357_1725453936.1549915918368-- ------=_Part_1356_783582909.1549915918368--