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-ed1-x53a.google.com (mail-ed1-x53a.google.com [IPv6:2a00:1450:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 35d2c71b for ; Sun, 17 Feb 2019 14:22:26 +0000 (UTC) Received: by mail-ed1-x53a.google.com with SMTP id u19sf5913893eds.12 for ; Sun, 17 Feb 2019 06:22:26 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550413345; cv=pass; d=google.com; s=arc-20160816; b=nQaQuPGaqnPOH1or8SI5TcSMoT3yt/vj6wQLW1HQGlHNNuEyCSTMy/w+c0ATo7DHSX AW5XCmR4DvRxjT6EDEBZ5DL3Ungbx+SKQzeEypCZNgF43r4GRwk5LTOefEbzf1ff8x43 EbHjnwCX5GMwSa9SJg6BhPxzynP+16v7i0txJI5639XsYpHTeSHUsJZMXuvWHGodqFGg LOLw+buzwoMfxMkGTh7XuYx0UtmvllkhryP4Ssc+Y02Xaok8lR7kYvXh+zrnGwYKAqmk xf0RKWibrhZagr089SB8fRrg/uRBC6fcWhVo9idIqFGg1CrTsH8bj5SN8BV+O3QEdcvG Y6yw== 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:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:sender:dkim-signature; bh=FT4BogQ9vKjtHBSHLC2e+fpC2XRTWtXvAvGDGh1V5Gc=; b=CfQLWaKJcCi6OfsBg5B54J8R6z/yRQ7geL/BK4ngxA1yT5RcKSXjva7WMDYEoIQrmh VINUNS61JtzaKjG4cxtx3iVU7QfwDnhglGuFCsECeeAwU1aTXhsyn93KN11+wrcyXzUf FsHvRylA6svZYef0FkHWv+XZKdV74vAXfyql1G4Wnwc29W99Y4bExpkJ/99mkVYLGPHm LTtFX1m7lUuZGFVub5hO/45sm+sh2D4At1QV9ioatAnJs2wJDZmR5/IcqCtxXIhAbxwq UNoYoKWhm14thZNnQtwZfB0wUCJF824IAfv7+vHrX6UrE+hVmPXCnXom3niCKFghnwZJ qulQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of andreas.abel@ifi.lmu.de designates 141.84.214.246 as permitted sender) smtp.mailfrom=andreas.abel@ifi.lmu.de DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=FT4BogQ9vKjtHBSHLC2e+fpC2XRTWtXvAvGDGh1V5Gc=; b=EayLht7NjJ0lTgvxUC9sRBOiR9kcD+jsS5oSWTOUmybs+c4SdniFlt8RisXKjIeK3q AdXLyB/9upDKfRwPA88cIN61d1Y/o4KXGioXpheuBCKZmfr6KQGFJqnJE0qYSvzIf6w3 PyH/2PU4/EM8zoE2Zio+Vyia3XbO8USynGmHA/E2X5FJPS5vEXAZkYR7Xm2ozZwhPCKA BUbHFcu6Ozzj38281xWhOsLLMC1+nUaiUcBofwA7q0OQZAsmljLNRcyfDbQJxaklkhfT Ne4KbqQ7AulVI/epA4LAbI2cl53VK1BkRIb42UQfDNR2aXi2gP5UZYRWxwmnLrz8fQcT xzbg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:cc:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding: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=FT4BogQ9vKjtHBSHLC2e+fpC2XRTWtXvAvGDGh1V5Gc=; b=arfj+jLpFP08F9Y5PW4HW/UwhbQA65MqxAM8leyCDhvpkLdTwG3zLOe8luhavd1CBm SljVfTj1QY+fliD/XzYB9QupjIAD5po8VmrpSeOvNbMmsIUlibzyBgSygVrvprh6Dg3k ir4kNS0owtpRMw8PmNlJh6vsoJl5y17zlhDV4c7NN6hSvktqfQakXkw/ukeQpGkfy3oL AKrxViGPT43rfnTDvqAbg0M4rvBKejMlex8sA/ROkT5B6DIK5Q4MmRXA9SX9Agxa8+MB T/LzkexxJ3lqGDdbUFL69zG93aaOgXkTK8PzLDO1HnYizFvuQLub4hR1uPUtYP/3TLNq RG+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub0LuXHNaZAFDPglQLKHt9NY7FIO2JbWXCzC0YgkiuPLy95JLdU 6eD8t687uu0PlYxA5nYLJI4= X-Google-Smtp-Source: AHgI3Ib5b9LeFnt7TLdoCXDsKbwW3BpHBCYa2Y3gXTGvaqQC/HCp52OMLeG6jYxN4zi9sW2ZTsdwSQ== X-Received: by 2002:a50:986f:: with SMTP id h44mr61616edb.2.1550413345708; Sun, 17 Feb 2019 06:22:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:bb22:: with SMTP id y31ls2421610ede.6.gmail; Sun, 17 Feb 2019 06:22:25 -0800 (PST) X-Received: by 2002:a50:aa70:: with SMTP id p45mr1060884edc.6.1550413345149; Sun, 17 Feb 2019 06:22:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550413345; cv=none; d=google.com; s=arc-20160816; b=JjIL6FGeZseZ3fUJtNinPZiQSIz6SYUNrNFyy7jBXItBN554zcXhNW9kWcCz2r8N6z UWuYeN9BMjhZQjZkxaMFpx1Uoytcp5GduhEzMoOum0lQlSvdMoyRPCYWoPzlCrWqRq1o GEiyN94tpZlJK+BTeb4Bt7ioUwe6GiDf2Er2QDPFbqJldWItfJ/KHUqS4UQrjYOPiSAy OUyZiWeeYGt0SXP86LsXV/O7t0V0XfIcok/nnnm/82HuIly2cZKgDj1aTPEmvW4mxmY/ tw99TxNDgnKttoABV4SVqUjfXgODI5r9Y3Ur3KMVo7ad0dG0VBrGTxlB9ntiS7L/wc6S CbZQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject; bh=ksKoyHq4EJ4Wk4sQTz/NhpBygVZci/hMgfU1zvUjsdg=; b=J+ppozzI0lylFfM/O8ydcY2X4iIIdEUgn+iTVHcnb5IuKyF+uhEfcFB933dfyVycy9 oI5tow7Ll1D14qPhUev14mNAjtIx1xe5MDCP3ipMYgA6BcAt6uUxhY+DqdGMYNhRHcWC 5YkkWEoI49YFtVG6SX4IE3HXZFtag0HxS1EW07f7exHDvQch48AnUS1kS1OIl6tERaeL YhS/7PkSMoKvFF8jOaADkrvpTk5E3i+W1q/LYMC/2q/y44htZ08hWONI+5gfjiX5C9sz zwh7LAam1oHpOG0dE6bB0a7ISIt8+87QLgotfL5wRZYaefA4SAhrrcrx7UJuypBKH664 5kLA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of andreas.abel@ifi.lmu.de designates 141.84.214.246 as permitted sender) smtp.mailfrom=andreas.abel@ifi.lmu.de Received: from smtpout11.ifi.lmu.de (smtpout11.ifi.lmu.de. [141.84.214.246]) by gmr-mx.google.com with ESMTPS id c8si265744edf.4.2019.02.17.06.22.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 06:22:25 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of andreas.abel@ifi.lmu.de designates 141.84.214.246 as permitted sender) client-ip=141.84.214.246; Received: from Andreass-MBP.lan (90-231-119-119-no64.tbcn.telia.com [90.231.119.119]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) (Authenticated sender: abel.andreas.tcs) by smtpin1.ifi.lmu.de (Postfix) with ESMTPSA id 3EB671D6454; Sun, 17 Feb 2019 15:22:24 +0100 (CET) Subject: Re: [Agda] [HoTT] Re: Why do we need judgmental equality? To: Thorsten Altenkirch , Michael Shulman , Homotopy Type Theory Cc: agda list References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> From: Andreas Abel Message-ID: Date: Sun, 17 Feb 2019 15:22:23 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:60.0) Gecko/20100101 Thunderbird/60.5.0 MIME-Version: 1.0 In-Reply-To: <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: andreas.abel@ifi.lmu.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of andreas.abel@ifi.lmu.de designates 141.84.214.246 as permitted sender) smtp.mailfrom=andreas.abel@ifi.lmu.de 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: , > =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the decida= bilty=20 status? Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types Talk given at CMCS'18 Thessaloniki, Greece, 15 April 2018 =20 http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedings= CMCS18.pdf On 2019-02-17 08:56, Thorsten Altenkirch wrote: > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of M= ichael Shulman" wrote: >=20 > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. >=20 > This is a very good point. However Streams are negative types but for exa= mple agda doesn't use eta conversion on them, I think for a good reason. Ac= tually I am not completely sure whether this is undecidable. >=20 > E.g. the following equation cannot be proven using refl (it can be proven= in cubical agda btw). The corresponding equation for Sigma types holds def= initionally. >=20 > infix 5 _=E2=88=B7_ >=20 > record Stream (A : Set) : Set where > constructor _=E2=88=B7_ > coinductive > field > hd : A > tl : Stream A >=20 > 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!} >=20 > =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the decidab= ilty status? >=20 >=20 >=20 >=20 > 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 > where permitted by law. >=20 >=20 >=20 >=20 > _______________________________________________ > Agda mailing list > Agda@lists.chalmers.se > https://lists.chalmers.se/mailman/listinfo/agda >=20 --=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.