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-lj1-x23f.google.com (mail-lj1-x23f.google.com [IPv6:2a00:1450:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5b0450b0 for ; Sun, 17 Feb 2019 07:56:42 +0000 (UTC) Received: by mail-lj1-x23f.google.com with SMTP id g12-v6sf3462503lji.3 for ; Sat, 16 Feb 2019 23:56:41 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550390200; cv=pass; d=google.com; s=arc-20160816; b=u899Yvjwn3qZsCTmjrt0Nmq0jceMGuOr3W48LfCrsd6uTlOUMI/VLCQg/P0QbGQHhZ 0wEmMoCiTZok3LrS/FtxSiSZGPA+d5JnMvqBt05i+8m3/XP2vNjqMqlTz7l35kMKKXEn ao0i0AbX4zl99+v0fYXJOIB5SP7KaiKUsETHtfLfNqoWo/Bi9pqGuQmtNgpLCDTZZ9mn nrIhnngscxPF3bjQnRmYmSWEYae5kj5MDJVNM+QCUfLhcQsqbVinmkeNvbXTN/ccwPTR YpoGsB+cQUR6igbjlsfbNm2YJgI8/waN1iq2KwHskyha863uKwjCPA81D7ikwHpaoAOH U9AQ== 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-id: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=kOhIHV4H93pEesdNMnLeAnSye/3LcCT3N/ptnteb6ZM=; b=nUs4auxofiOyMwU+gn3oXSvbSQ6KRocVnW7sTHXJFmIkxOFllJg525LB/Mv7AxFWIT vY1LB31u+v/evdG2JO1Qt61yrb09MBGgODYnCATLYm8GxPlG0ZXKTuDzvZfetrampSsj O3zvGl3xy6ArzsfNCA4MchBu9hvf6/CmGJjDxUl0F5lAuNG5y1u38t3gyWTDFyW5IcMR OFJSsYegcJQq1pV7yL783Jr8aLhcGDVBGOPpTL5tDSBL0H4UwEo2dp2cMN+o/U9OzJ/b VpzXd6vZeqoVuXRRvMaNMEvZJ/tCjGhUYsQPaX0VjML6knZEg+TBOZ06xSeQ91cp5Y9j PM0Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 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 :content-id: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=kOhIHV4H93pEesdNMnLeAnSye/3LcCT3N/ptnteb6ZM=; b=rd7Ia1dpUd3oJ07rI1fmpKwWPuY/hF8JEc34qterLQ8V2MuI5rqNQWOj8UnM7KnqJK Q3bjQNIw+HF68UuxFhtHUQdXZL5FkVKaV5KXzrSQSsVRsXwKnCT/X+bxrIltz4/mNpSP y7gDu8jUDAV0ccsQJiPPMtD9tJkE2cGMJOqmisucbSlHHiQy2HPJpMM8cQ9nQDFtes+6 S9b4ehFW5mIxfRgHqUE2+mEMBSlisaD8iiVZGjaSTLgM9KyoMfa3HENcpD4cIS3eal33 2u9gV5F+E8p1pSXZjCPgE5frs7CAZeHiLqMwICJ64PYpFCA6CYn1Uh/DdCScGlaxfvyx qP4A== 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:content-id: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=kOhIHV4H93pEesdNMnLeAnSye/3LcCT3N/ptnteb6ZM=; b=ILx0oGZRuICKtDMrtBMC1uqlywpYAWbxt/uvnXijlz0bHtMNIWajwyQdZa6EvYDdOV Bf4DNg5aZPFsHIBf9TVugPZB+Aiq/ksKOrszKBmjpaHiqYuay+WXOGwMn5eLJkOn+GR2 gd4jw/NNYKjahUaQy0Qnhl9BS+iuTdR76WJ1MbANNVj9+ERN/c900AsUKaCJGOiiqOSY GSPrdrNvMl6bhrtlNq/pWFpriMXULrqPFMnm3VoUh0nYBB8xWcBu4hECC1Xl170bJ9XR HwuuIwP3bXOjY0uasTvlsAgR/PAjbvgdnJcWPbqCDz2PRtKG2ivtqeGAJtIVsV4oa2L9 K5ZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYF8OrSudzhKQe8CSCUSKKRE7VDUAnlHuB5FaZKZOIdfwVG1b7E dolR6v+5iFuIUvVPFzlwCDQ= X-Google-Smtp-Source: AHgI3IYzAsYRNk0DVJmO2j6yFkoqPpB5ylVFXntgccKR8ADZy7WAg6kGa8x4M1rb5JKJpRXtbDcpqA== X-Received: by 2002:a2e:650f:: with SMTP id z15mr23310ljb.7.1550390200366; Sat, 16 Feb 2019 23:56:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:a786:: with SMTP id q128ls943718lfe.1.gmail; Sat, 16 Feb 2019 23:56:39 -0800 (PST) X-Received: by 2002:ac2:5215:: with SMTP id a21mr986741lfl.5.1550390199626; Sat, 16 Feb 2019 23:56:39 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550390199; cv=none; d=google.com; s=arc-20160816; b=cZ13z6zNzwM8JrU+3AlWy2UjkZb7YV9O1JlOsa+q/P/faYCMnIHp7LbWMeWvQ115id A/gFy4pTnX/7TrmycV9UpGbSRiLczYq++MlnZlQM6aSpxVJjrrsIs7AXYr/Nk5Lr2sVg 2OmwwkYlTFqS2FcYHz7a8RZfmGqqgdILZU4Cj3YBO5BBP8N8icszF+knpiHmQ1y64/sL HztdAQ1maYS7SmS4r3F8kD8TzBMh58R+OxjK55faPUfC1MRLc7KHHhHSMr1JpZ54jRK2 YX42jeVZNLfrFEYsUN41F9tGzuhSQhuGNbMI93T1NR6njhyaFStPwBJeVuSC6LcI/NTt GbWA== 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:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=Paxo6WkfJSxjN+4prijOX7Y8T1YhMvXOGLaNs/TsQdY=; b=oXXSEg//VZ02lfi/fRyYLuQBtesFDr8Pt7QK1r6gs7A8VsWiuMdvl9OIDlUlN7o06L qMesKUzMWShgok/Ri4JQGwbeyVRPwKezFGaQKYeMPqYi0v9iMw3z5tqWwd5zZdlgtURQ 4i2xyggsFOyM/nQRzZud3lXzFRGuW2rRc1f299EUJ4XMRMwkACfML8eHi5Hu9ykBKnUq j3lc8gejV59Znzr1fT2NSctgyOdVBz4pnnbPz9Yd14EqFE7B6Zr9cO07N5IHEBhRo7Sx DnYXxIAJ2SYP+mNqDFzRE9GpzXyHiplgmoogaBqsnXHd6l7Vucaz9S5jmFozMHYGX/qM r53A== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTP id m4si431364lfh.1.2019.02.16.23.56.39 for ; Sat, 16 Feb 2019 23:56:39 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id DCFE32EAA19_C6913B6B for ; Sun, 17 Feb 2019 07:56:38 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 3AD9B311492_C6913B6F for ; Sun, 17 Feb 2019 07:56:38 +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 1gvHJV-0008JC-V6; Sun, 17 Feb 2019 07:56:38 +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; Sun, 17 Feb 2019 07:56:37 +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; Sun, 17 Feb 2019 07:56:37 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) 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; Sun, 17 Feb 2019 07:56:37 +0000 Received: from EUR02-HE1-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; Sun, 17 Feb 2019 07:56:37 +0000 Received: from DB6PR06MB4021.eurprd06.prod.outlook.com (10.168.23.159) by DB6PR06MB3959.eurprd06.prod.outlook.com (10.168.25.20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1622.16; Sun, 17 Feb 2019 07:56:36 +0000 Received: from DB6PR06MB4021.eurprd06.prod.outlook.com ([fe80::8f6:4fb2:4e33:1124]) by DB6PR06MB4021.eurprd06.prod.outlook.com ([fe80::8f6:4fb2:4e33:1124%3]) with mapi id 15.20.1622.018; Sun, 17 Feb 2019 07:56:36 +0000 From: Thorsten Altenkirch To: Michael Shulman , Homotopy Type Theory CC: 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+3Xi0mp7irBTonfqaXSKVkAgBB8egCAAJ4wgIAAbUwA Date: Sun, 17 Feb 2019 07:56:35 +0000 Message-ID: <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> 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-ms-office365-filtering-correlation-id: 68bb8c43-056f-4217-402e-08d694ad70b4 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:DB6PR06MB3959; x-ms-traffictypediagnostic: DB6PR06MB3959: x-microsoft-exchange-diagnostics: =?utf-8?B?MTtEQjZQUjA2TUIzOTU5OzIzOjl1eHlYNUp5ald2d0daeUxzdS9rSHR6RHBB?= =?utf-8?B?bHQwa1BIOTlZSHZaN3BCZFlzSWd5c0hvMHFlSXB6R0VxMlpWazQvOUd4eXAz?= =?utf-8?B?M1hsL3h0cjRxM2s0cmZZaVcvWTYrdjlqamZpRXl4OFJuRmkvYnZHWE5yQlVS?= =?utf-8?B?c0RSVFpJT3dDNmV4WDJOVnF0ZTh1Mm9aWTRNb1BEbkZybmhXVHVCY0daMGRi?= =?utf-8?B?U21oenlGN1BGWUF4ZEtONUhxbENRbTUyRnA1eWo2YjRWUjd5THB1OEZIQ3Iy?= =?utf-8?B?dkNpMnFlVWJGcWtqN2Z5U0toazIxRXVwZVRlK0dUZDdwTXAwRTRpa2RLb3kx?= =?utf-8?B?OVdqZHpyQkMyb2M1d3NuRlBFRHR1UkZuOUtBb2U4RFd3MzlMbUc5a1orYSt1?= =?utf-8?B?enNxVUVUZDducDJBanFZa3lOWVVONDFnNHo1d3lJcnlLY2d2Qm9Id2pualJa?= =?utf-8?B?Z1hzSDByeUxtZFhLSTZCSkRBb2pvMHpqYUh6WXFubnRycnhVcmdUM25iK0ZJ?= =?utf-8?B?NHF1eUtoc3pUUXZER1lOeGk2RERWNTdKUkNYb1V1ZXRZbVQyMVZTWHg2elBM?= =?utf-8?B?bGxsTFExZ2ovaVBidmpxRUtLenU4VUVaWVNaTGpISG5scWQrOFlHWjQrQk9W?= =?utf-8?B?QzNVSEhTVGpVQWQzSmorNDZBUndSRnJDUFByS2JrTi9GQ0UxSndBWEp4Vktt?= =?utf-8?B?UTRJZXNSdDF5WlNSQ2NsSjh2Z0d3L0hVeVFSa0tPZHl5YlhJUXJHd3pnQ2Iz?= =?utf-8?B?Yk9MRFN4a3pEd3R4RDIwZmFlUTViVTE0c0llZlg3ZVZUNnc2cWtxOC9oQzM4?= =?utf-8?B?UkdMQTYzd3F6ay9FdFY5L2RKdU5FZXNjV3V5Y0h5RVZnSkFQWUpMcGVobGxO?= =?utf-8?B?M2tuWFR6ZWR0QWFCbVIxMmZmNllmcUFlYW1tbkFOcisvSXRjR0VLMTcvbGNr?= =?utf-8?B?MnNJcnVjeVkwL1FzbHJidDB4SkJ1QlN6VjhuOWFMTzlxV2ZXUERscXIvZkxB?= =?utf-8?B?Vmc5NTdTc0V2dnlrNHZsVm44bjNwUC8rbHprVFc5eStDd1h5NVNtS2RxZG9T?= =?utf-8?B?dHBpNjZJSHVGMjNWUVZiNFBQVTMrTy9QeVUxUnEraC9LWTNoL3RDUnNnYmxY?= =?utf-8?B?STA3ZzhDdW9xZkJqV2dUUGpwc1VSWm9UYnNramFhNjRkZGdEL3JIZkQxb096?= =?utf-8?B?L1k3L1hoVDVKQTZDR21yMWxnejBXWlEwNHVOMkM0K2dEUlRqSW8zUFpiTm1l?= =?utf-8?B?ajgwVUMzN3dVRTlPcE96NUZYb2tRYkNOd0k0ZWFhRTI3eWRTWHNmWDZXZEtC?= =?utf-8?B?MDRNSGkvNk1xcmhWbFhlVXZqQmRKNjhiQmxWTlVPN2ZJWmhXYmpPTDBCc3Rx?= =?utf-8?B?eXpnNXg2YTl5czBqZCtOeTZpN1dmSlVlOUZQR09Sc082aW1hMW82U3hrdktY?= =?utf-8?B?Y29hclBDbDU2MWNTMXlYZ1ExRVhFeXdQOTZGY2RSRHkvczVzaGk4NzJ0Q3dp?= =?utf-8?B?M1VqZm1hODNaQk8rQlhkRklRKzJ5aFRyeXBNcWZFK3ZlWnZ3aEhnVlI0Ykt3?= =?utf-8?B?S0FobzFGM1ZrcVgxa1p5L0l2c0hSYldHWWI5N2lNZ0s1Sm9wWUd4ZjltdXRB?= =?utf-8?B?TFg0dXJrdUljeWwvVFJROWxHU2k5Rnh2bWFsZkNrUXRUcjNrbXBQOCs2UVZO?= =?utf-8?B?RWxoVUI5WkZEZVlSejVHcEwwY05BYWVibDh5ZmFTWFZiSnRMUnpMdm5Ud05p?= =?utf-8?B?VWZyb1N1RGpRZ1NBM2hxc1lUc2N3RnlMQmg3WlByTVMrcVY3aTJiY2xLbFIy?= =?utf-8?B?NGxsVTFza3J4aGJDNFBFeVdwNmJSajJrQVAwWFpKNGZTamhvbE5BMHU3R3Qy?= =?utf-8?Q?MxvMRunzpE52Fj2dkAxxg0Td9FYTF+dW?= x-microsoft-antispam-prvs: x-forefront-prvs: 0951AB0A30 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(346002)(366004)(136003)(39860400002)(396003)(189003)(199004)(14454004)(25786009)(33656002)(186003)(68736007)(6436002)(6512007)(9686003)(74482002)(8936002)(66066001)(26005)(81166006)(81156014)(3846002)(8676002)(6116002)(6486002)(256004)(53936002)(99286004)(2171002)(2906002)(83716004)(6246003)(71190400001)(76176011)(446003)(5660300002)(36756003)(486006)(11346002)(58126008)(316002)(476003)(71200400001)(786003)(110136005)(4744005)(93886005)(106356001)(55236004)(229853002)(105586002)(4326008)(102836004)(305945005)(478600001)(7736002)(86362001)(53546011)(97736004)(82746002)(6506007)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB6PR06MB3959;H:DB6PR06MB4021.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: 6Lv4/U4Nge21n5ofBzLPVcnbFiqbRU47wqjALLvIDSpYFun21cr0XUA+7f5PkiZRw8WOaaVH3AnFBbSSZVVgsUe1xgX6xXVLytdOHaxCVjJph98DFF6SPI04XiBosnE8MZ2pqtzWCWxmJzbqiyRo5Wv/sqKvbFr1hXWyBPah4Q9/98+VsWbJF4DeSqnt5TvnbJnWsOyXJ1NOqolnoUez4AoZdr6Y/vrQCh6w3NMH+CCgTx2+HOYX22GFvrpbjm2I8AorGWUcb5gC1snKpIglpwlC9KUVn+VPX0PDD4X9JSMtQ7/TbAxmMkes/YNntEIl9hgEgXTPwc3/fTjOiUqDQvKnnUOXMBp+0V+mmykT5YVBXV15w5thpGezMSch+w1LmnZ8fdlGzU8ZpVe+xjHEcA6LhJSJxLGm+Q88MwVGNHE= Content-Type: text/plain; charset="UTF-8" Content-ID: <83717EFEF2A93B4DA8E8E6F012717486@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 68bb8c43-056f-4217-402e-08d694ad70b4 X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Feb 2019 07:56:36.0037 (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: DB6PR06MB3959 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.125 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: , On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Mic= hael Shulman" wrote: However, I don't find it arbitrary at all: *negative* types have strict eta, while positive types don't. This is a very good point. However Streams are negative types but for examp= le agda doesn't use eta conversion on them, I think for a good reason. Actu= ally I am not completely sure whether this is undecidable. E.g. the following equation cannot be proven using refl (it can be proven i= n cubical agda btw). The corresponding equation for Sigma types holds defin= itionally. infix 5 _=E2=88=B7_ record Stream (A : Set) : Set where constructor _=E2=88=B7_ coinductive field hd : A tl : Stream A open Stream etaStream : {A : Set}{s : Stream A} =E2=86=92 hd s =E2=88=B7 tl s =E2=89=A1= s etaStream =3D {!refl!} =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the decidabil= ty status? 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.