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-wr1-x440.google.com (mail-wr1-x440.google.com [IPv6:2a00:1450:4864:20::440]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5c49ec2c for ; Sun, 17 Feb 2019 21:41:43 +0000 (UTC) Received: by mail-wr1-x440.google.com with SMTP id f5sf6950955wrt.13 for ; Sun, 17 Feb 2019 13:41:43 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550439702; cv=pass; d=google.com; s=arc-20160816; b=bWip/kWuPsN1NQraCEtCvOu0WBsLgnPF6EDy5FwsxbbgVa/o1KPVVGsixgAVKLwCHa bZhuiNhPV8m0YGRfaSZwguPib7Fp1+tn4bzOcfRzhji+1dN/Qla3f+/nKp60bzh2WOcA xuHZ78pBHjKzaX1pvXeaxHF7XB/j+M0j0Eanxe/HwjitPEQGnySmrMYTyf9duDnBJsuj oHIgaXWyphjPi11X5j/LDstsccybgQJsheCpEQG+v0qHYv7wChOB5vnYRJVsdDjUgcmY hv7e1b53krJ5dY4PtkIdCXxzWAKRXCda1MOO3WfQD8q2r5LSYZX9SiVZ8zYpQCvDgalE cZQA== 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-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=lq2nb9MMrwx9uNE4JHk8InuVVZPiCIIhqQYobrJj/AY=; b=Ju9la7ZbZ8oRGn9TsmvEIwfHDmFUomeNN3Ou0EvJ/j9d0H5ZZBEazuS31Z7pJYNAw7 Bme76Ul8UmlyGLbYrPJrLsbPxpusqSOusYB2x4VJ7bPyhGM88VWkpfWPwLSWpA7vWsmo t5hPRobtz4SYoaqFHVVbyqEPOCgigIRAvoNBT8r1gBw5FONdJAXkk3DEWpyDAtfCZqLv QWhE5exXtx8IZ6nq5L3OZFLwWRBOQjBXaR7CyczGCz94cSAUyfZEvqMJMv/v3Pk/31mC 4xG3dA9Zeh+NQGe8UIoHkg/aetodWwcUWObfbWKYZRYX2i+VWXHLgJAOPm1w60kstjdm dyqg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 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 :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=lq2nb9MMrwx9uNE4JHk8InuVVZPiCIIhqQYobrJj/AY=; b=MciJ64wy3M0nP2A/yxOSTSzNN1c5BVPursSAmyuc01+9GP4qr0HWvxQCoBbm7TJqxS f1vM5bn/qDs3Kf2Nd6gFUJWRAi7RQURvxL5F8OViHMZEoGMG8FmCOuVQdolbRPS11dbm RKAjeICkREkMKafFF6Hcy/zHDYxgzXwVPe34iFCO5t82lKYVz41y+V0jPVIuNx/khpSr nIrSAMT81lyKLwVNXb3d6pIHsp9s1dT5xVBS2c3kT3AkDLMMJy6Z/KJmsMgSuSWa96C6 r+JLG8wnobfSBdj/pW3um9AGvZIImHkOpEQXR1iepLaYr2LhgGYMffeMbQiS0htufkjA u91A== 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: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=lq2nb9MMrwx9uNE4JHk8InuVVZPiCIIhqQYobrJj/AY=; b=Zx+BQ70YGpWqqLTAzfTytGaHc1LuzxR58UPm1R1OWk0HeaIy5B5QJPvKBOALAjsF8g NL0WQNwtIvDEu4kZh0gbKLDmD3NNdNJzHL1SImVWfzxAChR/MBrEZlZ44t36ht6ZIoGR hjm8VGSBuswCAnGLJclHSC+W/XutZCXGT8ULE+YFzQZS5EkX219yKFJ4Vrv2Rh7DE488 6wLQ9CDtO0IElfw399HM0HQQuYwdqVXXnakNNYQPek/a0/rd52majYSnnlELxasPnY7N AL2BCkV7pwJ3HlIK9fj1gI4wMSztFdRyUsQ39mMJH7eskbvshaaaPMKuJ2eiCnjv0kRW sLkg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuanBZezR8IZNJzdug1Z0gHHalj+AI99vPQZS861UYx33yZq1oLU a6mZAnnAOU+LYOO/601+WZA= X-Google-Smtp-Source: AHgI3IbWl/YyblDV66FUkAsb1fvq96xl3xwXrpgpypTCiq3Mw5cBCy2JlxvIiUxPY5chSs4b7Pevug== X-Received: by 2002:a5d:45c5:: with SMTP id b5mr155672wrs.7.1550439702719; Sun, 17 Feb 2019 13:41:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:a1c3:: with SMTP id v3ls2249947wrv.17.gmail; Sun, 17 Feb 2019 13:41:42 -0800 (PST) X-Received: by 2002:adf:bd81:: with SMTP id l1mr928079wrh.22.1550439702139; Sun, 17 Feb 2019 13:41:42 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550439702; cv=none; d=google.com; s=arc-20160816; b=RJt+uOoL5StJU8mJVLU6s8XmMswYbVn1Uqdlg/GhifnELRMReatT22YTz3WqjIbq/9 YAioDuBw1WowG+si7SW0hLV6QySqvBvNZxzLTUaBNJ3drJed4Hn2FW/O8KOMuI87ji/T Dq5R5fei4cqzHbSXRYwLCxsT7smxTk9zHJW8kI0qSbu7PRSjolMMajDbc1WoL2w8388T jW4E5hVWk1/phQ6kQ5W3lv6f1Cf3lofwrqo4NynccGpGMk7dmbqEH0huWpismDdnSftG J9yP4ILrlKhtunLNItdkBcO56I7GdfVy4JRONSMRNWJwzYfOxvbO5qUzp77TUPl6npSZ JgYw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from; bh=7ElbApnUWn45ct8iigvgO/iTACb78zYkvOSf/pqBcR0=; b=xTlrRBF1V1NqQu509WUl2s/LA4h1aAy4BZ8+RvRUGzVQtuHMY2EXetsxVDGolf8QV6 TTnIlN2Xb6763U8bbE+zUSAzBNCeoKmND1ui2G5wAHvc5g+QaODd4C90XnOzklbeVlRh BApHE5/dkkkP5W6ED6yDKRKlmZvnotlyiExWTeUb8k8BnnR/CnT4iKMQPi4aBZcmkbX9 iqWxwLGX3F6QkTGZmyuSGAOHm0FyOeCMTvqhzo9/1qmWeneupzMC3AefUb00KoM0DGsF depk6nMRpXzD0/3pN1B1pU/3v69BaRCTmXdlNENlcghgBv62D1H29LRQYTMgEITI5FAs K+sw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTP id y6si467564wmd.1.2019.02.17.13.41.42 for ; Sun, 17 Feb 2019 13:41:42 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id C5AD63C469C_C69D515B for ; Sun, 17 Feb 2019 21:41:41 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 9BE973D4CFE_C69D515F for ; Sun, 17 Feb 2019 21:41:41 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gvUBx-0006X8-CV; Sun, 17 Feb 2019 21:41:41 +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; Sun, 17 Feb 2019 21:41:41 +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; Sun, 17 Feb 2019 21:41:41 +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; Sun, 17 Feb 2019 21:41:41 +0000 Received: from EUR01-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; Sun, 17 Feb 2019 21:41:40 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5712.eurprd06.prod.outlook.com (20.178.122.210) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.19; Sun, 17 Feb 2019 21:41:38 +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.1622.018; Sun, 17 Feb 2019 21:41:38 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: Michael Shulman , Homotopy Type Theory , agda list Subject: Re: [HoTT] Re: Why do we need judgmental equality? Thread-Topic: [HoTT] Re: Why do we need judgmental equality? Thread-Index: AQHUvaaYYqfVw+3Xi0mp7irBTonfqaXSKVkAgBB8egCAAJ4wgIAAbUwAgAAW9QCAABpGAIAAC88AgAACoYCAAIPNgIAAIwu0 Date: Sun, 17 Feb 2019 21:41:38 +0000 Message-ID: References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> <5831E465-6CC5-476D-8C2F-43E5B0D63017@nottingham.ac.uk> <0c48660f87d8ead6d1bd2bc5e61d8b6f.squirrel@webmail.mathematik.tu-darmstadt.de> ,<20190217193613.GA676@mathematik.tu-darmstadt.de> In-Reply-To: <20190217193613.GA676@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 3735b156-2114-4983-2a17-08d69520b2a5 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600110)(711020)(4605104)(2017052603328)(7167020)(7153060)(7193020);SRVR:VI1PR06MB5712; x-ms-traffictypediagnostic: VI1PR06MB5712: x-microsoft-exchange-diagnostics: =?utf-8?B?MTtWSTFQUjA2TUI1NzEyOzIzOnBvVWgxV1Q5ZFdBQ2hLdm5mTm56Y1ZQd0JY?= =?utf-8?B?UWNGRFdMRkMzcEFZbU5sR08rVDhXdFl5OHJiRnloWjgrV3AyWEhYb2wvdnkr?= =?utf-8?B?cU9ZeFArbGZ0cm9zRUlrekd2V3hYdzZYMHNCNVBjWHl1c2hNdWJJOVRuSUg1?= =?utf-8?B?Q2dzMnNtME9EL1hldjNucEM2QVd0WjR0dUxIM2FIdXhOaS9NZUVFVHY4ZWds?= =?utf-8?B?dERXK0RaRjI0S0NKNHRPYU1zTU9zS0VDRVc4RlBYM1VZa29OMjQ2QXBTNytN?= =?utf-8?B?TVI3VmFhaVFKcWVHSURBZTYyT2tkRFF6TmRESkE0YzM1bnVSSG9MN01WUzl5?= =?utf-8?B?b3lxK1UySkExTFhWMU1ySEhILzUyaTJxNFZpbkZOMFMvSC9ROWRuOXYwQW1W?= =?utf-8?B?WEZFVE1FYzFucm9SdWlMUDBzdi9kS1I3UGJHcmhTQzMwYjg1TzBtRkV1bEVY?= =?utf-8?B?N3VCSVV2eE5zM3lMWjZDWXRpMDgwUE1OeTFKVnhpa3JabzliM0d1SlYyM1E0?= =?utf-8?B?YjJxNkRLekZhSmFGM2pEUWZHTVN1M3pOSUFKcktzM0orSlZTRDduWmNZckZz?= =?utf-8?B?NnYyM0Y2NzNQdXlWbDVmcTVURmUrMWQwaUNXQ1E5MjNnWFhJQk9yaHdYY1d1?= =?utf-8?B?SGlmWFlmY3VybzVmOWVJWUdDZVIveWpqN0gvQzVKT0Q4cGpiZlduRHJsUlFX?= =?utf-8?B?QUZrQkhBZWQ0RExSaTRvL29DWnVYbEFCNXhZOTFDT2JaWFhTai9RUCtSWjVB?= =?utf-8?B?MEdWWjlBMDA1ckxxMktHTGJrKzBOSlU2SlFscVJoRzRIbG5LM1Bhay96cEJz?= =?utf-8?B?L0hXVmw1Q2J2RlZRUEtCZiswd21KZ0cwdGliLzBtTCtsSldOeXB2WWowcjVO?= =?utf-8?B?M2o0LzA3UlNndThCenlCOVhDbGxTSFgzWFpZeDB5dEJYZUErVlB6UkRSRElT?= =?utf-8?B?Mnh6NStNWUI2aUVSOUlwd3BPMHEyS1pOUkVvYSt1TjZ0SnBDSXc3QnFta0hx?= =?utf-8?B?Mnp5OUJ2RjdCV0xtTzVzUk52ampRV0N0SUdUeHhFd3ltZUJkOWlNREw0T2d0?= =?utf-8?B?Vmg5ZlhXRnNrcS9zVmxGWnFucVNPd29SOXJXbjZVS0xRa3p3QXZoOFdTT0hy?= =?utf-8?B?ZktmdlVEZXlKR2xZR2JFdVhzR0hybURkZU15aG05eURDSU9iTlcxektubStC?= =?utf-8?B?bmpiUWZDUFM4N1NtL0Y2YmFNUVordUZqUVQ4eXFzUkhTL09sVzJHOVhGUERR?= =?utf-8?B?RjBKSDhqbnN6L3VQOThyNCsrN2NCQWhZM1RvVDFSVkdveWl4K0t2eERuaGJB?= =?utf-8?B?cFdYdFFPNnU0Q2NNWU83VFh6SllOK0pMbTVRbUpUNTdDVGhSdXdXUGtlRjhi?= =?utf-8?B?bTNMRGdGN2YySTRYTlJuL2NiUDN4a3YrUHlablNST0NyeFFuektjcU5wZnFG?= =?utf-8?B?aFRnL1RXc0JkSFU5c0JRSldFdXdQcDhsejBFTE9Hb3oxTFEwekFaY2ZYV2VZ?= =?utf-8?B?bkptUXNwM28yQ0drWFgrRXZUa1NQc3Y3YkJGS2JObktmTHpQYmpsY1ZlQVlv?= =?utf-8?B?dldxM3ppRFRpdmE2Y2RIZmtBSHp3ZnE4UURpUjVZN0hsOVFMMDVBa3RHNisw?= =?utf-8?B?b2ZlT08zcXhOdnRuQTU3S2djbkFnSnd6alBuNVlnZGRXMExKL3gxYllmeXdu?= =?utf-8?B?QXpTd3l1M3VlUkRNOTArbHhXRDV0aTUzbGVEajFQNFA4aUdjYVhhci9YeWFr?= =?utf-8?B?UElnZ2N4MlFXdjluaG9DKzhyWEhuSVVuODhxYkZSa2dvTElQZFJDQ1YreU0x?= =?utf-8?Q?o4khvGjzYuPxy?= x-microsoft-antispam-prvs: x-forefront-prvs: 0951AB0A30 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(39860400002)(366004)(346002)(396003)(136003)(199004)(189003)(5660300002)(82746002)(83716004)(256004)(71200400001)(71190400001)(6916009)(74482002)(93886005)(25786009)(6116002)(4326008)(53936002)(6512007)(6246003)(6436002)(229853002)(3846002)(86362001)(6486002)(486006)(2616005)(476003)(11346002)(305945005)(54906003)(446003)(6506007)(53546011)(76176011)(55236004)(8676002)(81166006)(478600001)(33656002)(14454004)(105586002)(316002)(786003)(7736002)(81156014)(8936002)(106356001)(26005)(66066001)(68736007)(99286004)(97736004)(102836004)(186003)(2906002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5712;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: eANxv3eZhc4cq0ewaxOdQUm11IIc0xyq9FGogFYBA7Nm+Rgcnbi0gcc4q7/tEkSilM7sBB4nYy0Ub4GOh0/GS901HrHSUC01p4vmIvO13DCBfmTEIOjNHjDP6g6fl4BESwimIuDpc7BfyNrbXnc+OavW/peR50Lunh+X53UKr5eUcM24Art63Y5JCf7FiSlrbsed6Ag7Frqf9fag9/7Be5gv/DEEUxxYF/9uz2qs7Rr5+g2LIRz0aJ/IbtJ/w8ckgUQT20Yfn1dfJNG44uQXca3504STNsv6zRO7mh2ERS5hYInUXlJsVAZJmENcC/BP5luS+v/WlYZxWnm9RM8vDJ+QFCNUF9dHJvJx3LQwtaVSEC09E+FATN+FGqDOyj9IvLKt0RFPgtlC/DYhPF2qMnEFhQ+QzPOsgsr1YTq0r+M= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 3735b156-2114-4983-2a17-08d69520b2a5 X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Feb 2019 21:41:38.6693 (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: VI1PR06MB5712 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.124 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 tried to explain in common sense term what is a function? And my answer i= s that it is something you can apply to an element of the domain and you ge= t an element of the codomain. You don=E2=80=99t know how you can inspect th= e function that is all you know. Hence the function type is explained by wh= at you can do with it. That=E2=80=99s coastal. Compare this with natural nu= mbers. A natural number is 0 or the successor of a natural number. You expl= ain how to produce them. That=E2=80=99s data. What is a stream? A stream is= something you can get the head and the tail of. So that is codata as well. Sent from my iPhone > On 17 Feb 2019, at 19:36, Thomas Streicher wrote: >=20 > admittedly, by coinductive I understand terminal coalgebra >=20 > in MLTT even function types are inductive though that's a bit of > cheating in my eyes >=20 > so I must say I don't understand what you mean by codata types > technically >=20 > I know positive and negative polarity in the sense of linear logic people > presumably, that'scloser to what you have in mind >=20 > 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.=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.