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-pg1-x53b.google.com (mail-pg1-x53b.google.com [IPv6:2607:f8b0:4864:20::53b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0c07a935 for ; Sun, 17 Feb 2019 09:19:02 +0000 (UTC) Received: by mail-pg1-x53b.google.com with SMTP id e5sf9814187pgc.16 for ; Sun, 17 Feb 2019 01:19:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550395141; cv=pass; d=google.com; s=arc-20160816; b=srcW8U8Rv5A+UvmBonv4NmwNRhzgxPPe2Sa4SqfoDVfqhZ6kkLsbWTX7BpUfB8oI1A ygsshB/MRF9cHqK633hP+sfqSctKr2AMDounR3HZdyaGW6bR9gx66jeptbqMNwpGzBMK 9Pkhz0KA8AZT33r5mdp7Oat7sO9I4WGjv8Bn82gOTjsClsep4EvGXxQkHGsoXXu5/k06 tXD1NCTfofI6aX2+L9UkF0woayVUWLvSftaFT6NM4+cLU+e/pBMAvMdhSC6I5TK0URDM 0U1s8lXi8oj7C36RajnIsaoNXHiQ2mwnwpS73UNIy1XwnIFTboL0kb2z6VI/z1y0yb4A uqYA== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=yBXH6Cts2sIQ3Xf3p39EIZFVGREwKelRbBN/5or9fuI=; b=wbR3BqTRMI0E6QrJ1EzJiI0WFr3kVk/+/JzesFDwsNvA+e+Pnz0HWp2foCeoIzY/++ F9YuwXPkksWlM5xgqSrbngPoPb0f/0CHnZadtz571Nra7lJzKaOjZgTu0g83L8/2waT7 6zYOaARCEFDDjWIuFuqP/60BNlV4/LknJdxelkm3KbS8+D+/8+qf1vrqjAQn3iVvaN49 FgrI1cW8LNqLG/p+7c1m/2WHBZG3K9Arp5mNl1TUIbPYqbJdrFYbk6/pZx9wZGIqJl9l egyw0lqNbkGb/VCSD8tdlU9VvfSCRMGTjfNjFbi6Af5aTFH42Ib8DuNTZvFy5cPNmu/t CqjA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=F+2iRSBa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=yBXH6Cts2sIQ3Xf3p39EIZFVGREwKelRbBN/5or9fuI=; b=dOerXmBdr0r97YUpWCm3m6F8QpBo1rB4lA3UdHcXTvQYJhtZ2PE+E1V6FbAUtYSLWH 5p9QWN4E2ZK/cM7RMeqJnmWFNYCmuj18nQbHB862szGk02r3QcWu5begb6jXBub51MDr MUAwflJJentZ/IDC/o8JjyP5UcSpcqIsFfXP3ORvEwtIi9lvTsE8ZJvr9zO53Z6Uhvum maEria7rie6/RZIHxdJyawKMUZla6/ZgptQpbmXcVobZzYmc5llLc2lndKfy8voZTBtM XMJ921Ik9Q+tQWXfwVkkzzuSLKKN0Q9Imxe7L7nIemiKx5hYv95R9Sf1AYf2xYqScOtc EoUQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=yBXH6Cts2sIQ3Xf3p39EIZFVGREwKelRbBN/5or9fuI=; b=tHgVGZfgBwvnCmOpw9mcbZd///E7w+z5cHRqcAiTskG05V+WDisggLe3m3ZZ5AMjpP P8dmU8+8jXhHdHa2/uwkClDhU8uSuwddIQSYGLypHu8s+TW1NHiscLkBqV0008PR7FCv 2Qxjx9u4jPz/prMEZXV/6SaMAvZ5K3O+aD23ASM6T6ADlMvOsmBmCizx9MX+jpDix/Ey op+G021ayLW30sOtyikFGPO/oGt4gUsXoZq+ISDM3AwDcGG76vib0GmvCGU6t1tpnmsX sJl0hmFPMcOH1/fd9FxZsJeltwLdkK09e2Ba73gmk4cVgi49haMmFGhYQ6+RfaN7x1qx OuZA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaQBFsdbxNo39vcBEE0IV/bosKPNyrcVa4NvnM9q7pGFcC/9gKi VH/WPjLFVoQ7Y5U/lRT4jPA= X-Google-Smtp-Source: AHgI3IZi+B5pxn72/24qUMEYL0RwR2qbnymkZWUK2/UNRcI/CIJzmuZ7J6zV6SlVHejCSknGBRN2Jw== X-Received: by 2002:a62:418b:: with SMTP id g11mr68746pfd.6.1550395140817; Sun, 17 Feb 2019 01:19:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:5958:: with SMTP id n85ls4533968pfb.3.gmail; Sun, 17 Feb 2019 01:19:00 -0800 (PST) X-Received: by 2002:a63:66c5:: with SMTP id a188mr6610994pgc.108.1550395140447; Sun, 17 Feb 2019 01:19:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550395140; cv=none; d=google.com; s=arc-20160816; b=lT14lPlyDqlxxl80oH9RApGJiK1r7Fmvc10YqD1NsOaoWFuCnZMaF2qmmUb5C9wa3e cHoVwhkGpYenqWPEBIFLjez8hjBH3Xf3JlY1krAV0E0UXwq7dW/RSF5UV92fGgNQW8mm FH9F/n6sPr8MhxqX0vHnQjMR0yvVa4yzkdsNgKBOmycH9QhJx09EBWpzENAmQ6wHMSl9 Swh4jTEBYmqteuPsKOJR/dCAbey1o0qii+sJ/P2sRRBSq6SzlGaFKwMxlnhvIIoHcOMu tb74axcM2r+lxnM+snTwkmw63ArZ6yaRauMiPFLgLFXdSuj25yEJZ3TJN2I2sFVW+V64 FMWQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=34jBhr4Gqbz+XufpW4+rxLS56EIg6Zhv+/PKGgV3+Lc=; b=SX+yZkm7eFEeSvf4RIs/FAS4v8PdOdkxutYYmQ5axEFKy6mLQsCvC4K/s/lu1HiwyO x8U/VHA1MEQlE8s1zWkSlNC9t9nzgIWgWe4EMHPYrFS7QOpRXMnRE8KebPz/ccevSaDW Mme+Qw4GEo7lsfAwZGykkzP2c2btmPOFMMrXeypgEna5zuySZP4PXZG2xahpBSl9vOwF B1zueDUN4G7DJb1yH4SH86G+L31N2jyA+kVGOC8rVoNzURXRYyix7BVxdZnj0Lps/kG+ tEeNJhluUHb+HDlLbi9uddFEE+OyYZWk3RzCUjii7SJ2oMwcdgHoc2wkl0jz/xLaZP8U nVgg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=F+2iRSBa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2e.google.com (mail-yw1-xc2e.google.com. [2607:f8b0:4864:20::c2e]) by gmr-mx.google.com with ESMTPS id q19si636619plr.4.2019.02.17.01.19.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 01:19:00 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) client-ip=2607:f8b0:4864:20::c2e; Received: by mail-yw1-xc2e.google.com with SMTP id k14so5348277ywe.4 for ; Sun, 17 Feb 2019 01:19:00 -0800 (PST) X-Received: by 2002:a0d:c4c2:: with SMTP id g185mr14159727ywd.31.1550395139470; Sun, 17 Feb 2019 01:18:59 -0800 (PST) Received: from mail-yw1-f49.google.com (mail-yw1-f49.google.com. [209.85.161.49]) by smtp.gmail.com with ESMTPSA id h62sm3946199ywe.100.2019.02.17.01.18.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 01:18:58 -0800 (PST) Received: by mail-yw1-f49.google.com with SMTP id u200so5331317ywu.10 for ; Sun, 17 Feb 2019 01:18:58 -0800 (PST) X-Received: by 2002:a81:4b45:: with SMTP id y66mr14173617ywa.421.1550395138290; Sun, 17 Feb 2019 01:18:58 -0800 (PST) MIME-Version: 1.0 References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> In-Reply-To: <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> From: Michael Shulman Date: Sun, 17 Feb 2019 01:18:46 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Thorsten Altenkirch Cc: Homotopy Type Theory , agda list Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=F+2iRSBa; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Well, I'm not really convinced that coinductive types should be treated as basic type formers, rather than simply constructed out of inductive types and extensional functions. For one thing, I have no idea how to construct coinductive types as basic type formers in homotopical models. I think the issue that you raise, Thorsten, could be regarded as another argument against treating them basically, or at least against regarding them as really "negative" in the same way that Pis and (negative) Sigmas are. And as for adding random extra strict equalities pertaining certain positive types that happen to hold in some particular model, Matt, I would say similarly that the general perspective gives yet another reason why you shouldn't do that. (-: But the real point is that the general perspective I was proposing doesn't claim to be the *only* way to do things; obviously it isn't. It's just a non-arbitrary "baseline" that is consistent and makes sense and matches a common core of equalities used in many type theories, so that when you deviate from it you're aware that you're being deviant. (-: On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch wrote: > > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of M= ichael 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 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. > > 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. > > 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 decidab= ilty 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. > > 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. --=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.