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-wr1-x43a.google.com (mail-wr1-x43a.google.com [IPv6:2a00:1450:4864:20::43a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 899d02f3 for ; Mon, 11 Feb 2019 22:58:45 +0000 (UTC) Received: by mail-wr1-x43a.google.com with SMTP id v8sf203235wrt.18 for ; Mon, 11 Feb 2019 14:58:45 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549925925; cv=pass; d=google.com; s=arc-20160816; b=Hb7jD9a0PZtsBZRGEf3m49PV7eMBWijZ6DMNNFtk9EJALxpb6rJN0pac2Be3M6bbLA ZWRPjmErZBgKbGrPk6IeuPcorUoGjB9OgftUcpsZCLhUwYPjWOfL6XHfxU2c+vS4DOxl HKKpT5uf+iNLpjmc2WOSu0FOB7LxjJBSO03P81tGfdwA0cDTqkQLLZ9hE+zGtvuRwzgT I40bPocoSeGKsBqwEA0mNV1lfY/4nYD0AKGntcBmWLaKxA5XT76RqeVNAuLFv/x7PGPy LewOp+A/X8lFbyKeoL9pILKDFNe/y67KHjMrFJe6+9lI6IksXt8oRKxEqobaduG6hV4K Jt4A== 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:mime-version:content-transfer-encoding :content-id:user-agent:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:sender:dkim-signature; bh=vHQ/oz5MXWVrzFJIJuRDe7LS/7Gyf5tbtQKoQtw1UMo=; b=Rk8VI0B/GH6mLYfzgk9jvOKkn/6YJSF0r23+qUcppRxgC7Hlm0Vn5KVkRIBP4C6plT 1wR10ffQDAqNNrgVrLHtS3+E55ziKZEmT1NJJHlx35bGQAOqrj6Z+7KvXrP7hUksH8oY ckSBtvXdyeBt78U78fP2MxKuZfWsQiPCAvy4kdMTtnt7szMJdtOcSvHa2R++eGlZDtNw T4bkSg52PWm4uU2CCEgdn2gTEfsNnaXVCXbShC8LTgdE5935neqI2Ltk0da9g2qJnsVl tpa4STA9cH2BYUeHsRyN9YCh6e3r//4EWnbO+ivk92p1vSnstlBRicEc2APU9XFKbF+B A8Jw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id:content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=vHQ/oz5MXWVrzFJIJuRDe7LS/7Gyf5tbtQKoQtw1UMo=; b=cxe6knIcip1PkJKNSlxZc+YTn9eUL7B1sMet2wsEZbYdFdQsRRYDWLe02qsKCITgGO /5/Nt0rTb3qHYp3/Kt4gVmrwA9nDORlx+ayg2MudEpegjXmZHkGXqJFNwgMo6ravvDFn 0LY2+sJlwM/VppJUOvXNckPzszBDyJTImkVHijUm2aM+2js2gXqzaOMCiH2JdeGDlwp5 DuSJGqQBee9Wj8dNgSQfqeVHIDaxZQRqHOAr8I7xXmIvRgJkD6QnRcSkri2xEkjnerBY r8wp0DOIAU13jQemsCjUtXvXPklSZKFUkjUUUBCmQsWOSuY6q5lYDr76q6YkyHNaYlsW BfCw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id:content-transfer-encoding :mime-version: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=vHQ/oz5MXWVrzFJIJuRDe7LS/7Gyf5tbtQKoQtw1UMo=; b=nq7T0rNpKvuF0VY1UedRy0AxfJkSyv+n4ttC8QnnU2gfIVgblyKclNLnbQXYNzmDy3 bCQft4p+l0mRUfplXnoMnmX7iqD6L/cvfBmXiQiDzGCrYJxv7hnrMkAjw773WZ7V33bD to0ZSfXtzTjegefL73CFlnPHom4CsCuzUFlmoxunlLAteznIDCJ/ZZobniK0zAuejXHh jb3HLmeEAQPZcZaYxDBI6SJDdQ66dMw7/9j9CE18xl9SdKM2GSBixWEROC2nicjTH6zb mpQ4AsN4dU0NHLBMOUSywgB6TLHWZLd/RoIHnYWm8nPNa+2vqBIu5BXmf3BkP9RvJFFX F7mA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubm6p9LR1D0wdsSHVAK3oqGAR7xhbahVWCEvoTrLWAg5mG1Uwpv uBySi3/ZWoEq3ZPpd0Kr+Zs= X-Google-Smtp-Source: AHgI3IYJ/lQzX8VNRxE2kfqm1c5jx5bKvdYxLITLDLYcOXLBHq8fwKQfUyVcoasCWXuuyD6vXcYvZA== X-Received: by 2002:a1c:7715:: with SMTP id t21mr5132wmi.1.1549925924910; Mon, 11 Feb 2019 14:58:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:8241:: with SMTP id 59ls353040wrb.5.gmail; Mon, 11 Feb 2019 14:58:44 -0800 (PST) X-Received: by 2002:adf:f5c8:: with SMTP id k8mr27196wrp.26.1549925924329; Mon, 11 Feb 2019 14:58:44 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549925924; cv=none; d=google.com; s=arc-20160816; b=WTMCNoEzQjSKedpf2G45uRdNO8sLGzDk3CwQaOjr/hRQu2jdmpR7Oq9jMt7jw/f0MB 9qX3qGCsPaebW+Z4y3uKGI1P7m9YxpVnysNowIgjZ7WBXnGNS33pSy+VNUAZ6Sbl5wxf h90IG6vzaLx7LlRw/CDS0TXjC+D9SlE4b6P1ey4J9Qq9F2fIiZRU+TzYZSUR66zL41+3 n6X5LnZuhFJqkLObhgwHgzLIPe3GOE1viiWH2gEXQRPjCv5SHOEWguzLPZcUTuZK0MMS +WOxiEW5jteDwMymY5LpBu4K3GPObG/ps/Z/oMPiJzPudTkE/22rUkuY7TkeqzvS/JK+ YDQg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=YF++OAeUaWIah6spVnpa1vN9ITH4hQo8qIXPrWM61qU=; b=G9xkf79PJS1h7ADk6CaWuOSAFYlvBnkQv+8qaU/J5RJe9a4S5ZTLbDTZnUKmVPIN2X eIfvtdthntq76J/0bwaasLExRcUZDyt7RBsyXvK4pbmbc+pG0ZRLN/ANpatI+zt8o8ED w1YsS2PQVrrF5YziuA+uobfK+7e2JI+ELCd9Q/gvcNHWdC5gltepi/M8z0TMW7XFlQjY EhUsA047FG6l3oL6r1ILFZI2OqKqwqkEPDZhOoOKKZdLe//ePN820WxW+l4UThkrjVKV j0l7eB/TFMEul6Esyk8t6JJpur8P7VAMbO39h8ybPmlwZOJ9SLyo5Sf/ppHGBptFGuOj zjXg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTP id t23si53657wmt.1.2019.02.11.14.58.44 for ; Mon, 11 Feb 2019 14:58:44 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id EAED52B7C5C_C61FE23B for ; Mon, 11 Feb 2019 22:58:43 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 79485366E92_C61FE23F for ; Mon, 11 Feb 2019 22:58:43 +0000 (GMT) Received: from [10.159.172.14] (helo=UiWexEDG02.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gtKXD-0003l6-EJ; Mon, 11 Feb 2019 22:58:43 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 11 Feb 2019 22:58:43 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Mon, 11 Feb 2019 22:58:43 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Mon, 11 Feb 2019 22:58:43 +0000 Received: from EUR04-VI1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 11 Feb 2019 22:58:42 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5342.eurprd06.prod.outlook.com (20.178.14.29) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1601.22; Mon, 11 Feb 2019 22:58:41 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::85b3:de9c:4991:b687]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::85b3:de9c:4991:b687%2]) with mapi id 15.20.1601.023; Mon, 11 Feb 2019 22:58:41 +0000 From: Thorsten Altenkirch To: Alexander Kurz CC: Michael Shulman , Matt Oliveri , Homotopy Type Theory Subject: Re: [HoTT] Re: Why do we need judgmental equality? Thread-Topic: [HoTT] Re: Why do we need judgmental equality? Thread-Index: AQHUwG4TVtwCLIAFnUCh+hNwix/S8qXXgAUAgAALFICAAGGlAIACmgOAgAAM+4CAACMRgIAAJIMAgAAP4QCAAAfTAIAARsaA Date: Mon, 11 Feb 2019 22:58:40 +0000 Message-ID: <5643E581-EE54-4CFE-BF75-A3AC274ABA16@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> <6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com> In-Reply-To: <6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.15.0.190117 x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB5342;6:R0GfTAJc4V46HdYVWhzThc82yWazLZFlgcmtQtgw6dwGMPu6mkCwF6X0zh1ICuMf2kp1zYFeKXFu1cIgw0pmIiwLQFaNGvDc3u8mU/tUMOUlcYUelh3lAZnXh3CSvacHxtbxbrd6cdmMwnFR7gd7xKARwbV81etG59z65gTvYpudk1/l+YpHUZZMmYwwStN1phaSJ9HxROb01q7QHASLk+5tshN7CGWkdtisGInSqm78axS6tH6wQENBf4ilBFSSIAcoei1IkBj88AgXgixEzF148rO0tNIMdbDRqeT6DyynKR5PJUl+VcoTQT0NXnBvn9vLPi2zdT41fV1IokiDlWqTJV+aZvoAS9ZpaJxlHvTLD0I7bDbtoZBSK8us/WlS27IJ1y/qjTH34e5D5B1O4U5Hpcn1ev4sM5fXT/RPukMv8Uxb/NsSupcLmyekq6NwgzjC5NQqbQTfhR/vjy8GnQ==;5:ciMw8nQlYZSwKyA3qSgKG3jdLIHlIPjoSlUD6AhrqpNe0f99ZHC5YWrnvVU6ynnFoDNEHJ5vhpOV6Zs3He6SU8bQLKjVxyE/kFqcgIrFNOWxJDCk/gOeyGy5ZZ13KIF1O71TrWq96PRYzIB1h2AItw3f/Hkbrz/Q2YwzKnT61PKZoA7keN6Yf0V9KNS2mN/yX85HhAMeegyHYr9tTc+scw==;7:pCjdU/7vUbtLdWG/tB9w9Af1rLsUgrF9YXayK0H8sh4tRNo1ZmLuMkMQD5F3LLSN1opSirvc6iiKrqao7lfswk3oW8aihqd5pZts1yUTV+iu5rWmehuiE6Odvg29ih0lf8DGhrIGUwy13hB3we87Ow== x-ms-office365-filtering-correlation-id: a2441018-8e6c-4de7-12f1-08d690747746 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605077)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB5342; x-ms-traffictypediagnostic: VI1PR06MB5342: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-forefront-prvs: 0945B0CC72 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(376002)(346002)(39860400002)(136003)(396003)(189003)(199004)(26005)(81166006)(2906002)(58126008)(54906003)(186003)(229853002)(97736004)(25786009)(305945005)(66066001)(6916009)(4326008)(86362001)(8936002)(1411001)(486006)(6486002)(93886005)(786003)(71190400001)(71200400001)(83716004)(81156014)(7736002)(76176011)(316002)(14444005)(446003)(36756003)(6512007)(476003)(74482002)(256004)(6246003)(68736007)(9686003)(99286004)(561944003)(11346002)(5024004)(966005)(55236004)(14454004)(6116002)(33656002)(102836004)(105586002)(53546011)(6506007)(106356001)(478600001)(6306002)(3846002)(8676002)(53936002)(6436002)(82746002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5342;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: w4y3lB50+HhLlIW61PD4iEO9oNpkZsfibSkav9vHQdNBg6HFWPkja6Vv+gsXjAckYFSQh9WHFF7aeCBeSXgoL1GA6O+4zf9cFj4nmX9W5vxnvtoQcFOVmhC3FPvLsyeMtkHIJBZwtq1bb1qPeERLesCkQvSv04EQzP/BCerA+EtterOnFL7XAW9L/IF8iD1c6AhJp/FBeun1YOtKana0JK0TngmvuZp9tbQ2TmCe74bY/pfX9q5z/w4ICSpVcxgeXk+A5WSUVojurYPYcJDcZTg0FYt0BOXAnAB4GuUksfK+jI9vtYHRMu09RCbGGFVyd7j3YvXdVShQWzX1qNE/v9hp91LQhZ6DXFmsTed4Hq2CDVDlkc/pD/vYEwQl3MrOVu0Jn5q033AydSsUaarA5kU93ABXepCZgBdJXgqEO9w= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: a2441018-8e6c-4de7-12f1-08d690747746 X-MS-Exchange-CrossTenant-originalarrivaltime: 11 Feb 2019 22:58:40.9449 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5342 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk 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: , I think it is rather misleading to think that 0 and the empty set have some= thing in common because in set theory they are represented by the same cons= truction {}. This is rather an accident of representation, it is like sayin= g that the number 49 and the letter 'a' have something in common because th= ey are both represented by the same bit sequence. Indeed, I think having access and being able to talk about the accidental r= epresentation of objects as you can do in set theory is detrimental because= it stops abstraction and this is precisely one of the main advantages of t= ype theory. Thorsten =EF=BB=BFOn 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on beha= lf of Alexander Kurz" wrote: Hi Thorsten, =20 "When we talk about mathematical objects we think about typed entities" =20 I agree, but does it follow that types and not objects come first? =20 For example, 0 can simultaneously be the empty set, a natural number, a= n integer, a boolean, etc etc =20 The importance of the "etc etc" is that this list is not fixed in advan= ce. It can change during mathematical course. =20 This seems to indicate to me that objects come first and types later. =20 Another example happens when I say that the dual category has the same = objects and arrows with domain and codomain reversed. The same object then = belongs to different categories.=20 =20 Do you think that type theory provides enough flexibility to model this= aspect of mathematical discourse conveniently? =20 All the best, =20 Alexander =20 > On 11 Feb 2019, at 10:17, Thorsten Altenkirch wrote: >=20 > 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 mathe= matical objects we think about typed entities, and the formalism of type th= eory should reflect this. It is not that we find an untyped object on the s= treet and then try to find out which type it has. We are thinking of a type= first and then we construct an element. >=20 > Thorsten >=20 > On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf = of Michael Shulman" wrote: >=20 > FWIW, I think the only thing I have against NuPRL "in principle" i= s > 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 id= ea", > 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. (-:O >=20 > Can you explain the difference between "definitional" (whatever th= at > 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. >=20 >=20 > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri w= rote: >>=20 >> It looks like Jon is with you regarding definitional/substitutive eq= uality, since he considers Nuprl's subtitutive equality to be alpha convers= ion. From the old discussion about it, I had figured Nuprl's substitutive e= quality was the equality type. I guess I'll avoid that term. >>=20 >> So I'll ask a more concrete question. You seem to be more open to An= dromeda than Nuprl. It has a difference between definitional equality (in J= on'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 ref= erence. Which is equality of sense? >>=20 >> Regarding the paragraph I said was vague, my complaint really is tha= t I don't know what you're getting at. I recommended strict or exact equali= ty as possible (informal) interpretations. This doesn't mean there needs to= be something called "strict equality" in the system definition, for exampl= e, 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 pa= ragraph. >>=20 >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wr= ote: >>>=20 >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri wro= te: >>>> As a form of extensional type theory without any "built-in" implem= entation 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 cou= ldn't come up with one, it just isn't specified. So I don't think HTS has a= ny "definitional equality", in Jon's sense. But it seems like HTS' exact eq= uality was considered substitutive nonetheless. In fact, it seems to me lik= e what Vladimir meant by "substitutional" was that it doesn't cause coercio= ns. Either because it's definitional, or because it's subsumptive (my term,= from another message in this thread). >>>>=20 >>>> So I think you're misusing those terms. >>>=20 >>> 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". 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". >>>=20 >>>> You seem to be downplaying the differences between these notions. = Why? >>>=20 >>> Maybe things are different in computer science, but in mathematics = it >>> often happens that there are things called "ideas" that are, in fac= t, >>> vaguer than anything that can be written down precisely, and can be >>> realized precisely by a variety of different formal definitions wit= h >>> 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 ou= r >>> 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. >>=20 >> -- >> You received this message because you are subscribed to the Google G= roups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, se= nd an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 > --=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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. >=20 >=20 >=20 >=20 >=20 > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment.=20 >=20 > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored=20 > where permitted by law. >=20 >=20 >=20 >=20 > --=20 > You received this message because you are subscribed to the Google Gr= oups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, sen= d an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. =20 --=20 You received this message because you are subscribed to the Google Grou= ps "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 This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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.