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-ed1-x53d.google.com (mail-ed1-x53d.google.com [IPv6:2a00:1450:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2f60fbd0 for ; Mon, 11 Feb 2019 18:17:25 +0000 (UTC) Received: by mail-ed1-x53d.google.com with SMTP id d9sf6036278edl.16 for ; Mon, 11 Feb 2019 10:17:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549909044; cv=pass; d=google.com; s=arc-20160816; b=EDn59M1LwzHG+HEqk/RqlLSfLx5OOqjoLqc9vgUUbdyPcj3k5P+RXr1cvPasWFVbSm 94AwcBKCw4t3NZICOId17EB96sEqdsBQDrVrzbCwgugTMt/4wfYUIoGFBQTFFBSKCKvS pVn+MQd3dXSYZ0Y+XT4KUAXttJncSm2/SkUTo0GjaqHpOAilj7JPGmurPcVTF5eHXq8g ak8O/THT6j6JKmiRQIKTl49+svhb0H+gz8XPJ9lbPoROjxrALcF1hiXk5/n4oFa4ghe9 JqOzcK0eySjazFxjJzkw385wh0W0pcBMEVfhjXt64BSoq6/szJXWY882EqmmYNO0Xb64 kxww== 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=A7QN20mShCAsrC1rp/o0FHIt121DWcAXf3NOb2Y2OrQ=; b=t8+aAgBUKEO9icQ61OD0d4J+fLCzh9hLosVGsHjc7gRX0ydP1opw2PlO78u6ih0CIf Xqwzzc7h4s/yjgLjOTILzP6dVSipVOL4qqTW8hiQt7KnF3n2A45TsvpCnAOOzrdzXu3o bsAg5ryBUoX32/FIkAqbTLDRH6Jw0oBBAeEbvMIU8W/6korLTcoBkT1VlDc8X3XN09+U CHRGsthX3yjvfph+O9stqZlvp604nqOceGA4w3Dy2EWxapepN1jNZxmZkmeAAI7d3Iev F+k+ym7CLOo56iWbTGcOAr3mK2FI2OJdQFspH2DfvHPqsISNtaMf4S4Pa5q/GdVcM+je lntQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 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=A7QN20mShCAsrC1rp/o0FHIt121DWcAXf3NOb2Y2OrQ=; b=jHYXeWNobw2bhTdiY81Ql/yP/wmz8F/2iOuUx0+KfJy7Z+jwz5JtRxGMmqXds1//Op I5mCn1G2t38mGDvccESqRd/Pwo4gNER1G2cJDGZL/yxa8DZeFzbn3xg9tW/u9Tn6RAr1 ms96d2eFT2NZ8HFfEl3bRE6AnPQKIJOA/m8HdLfBxYUAmCjbSPzwjBwUVf2z5/Cri0xx eldJ+nltiTiGsMEAcTUZTmL1VBhyiAMxDvifnEyRt+EEgOWRAlQSqsr0b06AyLi30GjD t49jN6BlWNbPGFtx9yhGEoJng4tKNKjGZIcjHZ5/VVztySPtVs/bIxFM9Bb6Gncqd5Kw rsvQ== 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=A7QN20mShCAsrC1rp/o0FHIt121DWcAXf3NOb2Y2OrQ=; b=lI6R5hfQJ9S+izeZgCm3CLcvcCS8WIg0nSZZESuxasW/psSzzV3vVc3phW/87HgtIW nPzz+ilyb+KYOXzeQ63+6ffuEjD2DWhiieK4R2KytzX0GJvcnJ1Ixx9xgAsVfY3doA/c JbpaROBASN8v/hw/AAvI3CkqUpZhOTEWMVzH3Le/HprDvozsZgugrfLiihVFNO1oaOTL joaQAUcVzLsXlYXbFRthNM+hv3wYkoofqilE+XCXYEXa8TD0ckRJPSKn0N2ADJGOMTt6 G8OHyq6GmE5owWoMJ4QJqGfBtjbyPtBvYHRSkMxWcZsPT7bjh0Q8FpYxBhX8gu5MMCP7 w7eg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubmcCHJ8x9kFFETsHgY+OK2J7olzBRf+rG4E2LMG50KI/PwX1xq j6DULmm+DvjcfMDvCNCIUnU= X-Google-Smtp-Source: AHgI3IYTp/3zJMK3k8t1KvkxOu2I0PC9KpuroBZ8ShDq1SBbHbR+qUjOq8apiln0I35HroHqM7xNnQ== X-Received: by 2002:a50:ea8b:: with SMTP id d11mr93258edo.7.1549909044831; Mon, 11 Feb 2019 10:17:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:d1d5:: with SMTP id bs21ls2782918ejb.9.gmail; Mon, 11 Feb 2019 10:17:24 -0800 (PST) X-Received: by 2002:a17:906:2346:: with SMTP id m6mr4225531eja.15.1549909044221; Mon, 11 Feb 2019 10:17:24 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549909044; cv=none; d=google.com; s=arc-20160816; b=c3vrQa0lVyFK0gzT+CUoaE+HnQ/zLJ34A7Jn0DvikK2hEhneV4OYdxK5F1Bz42EHR8 z8euv2bpF0tFQ8EMJTf+y94wSC23aeoQ3o0LnGoj1HN1EQdcaFvJhiJKvJAG1Y1jY/0v 5qFBMI9NKm+LrYoeGSZCHqkbcwDb5sJk6hzpNcPFK7XJZPN5Wg9EV6sw0bn3BhV4TRtI UFZT3U82Oyri9RNFGpFpDuuvwftN9rRDO9lcTC58qt+9kUs3CmmBbP7BUd5I2WbBG7qq JvcNGrf65H357y0NsD/5Uj+Fh52OSQycg49VNklAkD0XpzDLRbHnFxHpYcj1romX3hbq BhvQ== 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=nqErIZPRrCHB5LzsHDuMhXn6oauSczg28lmJv6Tr/8I=; b=tFLCQkxRFivLxTV6mnZLI1pRq60yELdA8OLI06NmpR0iv6Lp4wOEYr2zchasYIvJA/ ceRDppkuU/EeiMPG+DtfIJcO+vBwQV8aYiA0rRgDcwRwA+vibEgKiqSTTBEnoWh4fKkZ PPywfzhhBo0M6w7gpUurmJKWumyDW+7SMpKrIuC2QM6pZqQjAJ8VStjZfxwGIpT/cjO0 gOS8QXQDhwatKqXaPLTBBB9dWiVxuig8rkduY6HFn1TrGsd6/1Rj2zdoe9dHsW/rjhJo dlgEaL2f3EqCDw443ZtALH08P7IhxRKESOUaxWo0Z8PzEmYo3Zl3duz4HMxgKspAiIAv rISA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTP id l16si550023ejz.0.2019.02.11.10.17.24 for ; Mon, 11 Feb 2019 10:17:24 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id CADF26D10DE_C61BC33B for ; Mon, 11 Feb 2019 18:17:23 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 76807723512_C61BC33F for ; Mon, 11 Feb 2019 18:17:23 +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 1gtG8x-0005Z7-DT; Mon, 11 Feb 2019 18:17:23 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 18:17:23 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 18:17:23 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 18:17:23 +0000 Received: from EUR03-AM5-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 18:17:22 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4127.eurprd06.prod.outlook.com (20.176.6.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1601.17; Mon, 11 Feb 2019 18:17:21 +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 18:17:21 +0000 From: Thorsten Altenkirch To: Michael Shulman , Matt Oliveri CC: 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+4CAACMRgIAAJIMAgAAP4QA= Date: Mon, 11 Feb 2019 18:17:21 +0000 Message-ID: <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> In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.a.0.180210 x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB4127;6:W7To64MSDJLp19WrGD/g9puZN0tDls1YXI/o/THac0nlrdLPcvs3UIqj4b8Bd1xEzkaN4HvQn63B0jZKbucUUCXgefkYRQd7V/igRYUJuw0wu6MINXdX7CNyWOvadnxiNLzscLfOCSLkIHs/JfFdjekoTQmjNZ5/jUkUwnRZWBxBjoFMefmcTt4Hx+5b28PzSRvh9olVq2aHeYx5aJZweCLZZyuf4/SMcrVTiOzY14UCB0/LlFuks2xBa5FeNrbk+mOrc4WqEOEcxNZa0BG2uQJMu6zjUcvVm4IhCBQcOQF89nKE4BsmK5R29ZIFG5LVFg+NHqVaZrMFD3jYPh+6C7LTEmFJT+qPdtF1LKOtOIJmCx5e7Rx7sJXSFZJXL8bpf7zjkQMz30j8NnDPGyut9iOY+gNhopS31idAs+BsQHpvlXka2AoHl2dyA+um10wL56w1/5JAgi0DVWQkHY53tQ==;5:xLHSLCrRDwRIaoUTXQFMeXqiZRWDUmbG3AsYT2jzZSdtVGpLyWtwT34JtogBe/deYZdOLwKsstNTCTkPYkDqWLzQc6w16Nao0tbioem/SmyoC75aRSR053vJG4fnqRCgZg57IITRnX1JB/A+/QlkMf7kq/4BdosBqhY/1YQoLnHYBtSz4istPq2TOTtzMTaqmb6q+6UpvzskDb4C2Pgd7A==;7:oYWIWim2N8zUiO4KgXUMENuEvp/rOKfvicwk1aYIsKIqHiO805c0gPBmG9l13qTOvBFH27GuXfESOFb9NK5/vSw5bcSj0FUsHzNS4EjvEq+dwqpPtPNWu4zDv9rLnzE97j2V3nVJaJR11ePN9rC5mQ== x-ms-office365-filtering-correlation-id: d0c24e3c-e5dd-4da4-61d7-08d6904d2a14 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605077)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB4127; x-ms-traffictypediagnostic: VI1PR06MB4127: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-forefront-prvs: 0945B0CC72 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(346002)(39860400002)(396003)(366004)(136003)(189003)(199004)(14444005)(74482002)(3846002)(6116002)(76176011)(256004)(186003)(99286004)(2906002)(97736004)(82746002)(2616005)(26005)(476003)(446003)(33656002)(11346002)(486006)(561944003)(106356001)(105586002)(93886005)(478600001)(4326008)(14454004)(86362001)(102836004)(8936002)(71200400001)(83716004)(25786009)(966005)(53936002)(71190400001)(229853002)(6486002)(7736002)(81166006)(6436002)(2171002)(305945005)(6246003)(81156014)(53546011)(6506007)(316002)(786003)(110136005)(6306002)(58126008)(6512007)(68736007)(8676002)(66066001)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4127;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: DOHiw3k0/u9rfodE8S7wVu1qjAI5UmKm4MKRfhnAga+N0WDLIyyr/QVw2VCUwFm+hbnjoWmiKxAp0HNQxXkupLqltow8w4ILQH95jIQGWX2oSPyrapq/l9pwswxHJM8BwxcLI/Kzl03e+KWyJ575sN+ip8B/BhcShF1xp8PkmEFS5oVY517AeX0nE4a5X1SU4biUYLfnL+mXwoK5UIMjLRpqRu+4+G1YT4LZYUcTUfJFi54xe6OYej6gTeivuwPMPPkD4xAmE3tdD8/z9JQwKg/Sgr4DdYbBUhscFqVW3LfcGzdTzvIZ+8RrAMWiDvG25QnuR7FP1MUaMiCaJFQ2u51T57crU/kYRMV7Q6hyCsjQP3rsqk9neTirvtzONfS9uvyvPRN4L9yFL5k3SQkfjfTSfMixdf9AEPk+g9d47KY= Content-Type: text/plain; charset="UTF-8" Content-ID: <3A9AD68FCAB04C42817F8F60E7172559@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: d0c24e3c-e5dd-4da4-61d7-08d6904d2a14 X-MS-Exchange-CrossTenant-originalarrivaltime: 11 Feb 2019 18:17:21.0653 (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: VI1PR06MB4127 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.128 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 have got something else against NuPRL. It explains Type Theory via untype= d 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 mathematica= l objects we think about typed entities, and the formalism of type theory s= hould 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 =EF=BB=BFOn 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on beha= lf of 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 =20 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. =20 =20 On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri wrote: > > It looks like Jon is with you regarding definitional/substitutive equ= ality, since he considers Nuprl's subtitutive equality to be alpha conversi= on. From the old discussion about it, I had figured Nuprl's substitutive eq= uality 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 And= romeda than Nuprl. It has a difference between definitional equality (in Jo= n'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 refe= rence. 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 equalit= y 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 par= agraph. > > On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wro= te: >> >> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri wrot= e: >> > 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). >> > >> > 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 t= he >> 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 i= t >> 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 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.