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-wm1-x33f.google.com (mail-wm1-x33f.google.com [IPv6:2a00:1450:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e931e4ed for ; Sat, 9 Feb 2019 12:30:07 +0000 (UTC) Received: by mail-wm1-x33f.google.com with SMTP id y85sf2926450wmc.7 for ; Sat, 09 Feb 2019 04:30:07 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549715406; cv=pass; d=google.com; s=arc-20160816; b=GIhQvz8n5YrbTt3LgzBkozsVBUnTHFNvrAAx5I1p8DQlx7hSvSb6xyFchYkbuHAKDC 7Ro9O+5Ug6BdU1X1KyMTfOHo+K1bujLPtqehwK1u323r6N5S0xTa7hxDojeexew4uSo9 ihp35ryw1WC+1XhvIMvFj6jVttmUsHbYEsshlJ1ScfiLJzL1/Yl6m85DoL3AHAO1cC9v nuWdcEIXqyg6Y0gFBeIvniy+/r4hnCOD4l3goBHkRZKPW0EHj3k6HnyH9QAGa+jncs3N G6do3O4EBnd3ZVhKu48zx5ZUBIBp+imj5oDB2SMkno+YArfLHBjfRnyLW8CMGPwGIox6 aeKA== 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=Xh2INhc7c1JIsBWJOSW5kfCOPYLwUkZEw8nYJPU2jaw=; b=sujYxUvd0ncOPgXHSf8mFywkfa/1mNT3l2kiBQhwyZzJc0dy8+0RE4fEMoJ3HYt/SF lL843j+cABEpWpMCl7Pl/9UD1weRXIRfa7rmFAufkYnACxzw8c/BQILUvAE1ADraimFM h5ZAKtgue/OdLL3ITc2d6At2LDXe579spNPAcB2OZ7GuDrLq/tMBcnh87giaFGK09cz6 2UQOTEwrSapC9UBidk4sOG/mFTK+zFPN6ri5FX9bVdYoSipOYL+KNVhamMnXiC34uN1C 6uJyPpD0/OvS2UKeJ/Gr4gRZZViLM20vNbbylFFELQ7xeo12oDplmu49idpc2DNZYkNc yZKw== 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: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=Xh2INhc7c1JIsBWJOSW5kfCOPYLwUkZEw8nYJPU2jaw=; b=btHx/OTJXbtciEHcHtfI6UfwB3ASAJmfVwFWgDl7IKl4rmOX/GASWi4K1af8AC86Qv agD27u3sRy8d+zAqLzYyzuKeb0pd8n0tWEQVhaMuabLDq9Smdk835YiNQ4AtuhgX0jqN /ElXnC+B7rZ+u9xbN9iVjmIRr9tQaQGl4P1X4ZHZBrXzW2O6iw5AN5IdWbzjrgPEP1bW B9OTkTuwHlE4bowDeJFcjABoPT65x+LiqPGCI2D71nZGF8fGZaGO2a6GIRiGrdXzxnjZ lpqTBQaChTh+YSoVXWkp5SJA3h4FEld4Xq2isJj81o6OUlaBW7un0zWroUnXJpu211b/ p70A== 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=Xh2INhc7c1JIsBWJOSW5kfCOPYLwUkZEw8nYJPU2jaw=; b=RXiJ806CCq0V5Xr5A7aPRYbVMzDqvQcfNKkeFypnSIf2d8Z0lymORqHUxjd7AbO3V2 Z7OnNEnzbnWQ+/k00jgn4hAfeb6zBVf28H4/6mbAEsW9uNxJ/rt8YZwwh2KhXpq1zNff 6VMyebQMJVlIKnqzHkW+aG8HFFHsEW6dPsHFLz+4CII/TF8MsgmDBhiXnOT/bfd1rBg5 Gowuy/QLJL6ttlORNgj97/08PtLCcO3mSoik9QSMtEXJ3FfI7uBUkF4fkDNhZUBRYRWn yRFK0NObrqe+O323EI+KkrjTnU+AGUqcln+b5d6Aiy1yleqqOeFLFK5lnPTv4wpiDFDY daJg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubtUh2oijq84P6mZNGWMEfGFHehWoNvpVwc0la7UMERY7KDybI/ ZbRNOV2uWx0jmqltkb0TmXU= X-Google-Smtp-Source: AHgI3Ibl/ruUoYiNLQRYceDw54opw+LclWLUqAaLrxg/eC05id3dY14W/iYwYO7jLfCUQE2VHjKIeg== X-Received: by 2002:a05:600c:2157:: with SMTP id v23mr13312wml.2.1549715406674; Sat, 09 Feb 2019 04:30:06 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:544c:: with SMTP id w12ls1652406wrv.13.gmail; Sat, 09 Feb 2019 04:30:06 -0800 (PST) X-Received: by 2002:a05:6000:114e:: with SMTP id d14mr1374053wrx.5.1549715406008; Sat, 09 Feb 2019 04:30:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549715406; cv=none; d=google.com; s=arc-20160816; b=iTMJF7qmHeB5QnME/yh02BO6eLHPyuIdkOXdeGcktjlgfM0Pj0waZRJwKHDH2hNtGf dCSpCBOGAVmFc6Jyvg3lrvMZS5raJvAJMdQA2mWAW98CVTk2KQz7fErXV69gJMUWm4Ut 9P5fMfyK8RaTlG+ARfewUNKKIcR+FQbwONAbbDxgR68kW57/B5dQp7XxduQ1syj780aJ 9MAWMSC+VQVJiS3k+e+WKfbYMMa0YYtTkNsivP+XU6IeEpLFyNXFZUh9gdprafBaoPj1 0LOvz1sF9RSUzVC8aCD5cvzhC5GoDLqTu9UqemyUrNaoWcUmzsFO40Se80j9Gx7YbABx yfEg== 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=pqmHkE1ggs7FbzXzDptYu1EygXNNsL/A3EGfTUWIT7g=; b=NLXeUjtyDdxbEMn1H3SN48M+PgbFTYyxd/jyomcD9eqUg6frqBViS3izT4SwIQbOYs 0EMNREdC3R0i596qjNVBeyQ/n2D8h0LIl5FHX3ra8fLgV3voxyhE4Q8Eav3ktzBomhOW w4gK4Sy2WrGmry+WnXoljYCA/qUXIlyw/7h+xqiZnwise94XK/UkqJ9dDyq7BCH0eJ/K ZaLopuMuLNCQrbRtNDwsGLduUDcJldnI4RQCgzdF8VDYoYyYfWNOaYeDo9LTFiEDCTZU pEmA91IogkoX2bAePHqqjpTkSgDOHBODnljdh/A4otnwqj9BV7EMlVfgwO/y+a5QCrU5 bRTw== 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 t23si865304wmt.1.2019.02.09.04.30.05 for ; Sat, 09 Feb 2019 04:30:05 -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 A7E622B7D4E_C5EC7CDB for ; Sat, 9 Feb 2019 12:30:05 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 553182DD9AD_C5EC7CDF for ; Sat, 9 Feb 2019 12:30:05 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gsRll-00039O-A7; Sat, 09 Feb 2019 12:30:05 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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; Sat, 9 Feb 2019 12:30:05 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.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_GCM_SHA256) id 15.1.1531.3; Sat, 9 Feb 2019 12:30:04 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.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_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Sat, 9 Feb 2019 12:30:04 +0000 Received: from EUR01-HE1-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; Sat, 9 Feb 2019 12:30:04 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5757.eurprd06.prod.outlook.com (20.177.202.81) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1601.19; Sat, 9 Feb 2019 12:30:02 +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.016; Sat, 9 Feb 2019 12:30:02 +0000 From: Thorsten Altenkirch To: Felix Rech , Homotopy Type Theory Subject: Re: [HoTT] Why do we need judgmental equality? Thread-Topic: [HoTT] Why do we need judgmental equality? Thread-Index: AQHUuJKkRfTqtVJmYkaya4nBulFc3KXXdTUA Date: Sat, 9 Feb 2019 12:30:02 +0000 Message-ID: <730FBE36-8E4F-45F5-9DB9-3B3A04E708FA@nottingham.ac.uk> References: In-Reply-To: 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;VI1PR06MB5757;6:P3F8QObDOdnPc4MOAXrQaJ7mn+SKUQHW6LQd5VSaGOuxk9+RMUeoTHZW7Zhj+WIuh4SPQ57D8C1lTB0Nl3CobOf4WN4n6/q32v6z9zpmWvwJRzpwXm1RcR4ZCfehvLPh/weOhkGcbs5CvRP5Y5jFxltSl7j6GN+mN6gzHmhIgo9UoY6GoUJagRugVyvVqCxq6/Pchn82Brz75pdF1GaKWJE1Nv7K7YQk9J45k+UBZbb39vC+Q5Nvuctgy/dF3DgSFaH//PPXjpqVrJJikgIxMAqCiGuRd/7ePmR6Jb9bM7FjH447/rXLNMevAx7tcPWA3f9eJ2doxcVXvyx6JAKLq3G1gR3uQ/KLbwHo8IbpCtlehP/Lcx82z6ixev0qq20jYufvdKiZHga8UfTFH+19GYYVpDtQawnqUkxt5iNdckdRok54Bi8kVgsxKTmqOW/+cdGwyjmZftW65+XtIqDuaQ==;5:DPui4ulep2RYifWZQ3cC1whU27GBNWDTAjhn0ypKxgPpBamk/qX9U0mjFq0MfHHL1OeQxC+eADvLG8g7fo8t9lsaV1mI+NiiN8bp7aSzx5MN6xRY7tAGhGpLiYqwGi8Iw9M3M1FstZ0AGG98mr7CR667nLh5m8ZqoT+OBIg4nnSGUPBwhzM7D/n4QtUykYAbiLeJ7j5w37e5nvy16uVE8w==;7:Z6KpLtYLsWHcGd65tGlrXOVIbOt65d0P5NaYoWWiDGwshqJsD6hHAypWE0GMh1GHD1qM2pX1FmWUefD7lZRqxwjwgAHObPZHvZa5/MQtiCvtd3BTHL1JqGOqOcjLc7h7Y9iMhOmz6kuq67yi0uAUTw== x-ms-office365-filtering-correlation-id: 3f3823df-cfad-434a-ee66-08d68e8a50aa 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:VI1PR06MB5757; x-ms-traffictypediagnostic: VI1PR06MB5757: x-ms-exchange-purlcount: 2 x-microsoft-antispam-prvs: x-forefront-prvs: 09435FCA72 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(39860400002)(346002)(136003)(376002)(366004)(189003)(199004)(66066001)(8676002)(6116002)(9326002)(99286004)(81166006)(81156014)(68736007)(3846002)(97736004)(7736002)(33656002)(8936002)(82746002)(6246003)(2906002)(9686003)(54896002)(6512007)(6306002)(236005)(26005)(966005)(53936002)(14444005)(478600001)(256004)(606006)(14454004)(186003)(74482002)(76176011)(786003)(58126008)(25786009)(86362001)(36756003)(316002)(486006)(229853002)(476003)(11346002)(71200400001)(71190400001)(106356001)(55236004)(110136005)(83716004)(446003)(102836004)(6436002)(6506007)(53546011)(105586002)(6486002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5757;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: Jr3m/C367Zo6Uu5O3Ya+V7FutUlCkVTBlRbEb6Ra8rCCRhSe6Y9CqqD8A/Z+mCKcZaE9oZYbgwfc4Q9lQQWXyX70kuUTDUgWqOlIISf0hGAUN089rSCd2Of1MJkWGUhp9fZcTRHJaJLYYcYB1CCr2WzXSJmhLyUSEJtnyTOKyOiqXkptWefmdCqMoAwGWf3jCLFdcSwJLxtnfqK2r7eMJvGsEkIbpuZeTVWS4kWu2nO6v8QoEBOJCToHNoVpwgZN0lCzrt3fkQrIklb14CmNicoqci+7K5iDcU1mEDPMNuUVmdd3xKnki7HubzGJ6GiD0XzcjHdkvQdu0Jmqigwc6wMYNUu3FC2ECpnrwa9iViFeEizOunhCyXOT69T31gC6pnayEFTeKl4IqfTrZjPvwtge7fgKwSd4xzKf+xZ3bmM= Content-Type: multipart/alternative; boundary="_000_730FBE368E4F45F59DB93B3A04E708FAnottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 3f3823df-cfad-434a-ee66-08d68e8a50aa X-MS-Exchange-CrossTenant-originalarrivaltime: 09 Feb 2019 12:30:02.7743 (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: VI1PR06MB5757 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: , --_000_730FBE368E4F45F59DB93B3A04E708FAnottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, what we need is a strict equality on all types. If we would state the laws = of type theory just using the equality type we would also need to add coher= ence laws. Since I would include the laws for substitution (never understoo= d why substitution is different from application) this would include the la= ws for infinity categories and this would make even basic type theory certa= inly much more complicated if not unusable. Instead one introduces a 2-leve= l system with strict equality on one level and weak equality on another. Fo= r historic and pragmatic reasons this is combined with the computational as= pects of type theory which is expressed as judgemental equality. However, t= here are reasons to separate these concerns, e.g. to work with higher dimen= sional constructions in type theory such as semi-simplicial types it is hel= pful to work with hypothetical strict equalities (see our paper (http://www= .cs.nott.ac.uk/~psztxa/publ/csl16.pdf). I do think that the computational behaviour of type theory is important too= . However, this can be expressed by demandic a form of computational adequa= cy, that is for every term there is a strictly equal normal form. It is not= necessary that strict equality in general is decidable (indeed different a= pplications of type theory may demand different decision procedures). Thorsten From: on behalf of Felix Rech Date: Wednesday, 30 January 2019 at 11:55 To: Homotopy Type Theory Subject: [HoTT] Why do we need judgmental equality? In section 1.1 of the HoTT book it says "In type theory there is also a nee= d for an equality judgment." Currently it seems to me like one could, in pr= inciple, replace substitution along judgmental equality with explicit trans= ports if one added a few sensible rules to the type theory. Is there a fund= amental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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_730FBE368E4F45F59DB93B3A04E708FAnottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: <65BF0AC0E1A2344980FA2718830FBE68@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable

Hi,

 

what we need is a strict equality on all types. If w= e would state the laws of type theory just using the equality type we would= also need to add coherence laws. Since I would include the laws for substi= tution (never understood why substitution is different from application) this would include the laws for infinity ca= tegories and this would make even basic type theory certainly much more com= plicated if not unusable. Instead one introduces a 2-level system with stri= ct equality on one level and weak equality on another. For historic and pragmatic reasons this is combined w= ith the computational aspects of type theory which is expressed as judgemen= tal equality. However, there are reasons to separate these concerns, e.g. t= o work with higher dimensional constructions in type theory such as semi-simplicial types it is helpful to work with hy= pothetical strict equalities (see our paper (http://www.cs.nott.ac.uk/~psztxa/publ/csl16.p= df).

 

I do think that the computational behaviour of type = theory is important too. However, this can be expressed by demandic a form = of computational adequacy, that is for every term there is a strictly equal= normal form. It is not necessary that strict equality in general is decidable (indeed different application= s of type theory may demand different decision procedures).

 

Thorsten

 

 

From: <homotopytypethe= ory@googlegroups.com> on behalf of Felix Rech <s9ferech@gmail.com>=
Date: Wednesday, 30 January 2019 at 11:55
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: [HoTT] Why do we need judgmental equality?

 

In section 1.1 of the H= oTT book it says "In type theory there is also a need for an equality = judgment." Currently it seems to me like one could, in principle, repl= ace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. = Is there a fundamental reason why the equality judgment is still necessary?=

 

Thanks,

Felix Rech

--
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_730FBE368E4F45F59DB93B3A04E708FAnottinghamacuk_--