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,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x23d.google.com (mail-lj1-x23d.google.com [IPv6:2a00:1450:4864:20::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3d6f244d for ; Tue, 12 Feb 2019 15:36:09 +0000 (UTC) Received: by mail-lj1-x23d.google.com with SMTP id f22-v6sf927639lja.7 for ; Tue, 12 Feb 2019 07:36:09 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549985767; cv=pass; d=google.com; s=arc-20160816; b=OeIbPYPSWgXHOpTzH5DEzYOSp6XhKKM6vRuW0JEI6O7JSQ1bnZ2KOFiGFtYWpX6mj+ zFfC/RiDoDXqMbNseMoRrJl/AtY70qUCYGL1YwjC8S+T9K+7eekeQ7XWDLxV81V1Aeno xBywRjz+nRdzgY3+uRgz/yEaG6wLf91YW1Ub9azvY95gtsy6Exgn+bb1uEKG4LaCBaEh wkBB3nDHBXMYuEO3Lg4Wjyz4RVwxZEMFnIMl6fpbeq2Ce5/I8UY969++/NsfmhaLOwG/ K0MCNbo/7sy1wH+XAM5FE+W2ic0OuLRSPgE8K2sGyhoHaiY3fKs2junfZ9F/+rFZCiro JBeQ== 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:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=Q68fZNib2JmDnUmS7LAOZVbbCUTlYVZ6X4Fqtmv2sos=; b=M/Xk8PocCmHtSJjfD4ZoRZp8ERLT9I1wMqaawWWwYahNwQc9auyso9EYSF3cYMmHyw 44S/p5JP8d2Bja/+6d79hA9a9JJWeyFXY9r7VRcy0nr/fji9lFW/racnhmRqJuG8M7p5 RdtiwjbQL/ZO2cqx7UpCygBhyTeG2Yk0tl8lKXciPXYZycWuQxTZKSRywleKDLW326aa VGCq/xHVtFNNDjJXxSl4jPtKS88CxMk5hKKFI5qbcYxruwruWGymkIOsFNZSXTgSBsGm 3tehKTbOI3I3Er2jmGrDa6BxTJ0LuqkPD+UucViSSSvcqD+t8OCWTL/AM5vO/rjJEjj+ dcmg== 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:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Q68fZNib2JmDnUmS7LAOZVbbCUTlYVZ6X4Fqtmv2sos=; b=g2oHeDsDA86RGDr+xZPXll309QZWPWt0CVoXlIcJpZfFLdShT3sJFED/qSPsAvxWMU sJX2xESHtZsEJJ+HqVcvlpTdPT5V7rqcEswIyquoPxBOJ+WyzOHysTEePHuQmYBxlhDA WqTXg4etlsDZJpzRR0ktM0mZsRG7poVMPLlW/4v8bsOgTRE3xc5uB5XDL/QCTlyNfk8p V7rlmdymvBsRmkEyz7+v+ggB28nIjMEKySMhMIWO0C/XlDfUMWOQ1SjlwqpByR1X03OJ AAq5M3qPKGu96uLnKnw4bIFuUe90PsglOzYPZLpMOu9w+YS3bO9O2bI+WGMlDxTPSGRk Iy/g== 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:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent: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=Q68fZNib2JmDnUmS7LAOZVbbCUTlYVZ6X4Fqtmv2sos=; b=T4UCdWtX9Kdp8KTqpnGu6UiffbZGxnNHv0hrMz4kUvEAPRYum6R8z60c480WgSzndY CAqmOKJtf2b/v9eeK3XZoc4CR/kC3RisFu2Ufx35CgnVslyWbfJnufS+6FGAh51d2cYI rq9O166BGZPLVpk7YKmNk0AfmwDX4f7Q0mYNlHBls9sQ0yyL+fLfFZlZZdo36MQyNpvY GSvmv6kpbtORxnl7BveX3hxPcqXGvLtbrMuqahb5VB6qcXt3d68bz77VIYV/7vCj3nUd VcDanBKsq7694ndS1IhzNsyDlkTa5+svRe2ptqQ9H9rYvnJ+tGd5I8g7C/UDSUPMvloH 6S2g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub+KCNQdr6WUlUPWBu1ScEpeK18dyU+uzvbpzBBEJk8QEC2pIpg xsWdobygfC80qu3oOMyoW1k= X-Google-Smtp-Source: AHgI3IYNmzYuAlrhoXTHusHfPuHgOTcWRJTgfuq9gHhbQpr8rQpkOeitRs56ci3prV8a5i0aUbyYWw== X-Received: by 2002:a2e:91d2:: with SMTP id u18-v6mr23296ljg.2.1549985767615; Tue, 12 Feb 2019 07:36:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:520f:: with SMTP id m15ls1631576lfb.5.gmail; Tue, 12 Feb 2019 07:36:06 -0800 (PST) X-Received: by 2002:a19:d454:: with SMTP id l81mr320177lfg.12.1549985766098; Tue, 12 Feb 2019 07:36:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549985766; cv=none; d=google.com; s=arc-20160816; b=CY9p7L4+L2VvkNWKbZiM7VGllawyD/rD1yUIwtgocnDeLc4Inekw8eommyUHdJKQ/p xrtHv3UhwbdAAQN8b0IkFqI0fXvnGhtJE2so2jdMNNR7Rs3hKJyhySk6vFxx675cKJh3 +nXe+Rub5QQqG7VprPJkCGFLdLAQ1Kg0xuSdL9Oh8A+ZTKPEmTi0y3eMcLFqkW9JVjrr Vuq+nKFxN/U0Gkr/CJM/0ZOxAo5MLCnAipGuFbkgC1zU476jtH58Ebmg4sLjjX4Q3rGg Qr8vvZxaMDaZj9r0vZnj+j9laHWqn63Uv9yt8dX7fIJ5bMffx+LJwjP/bhq4DlQ3AQwO ugpw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from; bh=NQfCdKvzoRMoPsL4c0qBfQKT/NfI8ezFNMq0WrB+kao=; b=xOOo9QiNRazH8nCb3TnkiUOz7lIhD+dlA6LHklp2o12CdFH+qGeGkqlaqvLvnlAGb1 XKRKjKe+mIVvJ3YZ/09PZYMs1zB7N0ccd9dG28Ci808ZCmtItHXeZX5l5EVaBEysE9Qx 5puwABfQwBLpSFHgxFURDLLI3lNtUCmicbDdqgiPeDpQceXxCOYWW6cdC0WOLwqvsRS/ sk4JWQ5gFZARcV6+1JXEnltWO5bmMJpN+Ol+AcklNhq6hPoa40UwuV1nw9Ok5e8ZfYMW 2omlAJGD5/5d6Bqh9xAcVHCylLqqHcv3tvI3INgKyspU3napPYB44ZJu3xBvEgcKqoqV ySoQ== 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 h17-v6si819395ljj.0.2019.02.12.07.36.05 for ; Tue, 12 Feb 2019 07:36:05 -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 59BFF6D0F6E_C62E7E5B for ; Tue, 12 Feb 2019 15:36:05 +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 11F506CC944_C62E7E5F for ; Tue, 12 Feb 2019 15:36:05 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gta6P-0003JL-1J; Tue, 12 Feb 2019 15:36:05 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Tue, 12 Feb 2019 15:36:04 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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; Tue, 12 Feb 2019 15:36:04 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) 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; Tue, 12 Feb 2019 15:36:04 +0000 Received: from EUR03-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Tue, 12 Feb 2019 15:36:04 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4288.eurprd06.prod.outlook.com (20.177.56.74) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1601.17; Tue, 12 Feb 2019 15:36:03 +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; Tue, 12 Feb 2019 15:36:03 +0000 From: Thorsten Altenkirch To: 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+4CAACMRgIAAJIMAgAAP4QCAARkvAIAATBIA Date: Tue, 12 Feb 2019 15:36:03 +0000 Message-ID: <6C0820F2-A1E7-412B-A008-51FCF62BA257@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> <8ab48f34-edd7-4ed3-bc35-526bd8d10562@googlegroups.com> In-Reply-To: <8ab48f34-edd7-4ed3-bc35-526bd8d10562@googlegroups.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: [128.243.2.16] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB4288;6:7UTCNFbpLanQNohtW1EcJfFqC9svAPQG+cygALSF4XrGdeqhygr3YU07TJ3Xps0gttXUxf0c3dOJw73D7O++MAlTrLtsWVMA9htfqcwjeuxIQid97O4evfZ1LiQ/bsmroSvn3G7K2SIG4AIEbqP5ecKCSFGy1sJMUGd+eEt2g68nArySG0Z5QMamysNUimLrCawHfyYEjIWy/2fpXFkA3Uri0gigsGDhvXgKABeN87L9pPjaaHreM5P0+PusKyq5lzDjBmuQzy28BSWEUswZWvrIjtQLyKIlREAcOu0DsAXSYNabtSwcj31G9mZN31kpeCLju589QG7nZ0vO4nXnBJ/qfZqFxeBR45A5G0mu13SNzlYGNtDXcZ+tn03e5lgIrIVKvVsML/IgYJbZQH97xcjfIGIBlsE2FcyzhQTeLH69bNKU8l58nsk6js4M6bSKLA8uPsLGKNQ1TIXJjZrtIA==;5:12TyrZFgsl0L+KEQxR32ha4M1s9EnYFO5X8Bo47MaigcX1nx6jCOy1zE4tdW+pKmrWorm50MfzqgXfWaBLGS/Ovp+CMXvlRH52SibG1qE2gBByUeMMT3853smPCo4Jxr9+qq9pEPOmd4yF3xLiSFNi44q2tt7Un3hmTl59Se6dmGpg2GADdM1f2dqHgvPBFnFDXYV5Z2yuPypoiQ5J4AaA==;7:WKKyKvvNQPTLcgw5u/LoOwXmeoL7+33FTBpYKux7iDuBR+Nck1ti1KwPhHk/Dh6NQ6haw0T4MJ1me5mhZJnkbD7s8abrV/b2FvZ6D0EwtxQgLvX915TaQpOrfg9DXRse9k4Jr8omNKkRkhbIaKyKVg== x-ms-office365-filtering-correlation-id: 543a7c8f-b69a-484c-8406-08d690ffcbfe x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605077)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB4288; x-ms-traffictypediagnostic: VI1PR06MB4288: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-forefront-prvs: 0946DC87A1 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(346002)(39860400002)(396003)(366004)(136003)(189003)(199004)(97736004)(54896002)(256004)(82746002)(105586002)(106356001)(6306002)(2906002)(68736007)(6116002)(606006)(36756003)(3846002)(229853002)(33656002)(6436002)(9686003)(6512007)(236005)(6486002)(83716004)(71190400001)(71200400001)(966005)(14454004)(25786009)(58126008)(110136005)(316002)(786003)(93886005)(74482002)(11346002)(86362001)(186003)(53936002)(6246003)(446003)(478600001)(476003)(486006)(66066001)(81156014)(8936002)(102836004)(99286004)(6506007)(26005)(76176011)(7736002)(8676002)(81166006)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4288;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: ulf0Y8/EITY7rzn/pd/HBkuTfgaqyMPw7Y6I98WldiFMNeOdCYf4B7+5z+gKRqsWMwlDZFJAnnC/l+ojlvds0O3+WP9auANjjMnmfZZYQrSYmLw3NbJf9VOXueO4v2d4v4p8r2yx4qKUYrOia3WPY6pyqKIHX8rE4mxitsX534/TiK0HD4W64u9a55vwCSh1ALpV5NiEQNKIDpav3goaQzM1BR0cNRdei3q4Yr2toxIAaY89j72CWEBoOmDU1EL4c6AsPAtKC4MC+dpZ4jI6R1QCzmNw6KVT//hH7fzognbQujVB6iP7k+KSRuHK84FmcwFEhiCKZIdpylPgt5zTH8q90IDwKLFqgDv4GqRQ3SeIdoXhOLK8RnZV+DWt9/VujUippSo+q/Vtamp6LY4n0wK/eziA7a0BrB86LNhEzbc= Content-Type: multipart/alternative; boundary="_000_6C0820F2A1E7412BA00851FCF62BA257nottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 543a7c8f-b69a-484c-8406-08d690ffcbfe X-MS-Exchange-CrossTenant-originalarrivaltime: 12 Feb 2019 15:36:03.2578 (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: VI1PR06MB4288 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: , --_000_6C0820F2A1E7412BA00851FCF62BA257nottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable You are right that you don't need to explain elements in terms of objects. = That doesn't necessarily make it a bad idea. Not necessarily but I think it is a bad idea. Why do I need to understand o= bjects to understand elements? Why do I have to capture all possible constr= uctions if I just want to talk about some specific ones? This is something that irritates me about set theory: if I want to say for = all natural numbers =E2=80=A6, I am actually saying for all sets which turn= out to be natural numbers=E2=80=A6 At least conceptually this is rubbish. = Who thinks like this? Yes and in computer science we think about types sorting untyped programs. = But why? Why do I need to think about untyped programs to understand typed = ones. Untyped programs are just weird. Do you understand the untyped lambda= calculus? It=E2=80=99s syntax is simple but its meaning is a headfuck. It = took Dana Scott a while to come up with a mathematical semantics. I think we should put our mouth where our heart is. Typed objects are easie= r to understand, they make sense by themselves so lets refer to them. Yes w= e implement them based in intyped things, trees, strings, bit sequences but= we don=E2=80=99t need low level concepts to understand high level concepts= !! Yes we need them to implement them but this is another issue. 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. 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. --_000_6C0820F2A1E7412BA00851FCF62BA257nottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable


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

Not necessarily but I think it is a bad idea. Why do= I need to understand objects to understand elements? Why do I have to capt= ure all possible constructions if I just want to talk about some specific o= nes?

 

This is something that irritates me about set theory= : if I want to say for all natural numbers =E2=80=A6, I am actually saying = for all sets which turn out to be natural numbers=E2=80=A6 At least concept= ually this is rubbish. Who thinks like this?

 

Yes and in computer science we think about types sor= ting untyped programs. But why? Why do I need to think about untyped progra= ms to understand typed ones. Untyped programs are just weird. Do you unders= tand the untyped lambda calculus? It=E2=80=99s syntax is simple but its meaning is a headfuck. It took Dana = Scott a while to come up with a mathematical semantics.

 

I think we should put our mouth where our heart is. = Typed objects are easier to understand, they make sense by themselves so le= ts refer to them. Yes we implement them based in intyped things, trees, str= ings, bit sequences but we don=E2=80=99t need low level concepts to understand high level concepts!! Yes we need them to= implement them but this is another issue.

 

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 Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.


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.

--
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.
--_000_6C0820F2A1E7412BA00851FCF62BA257nottinghamacuk_--