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-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c0a15a29 for ; Mon, 11 Feb 2019 15:09:52 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id a19sf11418004otq.1 for ; Mon, 11 Feb 2019 07:09:51 -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=ahAfEAzfuj7Vts9qQ5uwcE8KXMsDci5oDW/kGRVqKmk=; b=tkFC03U1NlMdWVl9ZNYTjCSQBBvshbbWSmLIwQBBkVum9IxzcDJ0XiB5VPFD+kZ3yf Kaj+04nR+WPPauz5xAhFSsIgN4BaXxCGP83y8QdUcJC7E8/AAar8cH08zwyxsz6Vf1r+ GMbeE+m5zEhwU+gyGV5LICVF/SI9jJWK09Gmf4ujKpphoRAmySpp+ZhKEFupL34uuiIH H1M2lkPD92vBmAOZe87KtKlzYJZR6QFjSUUKCKaCvnNsP+yc3tisW9de8vP0WdLlcJXV 2ekRKtm2cp26H7FxMExj0nULihP64SGrVF5yqFnvP2ZduOLijceip6TFKHC7ijTka1M7 o4WQ== 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=ahAfEAzfuj7Vts9qQ5uwcE8KXMsDci5oDW/kGRVqKmk=; b=YFLwCcQ3aSvp0IA0GCJDYYEwWTufgpmwuR6eITp5uz1kLknG/NLjmIlXq9uN3KhnX3 GK2UN6X6xATRPu7geloRHRCB0molt3EBXuzKaw2fST3ONFLrXyVsFPqSa7Fsns2T2q1w Q5t58VlJZ5EELeVetyxoDQnVHnIF3QEUQ61TSBHhdtsS8HhuBx+pGdRTMDRtE5gtS+O5 g7Xhm7197jSLAFzdPz0Mp6u0jnAHyijQXCZG8CtisVW2XDlWs84QAC2iGHegd4epDOQW gM0Wzm0mfft2jlmpvBgCis2J2QU4ZbP/SPgbs05C+IFpesO2R6F28X24AFt5QJno/3HZ 55Kw== 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=ahAfEAzfuj7Vts9qQ5uwcE8KXMsDci5oDW/kGRVqKmk=; b=b+DujliiPZHV7OqMqqDbaPpM+ihtkorOZp1P4riTzEZlU3yYYkfxLueDIVWEHkN3Hg 6tQGuzjFrhg9snr1FZ5wQ61thcZjZWg8BMuATGE+cVRCB33AUjdVxDZVfvqiCPcvWW99 ifjT8eyo93drSML++6SKHlGps0xFfLTMcyv5WgO9Hl3k/pubzEY80FOZWbT6OtJ+8E31 rgmtZ2qpjLUUnyGltnG2z0y9kzNkwpKr1hYPJFj0cJsstfy2l8zG3JE+zZq89lezMLWV plWFjx011hpRHcuIFGHsiM8kwx+ZKWMUwaMrwsGF9JSitU/bgevL3PAiqgLGQ8refLJw ZIWw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZLoDH5uV62jxJjdzhZfqpM5Mfu+8pn0KoIACSAJIVn8ObvRaQO 5a5TiqwsEFtJHNVP3eOFGC8= X-Google-Smtp-Source: AHgI3IaUf5y0VgI0WugQYdga1pk/sVw+37c7vCvfJWp8Ez+s2htyURap9081oWsNX0IHH8Aqnxr5Hw== X-Received: by 2002:a05:6808:208:: with SMTP id l8mr93857oie.2.1549897790731; Mon, 11 Feb 2019 07:09:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6409:: with SMTP id h9ls7961412otl.8.gmail; Mon, 11 Feb 2019 07:09:50 -0800 (PST) X-Received: by 2002:a05:6830:1212:: with SMTP id r18mr336999otp.0.1549897789882; Mon, 11 Feb 2019 07:09:49 -0800 (PST) Date: Mon, 11 Feb 2019 07:09:49 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1221_1936526597.1549897789261" 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_1221_1936526597.1549897789261 Content-Type: multipart/alternative; boundary="----=_Part_1222_2078479294.1549897789261" ------=_Part_1222_2078479294.1549897789261 Content-Type: text/plain; charset="UTF-8" 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. 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" > implementation 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 has 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 coercions. Either because it's definitional, or because it's > subsumptive (my term, 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 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. ------=_Part_1222_2078479294.1549897789261 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It looks like Jon is with you regarding definitional/subst= itutive equality, since he considers Nuprl's subtitutive equality to be= alpha conversion. From the old discussion about it, I had figured Nuprl= 9;s substitutive equality was the equality type. I guess I'll avoid tha= t term.

So I'll ask a more concrete question. You seem to be mor= e open to Andromeda than Nuprl. It has a difference between definitional eq= uality (in Jon's sense) and the (strict/exact) equality type for approx= imately the same reason as Nuprl. If the theory you're using is HTS, th= en 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?

Regardin= g the paragraph I said was vague, my complaint really is that I don't k= now what you're getting at. I recommended strict or exact equality as p= ossible (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.

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 <atm...@gmail.com> wrote:
> As a form of extensional type theory without any "built-in&qu= ot; implementation proposal, it seems like HTS has no notion of "proof= object" in Jon's sense, which seems to be formal, checkable proof= s. It's not that you couldn't come up with one, it just isn't s= pecified. So I don't think HTS has any "definitional equality"= ;, in Jon's sense. But it seems like HTS' exact equality was consid= ered substitutive nonetheless. In fact, it seems to me like what Vladimir m= eant by "substitutional" was that it doesn't cause coercions.= Either because it's definitional, or because it's subsumptive (my = term, 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 how
NuPRLites use words, so it's possible that I misinterpreted what Jo= n
meant by "proof object". =C2=A0But if you interpret what I me= ant in ITT,
where I know what I am talking about, then it makes sense. =C2=A0In ITT= the
relevant sort of "witness of a proof" is just a term, so &quo= t;not
perturbing the proof object" means the same thing as "not cau= sing
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. =C2=A0The 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. =C2=A0Indeed, the presence of multiple forma= l
approaches to the idea with different connections to different
subjects make it *more* important and provide us *more* options to
work with it formally. =C2=A0I 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 &= 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_1222_2078479294.1549897789261-- ------=_Part_1221_1936526597.1549897789261--