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=-0.9 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-lj1-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 055fd16b for ; Thu, 8 Nov 2018 19:39:51 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id j5-v6sf1942747ljg.1 for ; Thu, 08 Nov 2018 11:39:51 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541705990; cv=pass; d=google.com; s=arc-20160816; b=EK/qCBvEVLrcN9B0km87lAV9NC2bX5dxdwwPHCzB+jhYM+zefj5Sz7Z5BhL+8CECva QtdpkUluA2WeTrNNUjVZAAll3Xt/uFbj54q+7W26xvDrpyP96glJ2gZ3y/8qVa2IXiyR TGgcK8heFEku0poQh1GzQ7T1QQSBfKr+ThQsBhE+1m2uKg39xoGOnv1Xkln/Pl3aKmIg p2RFyA94IMAgcMYX0vkOfH90HzmWPZhtifHdzYtGMqG6IWPRlYCUZWTZdSBtr/0G9nLf /9Swcnmb5fYppNU48Pt68xxyMuc5+2Z7WEHBgWnw1+1Ui1qT2YpXsB8b3nBhG57uzpZ5 n8iw== 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-id :spamdiagnosticmetadata:spamdiagnosticoutput: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=hslWulcjUncle2MNEG1cgmgdfIlBohioeJOZaAA3b+4=; b=RsNDa+Bioex5CCXzhW3vGJZtMTg95Ty3xG5inV4VRSfdV3pCPk8ueQowcf832F6cQN KhBHxD1EXMLMRvVJsLByO81jRBKBnnysPOZU5UIc/KG4LzS37S1SW91D37MXP9t9Lra7 AnAgpHp7vXCAv4DvVkjO+rOOYxue60KrIUgBOxE/BdhyDKV05BqdlsWzh0T3dGCYwyrG hqE+kP9/DZUlklcTlX31HFJJ0r/PdlfdijZAh9woqxZmsV+GaoGtjeT9mUFeNau/oZHU aXwbl1ELf0Wruy9iyqymtUHiaQj3o7BrDvz5H+nP2qKBjS1ZzxlWvnCHZTYqmXEDH9yf UmsA== 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 :spamdiagnosticoutput:spamdiagnosticmetadata:content-id:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=hslWulcjUncle2MNEG1cgmgdfIlBohioeJOZaAA3b+4=; b=s4EQm1v49M4qzPU8YzI4L8zr74vaVC/3Kq6u24sJOa+LHCVFT+IgnM8fQKLz777ypv oUmAtzJkqPRphRHfRNA88FgWHraR9CK/CSpYGoaxtqGRur+QOn6CF1h7RJsH9AqGd1tK Vryfof+tRrzaRCzt59rPVDWM7VGJ0VHdYhqnryexet/LVLlv5NFVeN6NfAAeFB1wuvRd 3qY0w5dW+d8BvBK7MyHFAmIUYGGQWrzhebIRYXHfe3lux7jaqr/SDQRHn8QpgEfd5o43 kPxzgVl/Wu3iA7kQlVf+x6ZmQa7k01J8a4X5oPFio02Qf86uQ/MYMexrUs0XS1mLgjDI eqkw== 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:spamdiagnosticoutput :spamdiagnosticmetadata:content-id: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=hslWulcjUncle2MNEG1cgmgdfIlBohioeJOZaAA3b+4=; b=b+dtkJIaZova70+R3R8KMOiU8+cY6eQoPagPOkzhGuDJJzdbiqkeUae+tJ6/dl0u0J rGHEOC6rPAgto2MkhxUDQsYnKnCHf2dVEYKv0QXNBQ7ZNwIY1pZaSxIgDVqUZis8Zsc7 7LOpVoKAoC2X2q20lG8aJVcZVCeT11SCg1hqEPd42MUY31yAnJgQU0iLsZjLbZ+rMOEa A+j9tMjMImkTzLqlOmIDAMLOOZF19HrE1jEIu/yBrcijqAuEeBi6DtE3KA5Ai4BGutVv mXtoCWaE3IYH6bC3Qf6/5VweIBupdjNBGbk3Z99zvELpexYwsqzM5X6ox71GhqNGEfOr w0Kg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLZbYalxHQGV74lpsrh8DLtPmMdW4OXuQpggFigXmgcfAXBHIYo PHyeIBm1xO/7wqX3uR0CHv0= X-Google-Smtp-Source: AJdET5eyGdtFK5UKIM2FrrbVB9pa2ScpSzO/4SopeBFzuG5bWIy/3hfZwo3meT8hGCwbAhRhOv7feQ== X-Received: by 2002:a19:ed17:: with SMTP id y23mr32936lfy.1.1541705990713; Thu, 08 Nov 2018 11:39:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:350e:: with SMTP id z14-v6ls297530ljz.25.gmail; Thu, 08 Nov 2018 11:39:49 -0800 (PST) X-Received: by 2002:a2e:9e4a:: with SMTP id g10-v6mr633720ljk.26.1541705989768; Thu, 08 Nov 2018 11:39:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541705989; cv=none; d=google.com; s=arc-20160816; b=DMwzlGN4E731JkBjUM+LA/NAM/X5bGWvf4QOmi8IMfqI7x/RdoN32nVejJjR5BCL3P 8sgujftKexE6NJZWYfL8UgvsjcgvX7181OXev8Y5C6B3OzWaj9F/Okmf5v+aHiR6OBcQ eptgJCx8+w8FjAq/a3oE4pzpoDFSSfCmz+ykNo3CPNgx5IL/1MafpErto3vMkgeqPZ4i zs/woCfLCZkxJh4TYdkQ7Btd4iEBGNNVs4JAfKyUOtLt0ypIkJV3qhwh+VmPDr5Tr06E N4M0NTmlFi2ZdjTA+3ZLQ1Quf6vYhyWVo5tO9Lai695tfKWGz6scMxZ/FfllzXs+Wv/M htyg== 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 :spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=b+IiahtY3IRwpiFTBWuo1zfxzBrMfDySMihfeeXMBtk=; b=wL/GBzWXQg/vX5bLV4JNSevLKtLcVb3q5+YfAey2eugb3Me8420cMagm/gfOBoYFY+ plYXEcfuiWWvu/iDeg/sqbdksT//ENVuOPzoWfYO2wJ2SKvrX/c30NLWbbGeL771YQie qSiFzwQZOEgXzpSyl1Q0pMUkY/ifwH0D2z8XGoMPVCIC2ucxq25/nMECaeonlX/2wH1n G5VWVhdY10rCzLYvP4Ou+2wM7lhurVU27QxniXSGJTxczm1y6Gimk5OC5iTsurcLmuHt jLbjZJaKHQIAk8WyHDUVapIlcPazVMqfBlmKHzI7xNKyz4WJjM7w8ljDMPabozDdvmmH OlQw== 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 l5-v6si208102ljh.4.2018.11.08.11.39.49 for ; Thu, 08 Nov 2018 11:39:49 -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 D998F2B7D00_BE49104B for ; Thu, 8 Nov 2018 19:39:48 +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 5F6AD2DE2C2_BE49104F for ; Thu, 8 Nov 2018 19:39:48 +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 1gKq9c-0004w1-Av; Thu, 08 Nov 2018 19:39:48 +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; Thu, 8 Nov 2018 19:39:48 +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; Thu, 8 Nov 2018 19:39:47 +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; Thu, 8 Nov 2018 19:39:47 +0000 Received: from EUR03-DB5-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; Thu, 8 Nov 2018 19:39:47 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4558.eurprd06.prod.outlook.com (20.178.8.139) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1294.26; Thu, 8 Nov 2018 19:39:46 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4f:450e:6b43:f35c]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4f:450e:6b43:f35c%5]) with mapi id 15.20.1294.034; Thu, 8 Nov 2018 19:39:46 +0000 From: Thorsten Altenkirch To: Thorsten Altenkirch , Thomas Streicher CC: Ulrik Buchholtz , Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Topic: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Index: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAACergIAABn8AgAASxQCAABXOgIABP7SAgABD9oCAADysAA== Date: Thu, 8 Nov 2018 19:39:46 +0000 Message-ID: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> <20181107153556.GC26970@mathematik.tu-darmstadt.de> <20181108115815.GA5022@mathematik.tu-darmstadt.de> In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.5.7.151005 x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB4558;6:FZC3YxpUIs1j3wiiGgkTDxE1UQSLuaf6zGOcZ+C/ioAbmux/Xm+EDfkymsQFVHzt9ttNsN4CCmByMBcLXcCCpt1rkvIq7uUQk86huZifZ91+9bDziblG/U/v2XRUeojnXofVNdwv8Zpo5nQb7z+HbLrByAvrgUGq5yODxO4buMArcM4+C8bUfIwng9GrbppmplQqgltTQebXRi3O54xxXmMnVAGbOHbuJTZnHUjxv2V5yRKMln73Njkaq3wxaktNq7MYgH2kJv1xmELqHyU50KWeZtwyeY87hK4XTnaNfWbN24fxpUHrqgIBsCfJd1tHRl0Nx+f8CtawXImCplO5FH8QdvzXDkBweReT3ORsenUDznj7uk6KeSp7ewk96ZI35P7r0XoguS3PLCLIa5uuPx4Bm00m6CbtjoolEIM1wGLBureUjDk6jG+FTR6aLwqr5Qf+z1RVskBA2et9L6KaIA==;5:i5U3t5Vra+Xwyt4mBAAACvwZ+9cn37Q4hAYnXQELtedO76LYQJSDPxegBLiNpG09ftaYIDK/UqlN+AQR5QmzyZ2/oMekJ7peolzX7txUx+iIIAlaOznpiWe+Jyd2xE7L2xh1xhQl3Oi9sa16qJ4/vURflCfreGi3k0kjP8shnZ8=;7:4q7TTArrYpf8Jj8BeVwoXGxk7ChoblLtugVF6C78V4Sm66Lp1dJh3Xol+65k8djo+iH3GT0pxz7W+aL/dd9WEhPxC7enSWIY3JCVJTgLatG7gQ3cvgCiApoPW7o39rGhfHOqpZdtA7Awg6u5qT31pA== x-ms-exchange-antispam-srfa-diagnostics: SOS;SOR; x-ms-office365-filtering-correlation-id: a1bf7333-c5b4-482d-3142-08d645b1f098 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600074)(711020)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB4558; x-ms-traffictypediagnostic: VI1PR06MB4558: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(76576733993138)(165104125076784)(228788266533470)(211936372134217)(214861330456307); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(93006095)(93001095)(10201501046)(3231382)(944501410)(4982022)(52105095)(3002001)(148016)(149066)(150057)(6041310)(20161123560045)(20161123562045)(20161123564045)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB4558;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB4558; x-forefront-prvs: 0850800A29 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(39860400002)(376002)(346002)(396003)(136003)(189003)(199004)(81166006)(74482002)(8936002)(5660300001)(106356001)(68736007)(966005)(105586002)(14454004)(6436002)(4326008)(229853002)(25786009)(2900100001)(97736004)(6512007)(6486002)(6246003)(6306002)(53936002)(2906002)(66066001)(81156014)(7736002)(305945005)(39060400002)(3846002)(86362001)(478600001)(6506007)(55236004)(6116002)(53546011)(26005)(76176011)(99286004)(2616005)(110136005)(58126008)(256004)(102836004)(186003)(14444005)(54906003)(786003)(486006)(476003)(93886005)(5024004)(316002)(11346002)(71200400001)(8676002)(446003)(71190400001)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4558;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-microsoft-antispam-message-info: /i8e5z1Z16z45rZseBukkxwHMFazDt1jO1RvpfgR3V2hDtpAT0aR0aH49wS3csCfcpqeHhPX1STL42TAwxTOqYiJ+beASDgSqxNvzLJKB9RneVlxCmR8y5epXV70514+es3Lu4MfkEYs+WkndhJwyyg9+V9c8w1SjH4ukH9FPueiqjYzIAfLdvluPXsQak3P2tjOMJpXtb6XsN6wCV2RmYIsZgKRXejnonr3Sdl2LRkYSKqXwJzfOkRpzkCtubbepgfBz7AYUjoEpdQRtJbFNNmF2zDpQafv/luIEBSlf09miD9L7XD7xtKs3hziGKXZgU/Z/HUejMaUvWWj23kPEZRyaI5OQcp+UZtY9KlM40A= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="UTF-8" Content-ID: <2DE82328C0EF8D47AEF6D90818D97863@eurprd06.prod.outlook.com> MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: a1bf7333-c5b4-482d-3142-08d645b1f098 X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Nov 2018 19:39:46.7027 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB4558 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: , Sorry, I was to quick pressing send. We need the category to have homsets C : |C| -> |C| -> Set which means that the equations of a category are propositional. Similar we need to say Fm : C(x,y) -> |F|(x) -> |F|(y) -> Set and add fibred id and composition and the laws (again propositional). Thorsten On 08/11/2018, 16:01, "homotopytypetheory@googlegroups.com on behalf of Thorsten Altenkirch" wrote: >Hi Thomas, > >two answers: the first is that in this particular case one doesn't need >strict equality because one can present this as an indexed structure in >type theory, e.g. assume as given a category C then a fibration F is a >structure with the following components (here I assume that the base cat C >is given by objects |C|, morphisms C(_,_) and so on. > >|F| : |C| -> U >Fm : C(x,y) -> |F|(x) -> |F|(y) -> U >id_F : Fm id a a >comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c >coe : C(x,y) -> |F|(y) -> |F|(x) >coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a) > >The 2nd answer is that this is not always possible and the most well known >example are semi-simplicial types. In this case we can produce indexed >structures for all finite approximations but we can't generate the >approximations in a uniform way (the question is actually an open >problem). However, you don't want to force your categories to be struct >but you want to be able to talk about your univalent, non-strict >categories from a strict metatheoretic perspective. This can be realized >by a 2-level type theory as for example explained in our paper [1] >http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf > >Cheers, > >Thorsten > >[1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561, >author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus}, >title ={{Extending Homotopy Type Theory with Strict Equality}}, >booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL >2016)}, >pages ={21:1--21:17}, >series ={Leibniz International Proceedings in Informatics (LIPIcs)}, >ISBN ={978-3-95977-022-4}, >ISSN ={1868-8969}, >year ={2016}, >volume ={62}, >editor ={Jean-Marc Talbot and Laurent Regnier}, >publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, >address ={Dagstuhl, Germany}, >URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561}, >URN ={urn:nbn:de:0030-drops-65612}, >doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21}, >annote ={Keywords: homotopy type theory, coherences, strict equality, >homotopy type system} >} > > > > > >On 08/11/2018, 11:58, "Thomas Streicher" > wrote: > >>Thorsten asked why I prefer to have strict equality on categories. >>The answer is that one needs it in category theory typically when >>speaking about Grothendieck fibrations. >>And the latter is most useful in many contexts in particular when >>understanding geometric morphisms. This by the way also extends to >>Grothendieck fibrations in quasicategories as in Joyal and Lurie's >>accounts. >> >>Thomas >> >> > > > > >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. > >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 >where permitted by law. > > > > >-- >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. 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. 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 where permitted by law. -- 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.