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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x33a.google.com (mail-wm1-x33a.google.com [IPv6:2a00:1450:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 75f0a7cc for ; Wed, 5 Jun 2019 17:11:50 +0000 (UTC) Received: by mail-wm1-x33a.google.com with SMTP id t62sf20664wmt.1 for ; Wed, 05 Jun 2019 10:11:50 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559754709; cv=pass; d=google.com; s=arc-20160816; b=e1CkQgLGd0TGkSkuEzMi0NuzT+MLhZhMtr7XxVDyICchcdq1dGltlS/x5qu8GRjfmE oIW0/pVXjGmitjkmx5AVHcUnkentIXfnMBeuo3t0GTH6jVfTb0YN+YbX4OErF+tV9ZrW 1jL9PQQ4htfhVMLo1CNiBLRpAL7zmVkQhEEzdOwr181QOWlQPDqrzbkuR5CQfBz1lRfe h6WSHNDPmbMBGySQ+xHEWGGM51h+3PKVZc+um67A0tg8uv2XvlX+Cc7EtGwnLcySJRFw PgvqCItWcxM3iidT8lii63X6sfEQkHrYQtsEkEgQ+GIpr1Ft1ZZ1dbTXpaWrb8WbC69y vN/w== 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=eo12nnmYUod1lU1bKZnWoZM4LAZXl1r2FscnVlQJDJs=; b=mwTuCe7Dq/3ZsUaSsa0R+c+jnPqfPjLFCFRjXpQ9+3iRlVNpqfDgVIbmUggGZRNFrQ V6AN6OXiiiX+6J03MsLz+bbaMmjSz1Tc7zycUlvSMEv3I0dSjyQS69OpatOiVSWws057 Ccnir+21yRewaKY1EUUMrIZkyjSOtHYxsURnXR/i4nEaiNqPKJU2TJwDO/0SnXAsdlp2 UGfjYbK58oOQAA555ZYvRfFMhN3/LgtXJMjqhQPJPMHnUjCJTXcn4klRkn9j6LC860wM mqmwBOw/OVM9MoYTtO3zbvS45PO2GOJYQJve2idaFWCVqm6kgLhyckth6B9kFenmvNmZ MjZw== 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; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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=eo12nnmYUod1lU1bKZnWoZM4LAZXl1r2FscnVlQJDJs=; b=lKc3MjxL0JOqJKk1Ozy2GNnU69iOWPDDEGFgyuqg2mZKWCU5ZuncH3L/FLGz2c4F30 ftJiaCAyGVdfLbbWARHTobxM7zsF0peIY6kumj8hCTCKX5QlZL8QRRdaWcoIDfwUXmOs Sho8luET2KRUKDgt9AhIMYxrt5JWCOFIV1/U28xcnJ5fGNQO0MFOFSoRSgMNHvT1chvH OJvc7PESaeFYaq5AeMfaOpbdslMq2HkbAsfX8Qa4NB+R9W7K5fCsvRJAMZSOCfFt90ky IwLFnwpigwgNfu8QBNvVTAAT2RnoL6R5sToEXy71BCFprTSMyN72SOWqplH7N6F799yy Pu6A== 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=eo12nnmYUod1lU1bKZnWoZM4LAZXl1r2FscnVlQJDJs=; b=hZ8WDAGxK0kwH+4C/C/BZLuNbFeaeDF/d9mvwc55OvTeGdvsqXyx0oFhFEZsvQTjwB uWelc/w/sr/e+QWZd3yTJ3Y1wQbe5VAEFx0nT8WOWMYwyslb+/BkUOjG02BLZERquUdc KryEKwcHboU/bUZOTBsYHMGOrRIEfBqCrj88P2uzH+xAh/oltrXqdlUph6GFS5iu0mUj 9b1zKOfQ9KE3ZOqS6wvM1eQGtycNKXy4Emu7XVgOc+V8iNAHb82rkJ9WvJt2fPBaWu/W OLYKpsVMWf5oWOlIVtHz37YuVBN6pvPUwpD+C0ArFCdHCMJbaZKttFwcieA/thP9gvtR otjg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWjQUZcZKZI+0LWZmaXx7SyHxhG7k9EHGvKAOP/koG73KSHg+ha aMwJseHv+Rv+7lYG7iOi6AY= X-Google-Smtp-Source: APXvYqwjsb0ywQPuEkJb4p15pOzrO/KhJZQP3BqypRjfrYzSWxuwVQ2MtmXvoGIht9RwbHuqec8wLQ== X-Received: by 2002:adf:d081:: with SMTP id y1mr22572656wrh.34.1559754709593; Wed, 05 Jun 2019 10:11:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f505:: with SMTP id t5ls925262wmh.0.canary-gmail; Wed, 05 Jun 2019 10:11:48 -0700 (PDT) X-Received: by 2002:a05:600c:1008:: with SMTP id c8mr1427550wmc.133.1559754708873; Wed, 05 Jun 2019 10:11:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559754708; cv=none; d=google.com; s=arc-20160816; b=GvxMd4+n1rvdhtKnsmzhgjzPM6U/cB30J4uzMy7n1hfJi9EH8Z9O0oThnXCgEkhB2T QXF/WEqekT1OqVnNVE5pp2pwQ3j388IIpKkl1ALP0EwjHJC9oJtznu8v8yznFJnYOnt9 vqBCDPOkOIgEwvAXiTGvn0/Sv/eSuBD1dRnWm8dOgYTeABVDoPg+XT7cC+xj6DPYJQnp mMElhcR8NgEUnNPnHXAyqY43tvNjafQ7aIlWEXLz18AVbNTmZb9NuW5sF2qMm6jrYV55 dlBMe9wNbndIdsx8wuL/kh6fnXW9qS/rPIz1TvwXa3CDMOMn9nMRDAaWsgd/gOpNzVdz Svbw== 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=0rhrsK/gtGHqYrRA/MnRggZfaj/hh4IaJP5fn+kdmFI=; b=yVXzMGRn3TQK4CgpVihswhFHkzWHD6+Bhv1FrJyMepPqABc9ecT2aZxeK9FeL5MUfE rOp5rVdmwOWs40Zr8l0NW52WAbCoFA2UriDZs+iUBzHw7S0I2OHGxf83C+5W+N19A0/M zsp4GGjFRzfCz43xkF9CQH0G5jlQ1tGqY5BTZdKViH5cMe9qeQlbINXpd9SJo4rHV5JS 9PoIMsxiLkMW/tYeYMqeo/rSwKYwgHaqjVmusKFZtaGo2T9DvPdrxh6FGrZWuhOHGxlc q+wOjyjalFHgrkAcGXt/goML5YLxpPqExpwCGlpB+1V2fk1hJv12ZlFNSfXa4Hx0+pRa eh0A== 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; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id y139si937762wmd.0.2019.06.05.10.11.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 05 Jun 2019 10:11:48 -0700 (PDT) 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 79A492B7BD3_CF7F7D4B for ; Wed, 5 Jun 2019 17:11:48 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id B2A0B2BB0B4_CF7F7D3F for ; Wed, 5 Jun 2019 17:11:47 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hYZRz-0007AK-M4; Wed, 05 Jun 2019 18:11:47 +0100 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; Wed, 5 Jun 2019 18:11:47 +0100 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; Wed, 5 Jun 2019 18:11:47 +0100 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; Wed, 5 Jun 2019 18:11:47 +0100 Received: from EUR02-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; Wed, 5 Jun 2019 18:11:47 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB3037.eurprd06.prod.outlook.com (10.170.229.152) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1965.12; Wed, 5 Jun 2019 17:11:46 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5%5]) with mapi id 15.20.1965.011; Wed, 5 Jun 2019 17:11:46 +0000 From: Thorsten Altenkirch To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Subject: Re: [HoTT] doing "all of pure mathematics" in type theory Thread-Topic: [HoTT] doing "all of pure mathematics" in type theory Thread-Index: AQHVEuLdO7BojRhwskuHaReP9sPJrKZ7ocaAgAA1u4CAABULAIAADOgAgAASRYCAANxQgIAAYg2AgAAH8wCAAaL1gIABWuUAgAAGRoCAAAKpAIACJCEAgAFzkgCABMCuAIADV2WAgAFl6YA= Date: Wed, 5 Jun 2019 17:11:46 +0000 Message-ID: <38C01A88-302F-4DA0-91CB-8411B4F595A0@nottingham.ac.uk> References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> <9232f85a-6d64-84dc-a2d0-290c0fc6e760@cse.gu.se> <209e2262-cb8a-4b31-9b6b-44a5df0185a5@googlegroups.com> In-Reply-To: <209e2262-cb8a-4b31-9b6b-44a5df0185a5@googlegroups.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.19.0.190512 x-originating-ip: [31.73.205.162] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 78c874d1-1cb1-4621-70a2-08d6e9d8e3b9 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:VI1PR06MB3037; x-ms-traffictypediagnostic: VI1PR06MB3037: x-ms-exchange-purlcount: 2 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8882; x-forefront-prvs: 00594E8DBA x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(346002)(396003)(366004)(39860400002)(376002)(136003)(199004)(189003)(5660300002)(966005)(316002)(86362001)(6246003)(11346002)(6486002)(26005)(476003)(110136005)(6436002)(786003)(74482002)(64756008)(102836004)(66556008)(66476007)(53936002)(14454004)(478600001)(256004)(186003)(58126008)(2906002)(36756003)(486006)(25786009)(66446008)(236005)(8676002)(446003)(83716004)(71200400001)(68736007)(73956011)(71190400001)(606006)(7736002)(91956017)(76116006)(3846002)(6116002)(6512007)(8936002)(66066001)(53546011)(6506007)(6306002)(81166006)(81156014)(9686003)(82746002)(99286004)(66946007)(76176011)(229853002)(33656002)(54896002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB3037;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX: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: jK+7EVQXxvJev8adRGGa6SY82LqODuW3PCNdKujA/xRrFY8VEUWdDoeI1s9T+xzdx56ds1uSoMrNvn4lkIcQOrBLp5TG/Q8TZRcdTuoYMTMvaJJG2soub1Ki4Yx/mFXHlprv9YA3/8V+yx4ztVMY+CUjYBA9jtG5Kbg3O3dHX+lWEKF0LvhrAvtfOp+bVZ8FBkOIU7auFIzf3EHBYjL7Q4w33r89ypJo4FMCcaSHEozmHUL1+Qk8TzqzYNlUnluXKw5BymmCY1rd636H/wk+ooInHewUASjslzX8YetEnUlYaTLMEbGuTchwSrKqmypRkTYNv1CtU9zqAIUPYkKMs0umOijZH41Cv31gk1Ep4rKk+oHSOZwSJcnvfnKaJzapAXD/leobLers+2cQ7zvsf2iPEurpzftwLTGA6xYhsDA= Content-Type: multipart/alternative; boundary="_000_38C01A88302F4DA091CB8411B4F595A0nottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 78c874d1-1cb1-4621-70a2-08d6e9d8e3b9 X-MS-Exchange-CrossTenant-originalarrivaltime: 05 Jun 2019 17:11:46.1543 (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-CrossTenant-userprincipalname: Thorsten.Altenkirch@nottingham.ac.uk X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB3037 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; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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_38C01A88302F4DA091CB8411B4F595A0nottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Sees my name was mentioned (says the devil). Computer games are the perfect analogy. You are fighting a proof and once y= ou have done it you reach the next level. But then there is still the boss = lemma to be defeated. When I started using Type Theory using Randy Pollack=E2=80=99s LEGO system = ages ago, I was playing nethack at the same time. The similarity of the two= activities was intriguing (also both were entirely ASCII based). Also you = can still to formal proofs when tired and or drunk. But you can=E2=80=99t d= o paper maths. Thorsten From: on behalf of Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 Date: Tuesday, 4 June 2019 at 21:51 To: Homotopy Type Theory Subject: Re: [HoTT] doing "all of pure mathematics" in type theory On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote: The thing I know for sure is that there are modern maths undergraduates who grew up with computer games and who find the idea of turning their example sheet questions into levels of a computer game quite appealing. I am surprised that Thorsten Altenkirch didn't manifest himself at this poi= nt. He uses to say that you can't teach old dogs new tricks. I am not sure it is the computer games (it could be, and if not they could = anyway help, perhaps). I think it is their open minds. Martin -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com<= https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6= b-44a5df0185a5%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter>. 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/38C01A88-302F-4DA0-91CB-8411B4F595A0%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout. --_000_38C01A88302F4DA091CB8411B4F595A0nottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

Sees my name was mentioned (says the devil).

 

Computer games are the perfect analogy. You are figh= ting a proof and once you have done it you reach the next level. But then t= here is still the boss lemma to be defeated.

 

When I started using Type Theory using Randy Pollack= =E2=80=99s LEGO system ages ago, I was playing nethack at the same time. Th= e similarity of the two activities was intriguing (also both were entirely = ASCII based). Also you can still to formal proofs when tired and or drunk. But you can=E2=80=99t do paper maths.=

 

Thorsten

 

From: <homotopytypethe= ory@googlegroups.com> on behalf of Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 = <escardo.martin@gmail.com>
Date: Tuesday, 4 June 2019 at 21:51
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: Re: [HoTT] doing "all of pure mathematics" in typ= e theory

 



On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote: =

The thing I know for sure is
that there are modern maths undergraduates who grew up with computer
games and who find the idea of turning their example sheet questions
into levels of a computer game quite appealing.

 

I am surprised that Tho= rsten Altenkirch didn't manifest himself at this point. He uses to say that= you can't teach old dogs new tricks. 

 

I am not sure it is the= computer games (it could be, and if not they could anyway help, perhaps). = I think it is their open minds.

 

Martin

 

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6= b-44a5df0185a5%40googlegroups.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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/38C01A88-302F-4DA0-91CB-8411B4F595A0%40notting= ham.ac.uk.
For more options, visit http= s://groups.google.com/d/optout.
--_000_38C01A88302F4DA091CB8411B4F595A0nottinghamacuk_--