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-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ef9211f0 for ; Tue, 12 Feb 2019 11:03:47 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id t13sf2272281otk.4 for ; Tue, 12 Feb 2019 03:03:47 -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=WaadVkGmXJ5mM0N153bRiJ79cVhtPspl52e7EEsBdfs=; b=WkpULc6jYYT+WbdBGNS1xjaI6H6qFm0W3H5eLB7slWL8g5QLMwP70GomhIeiVE9Udz 4tCHok2ddShKb1bBnwOBqwcg0iqHjPxLow+Z60XxkHk1aUQX/GQxkd6SiIHUl6qbpsBz Yg8wEgidUJBnvtN39Fvb/QMdRL9kvg9YFnk5iy5gVkFqIczLzjN2d8qxYDv3jqh8D/bf aEWX21zeF+Kth76jFsbgMgSzzpAMbZ0qHYE/5breyM8cMU4NWHRPAVZWxB9YDxPmvnVC ixBHsHTar6It3Zv7sSX3NdHUzbbqMvfJoXW/7SqYM9o+gBIy14c5oJ7jtyFSljFLETvw SRCA== 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=WaadVkGmXJ5mM0N153bRiJ79cVhtPspl52e7EEsBdfs=; b=AJXPLwAbkg9Axq/AqBIoNqmSoT1SvkttGv0u3oV1vUjwP1J5bYss5cHoOS4p/LgtEE x0AesKXl2EUOpNGaraCbL0Q4rX0s9sqUBDJp/JkTACDa4QpEa1wMDlT9hgQGk90xCkta xCJumRCfnW247JvJLKyZm4uob7IvSTgr65q4tYGsf5TIN5qcBTFNMuprdp64OlLxty5A +nsezTU5q64DjFS0WDM1ca6AqTW45+CYTlF2k362CPUQudWgCHiQwmMYy4ds/w8c9HIN tLnkSnHpWxWQZpw1tK9nymb/UWCQjWWXbiAjXluws2Z5Br0x3ZWaG76oReBZVvUZRyov VE0A== 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=WaadVkGmXJ5mM0N153bRiJ79cVhtPspl52e7EEsBdfs=; b=VYdf2baej1SrXnB9X1S8ZPCBr0H9CsNtAt8vGT5+dst4WGOaUZCmDCgkQLNa/spEXQ I7eXh2jP20RrXa6Ax2W8U9LKiuxlezddrwP5nLuKdwuWtxLv9hQ1n3Ubqx+GXOLhvucV sqEGyA0CXVpzvY49PDSFq9JgbqyDCZht6bxRCs9oft90OhpUbwWmbUG5mgqNfj8WD5ZS zVUqio6Ttq/1CNh3Iv88aCJFszvkglz86e/tdZsiJlV6rxiinrc7l27EEBh9Q75d2yUN BlSIKclhy5zw28ahXk9Wz+ixCtXbdDbLUoPGDTIn08vDoputWAOXNG7G28/GFsFBjE77 JCeQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZdYPlftaIV748oxQY25SHncCY+YksLTK9adxM8eWzpny1owV/v k97GnMdu3eVHakhHsx7HqFA= X-Google-Smtp-Source: AHgI3Ial85YIzvkwtwCCrJl2YQrBCf2oSHCkiYWwy2CwSZyeP2Ojqi5Nt0Qa0Gs42PRC53XtH36KFg== X-Received: by 2002:a9d:3476:: with SMTP id v109mr80573otb.7.1549969426470; Tue, 12 Feb 2019 03:03:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:75d0:: with SMTP id c16ls10653613otl.3.gmail; Tue, 12 Feb 2019 03:03:45 -0800 (PST) X-Received: by 2002:a05:6830:1212:: with SMTP id r18mr80650otp.0.1549969425776; Tue, 12 Feb 2019 03:03:45 -0800 (PST) Date: Tue, 12 Feb 2019 03:03:44 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <8ab48f34-edd7-4ed3-bc35-526bd8d10562@googlegroups.com> In-Reply-To: <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk> References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_446_1944064182.1549969425050" 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_446_1944064182.1549969425050 Content-Type: multipart/alternative; boundary="----=_Part_447_1990721462.1549969425050" ------=_Part_447_1990721462.1549969425050 Content-Type: text/plain; charset="UTF-8" Let's say that "objects" are untyped, and "elements" are typed, by definition. These are semantic entities. Nuprl's (closed) terms are untyped in that you are allowed to think of them as objects. You can also think of them as elements. This is not the same. I'd like to distance Nuprl, based on PERs, from set theory. In set theory, objects are given their final meaning by the universe, and sets are types only in the most boring possible sense that you gather up objects and call them elements. In Nuprl, terms obtain their computational meaning as objects, but their mathematical meaning as elements. Interpreted as PERs, Nuprl's types let you ask whether two objects implement the same element. Equality of elements is not equality of objects, and the way you think about objects and elements is different. A variable has a declared type, and it denotes an arbitrary element of that type. It is meaningless to think of it as an object (unless the declared type is a subtype of the type of objects). You are right that you don't need to explain elements in terms of objects. That doesn't necessarily make it a bad idea. Each PER indicates how its elements are implemented by objects. There's no requirement that an object will have a unique type. Each type can be thought of as an abstract view of certain objects. Constructions in Nuprl are heavily based on types, as in any strong type system. You wouldn't bother with a strong type system if you weren't going to do that. You can construct elements using the usual sorts of rules. Because Nuprl also has objects, you also have the option of constructing objects and then proving they implement elements of one or more types. If you've never felt at all constrained by a strong type system, great; you don't have to do that. But for many people, the intrinsically untyped approach is sometimes helpful. An element is an element; it doesn't matter whether it's an element by construction, or a verified object. I see this as a tremendous benefit for strongly typed programming. On Monday, February 11, 2019 at 1:17:25 PM UTC-5, Thorsten Altenkirch wrote: > > I have got something else against NuPRL. It explains Type Theory via > untyped objects which are then typed. In my view there is no reason why we > need to explain typed things via untyped objects. When we talk about > mathematical objects we think about typed entities, and the formalism of > type theory should reflect this. It is not that we find an untyped object > on the street and then try to find out which type it has. We are thinking > of a type first and then we construct an element. > > Thorsten > > -- 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_447_1990721462.1549969425050 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Let's say that "objects" are untyped, and &q= uot;elements" are typed, by definition. These are semantic entities. N= uprl's (closed) terms are untyped in that you are allowed to think of t= hem as objects. You can also think of them as elements. This is not the sam= e. I'd like to distance Nuprl, based on PERs, from set theory. In set t= heory, objects are given their final meaning by the universe, and sets are = types only in the most boring possible sense that you gather up objects and= call them elements. In Nuprl, terms obtain their computational meaning as = objects, but their mathematical meaning as elements. Interpreted as PERs, N= uprl's types let you ask whether two objects implement the same element= . Equality of elements is not equality of objects, and the way you think ab= out objects and elements is different. A variable has a declared type, and = it denotes an arbitrary element of that type. It is meaningless to think of= it as an object (unless the declared type is a subtype of the type of obje= cts).

You are right that you don't need to explain elements in t= erms of objects. That doesn't necessarily make it a bad idea.

Ea= ch PER indicates how its elements are implemented by objects. There's n= o requirement that an object will have a unique type. Each type can be thou= ght of as an abstract view of certain objects.

Constructions in Nupr= l are heavily based on types, as in any strong type system. You wouldn'= t bother with a strong type system if you weren't going to do that. You= can construct elements using the usual sorts of rules. Because Nuprl also = has objects, you also have the option of constructing objects and then prov= ing they implement elements of one or more types. If you've never felt = at all constrained by a strong type system, great; you don't have to do= that. But for many people, the intrinsically untyped approach is sometimes= helpful. An element is an element; it doesn't matter whether it's = an element by construction, or a verified object. I see this as a tremendou= s benefit for strongly typed programming.

On Monday, February 11, 20= 19 at 1:17:25 PM UTC-5, Thorsten Altenkirch wrote:
I have got something else against NuPRL. It explains Ty= pe Theory via untyped objects which are then typed. In =C2=A0my view there = is no reason why we need to explain typed things via untyped objects. When = we talk about mathematical objects we think about typed entities, and the f= ormalism of type theory should reflect this. It is not that we find an unty= ped object on the street and then try to find out which type it has. We are= thinking of a type first and then we construct an element.

Thorsten

--
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_447_1990721462.1549969425050-- ------=_Part_446_1944064182.1549969425050--