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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 93c7ed41 for ; Sun, 17 Feb 2019 09:14:47 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id d25sf12518081otq.2 for ; Sun, 17 Feb 2019 01:14:47 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=WjfxdP4r6jz2zDpy+hJgd4avdeHG++OewWi7/HMD4bk=; b=G6KSCMPdSlMtz/WAhNBrk2lU9MDp6F2d7wE5sYJ/bJw/qRB6dLm8XPcOoN5VxIVAxx n0OFwy7HVv8vEzmM3H6r4nE1bOVieG3nubrhfdlTj2bH/D/kpbuS+evDnSjBlPRGjheu hmtQREPKXc3HLvFWRI8aR6ERuw3XoolX2w1idpg0j6Vip0Xugv/BJYk0XU9rkSHyvfTl SYsfQM5A6cmso71cu0VwKx57Vo4cx9i1d9L978XhW7r1aDP8t2l8jtPxoBmup/UiIxyP /o/IDKO+wGothTEIyM+m8DrHqlttKiiKLjrvrkLi4tV/7289XJcVQUp0Pk01wtwGLfN2 ac1Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=WjfxdP4r6jz2zDpy+hJgd4avdeHG++OewWi7/HMD4bk=; b=bE/zFE9+PWfg+kc4xSrzy3rkyZ3C0HcZg8ATVSUalDfGBUbgGF4VsX0I+VwM8BaajM kgP3YG2CxIzIveR82Njlalle1fJHbWe/aAR9ACozFDQUG/OS+WRQ1tSK418dp6Bedojq UoQw3Nzp3uoi5tFZXgxnamo7Agn/tkW4Pn6YpIQRp2QTaEk90IqM3SqePKFqyVTRedUs yQrJfkH49CtwPRJ1/NVv0vrblYBqElsjWgP+KJTw5Y4xvmqvtidkCoNjyJuwTldXYpbG Y1KTjBkkGKN7r9MUm6065fT4TfHaOj6qVhPxf2tEkkHAjKkYJB+rxZcgbJrpIxMefNsk lqvw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=WjfxdP4r6jz2zDpy+hJgd4avdeHG++OewWi7/HMD4bk=; b=iVKAOXDXF6nwMl40V324Xj9v4nThKLtFZ7yhRXTUy4uO35dwLZVeWsSJB+wkmnCSHV FPla7NvE06XKqUSOA0PTI1WDE2pK3P6Wc1fd8gpchazgkdSdBn2PLD1yfj56B99MUJbe Z/aQjhS7dNN8ZZqzPBMjUzGsX5phCYbLY6Dtd/eqL+PAwjLyIaFpcz1B8ruUEdEMSNwc Jpz+G4xo9me0TCn5XMCVlltzxLtX4P1qEXBOyz8b70OqNDlVylvw8zwFwMleo7Ndw5yd +xbrqQYVGKad14vBd7sh/yhmXe2i/+D93hiUIFYvnuWtHPTyPf08+Yvqd2imxsJnnOcJ y0yA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYbKTI13tE65QDyRKav3/72ITrO24WA5weeeVA+FFQtytVYtEZU ChGauk4d7wya2fg6mlFjVhI= X-Google-Smtp-Source: AHgI3Ia+/IpfqP23ZCaNj8tmGBbTFIiQBATRle8zA/TYH3pnC89RbYsub0749dXzF8izOcVJjAxT6A== X-Received: by 2002:a9d:654f:: with SMTP id q15mr170557otl.6.1550394886331; Sun, 17 Feb 2019 01:14:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bbd6:: with SMTP id l205ls6134272oif.3.gmail; Sun, 17 Feb 2019 01:14:46 -0800 (PST) X-Received: by 2002:aca:eb83:: with SMTP id j125mr72076oih.1.1550394885943; Sun, 17 Feb 2019 01:14:45 -0800 (PST) Date: Sun, 17 Feb 2019 01:14:45 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <0c25a691-82ee-422b-998c-4fe960c102eb@googlegroups.com> In-Reply-To: <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_260_436407209.1550394885340" X-Original-Sender: atmacen@gmail.com 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: , ------=_Part_260_436407209.1550394885340 Content-Type: multipart/alternative; boundary="----=_Part_261_320179550.1550394885340" ------=_Part_261_320179550.1550394885340 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable (Since I've already made such a fuss about Nuprl anyway...) Nuprl has a type of streams (of whatever) up to bisimilarity. That is,=20 bisimilar streams are judgmentally equal. Bisimilarity of bit streams is=20 already undecidable. This is essentially the same problem as extensional=20 equality of functions (nat->bool). I think eta *reduction* of streams would= =20 be OK to throw in, but it won't get you strict extensionality. On Sunday, February 17, 2019 at 2:56:40 AM UTC-5, Thorsten Altenkirch wrote= : > > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on=20 > behalf of Michael Shulman" = =20 > on behalf of shu...@sandiego.edu > wrote:=20 > > However, I don't find it=20 > arbitrary at all: *negative* types have strict eta, while positive=20 > types don't.=20 > > This is a very good point. However Streams are negative types but for=20 > example agda doesn't use eta conversion on them, I think for a good reaso= n.=20 > Actually I am not completely sure whether this is undecidable.=20 > > E.g. the following equation cannot be proven using refl (it can be proven= =20 > in cubical agda btw). The corresponding equation for Sigma types holds=20 > definitionally.=20 > > infix 5 _=E2=88=B7_=20 > > record Stream (A : Set) : Set where=20 > constructor _=E2=88=B7_=20 > coinductive=20 > field=20 > hd : A=20 > tl : Stream A=20 > > open Stream=20 > etaStream : {A : Set}{s : Stream A} =E2=86=92 hd s =E2=88=B7 tl s =E2=89= =A1 s=20 > etaStream =3D {!refl!}=20 > > =EF=BB=BFCCed to the agda list. Maybe somebody can comment on the decidab= ilty=20 > status?=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. ------=_Part_261_320179550.1550394885340 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
(Since I've already made such a fuss about Nuprl anywa= y...)

Nuprl has a type of streams (of whatever) up to bisimilarity. = That is, bisimilar streams are judgmentally equal. Bisimilarity of bit stre= ams is already undecidable. This is essentially the same problem as extensi= onal equality of functions (nat->bool). I think eta *reduction* of strea= ms would be OK to throw in, but it won't get you strict extensionality.=

On Sunday, February 17, 2019 at 2:56:40 AM UTC-5, Thorsten Altenkir= ch wrote:
On 17/02/2019, 01:25,= "= homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> = wrote:

=C2=A0 =C2=A0 However, I don't find it
=C2=A0 =C2=A0 arbitrary at all: *negative* types have strict eta, while= positive
=C2=A0 =C2=A0 types don't.

This is a very good point. However Streams are negative types but for e= xample agda doesn't use eta conversion on them, I think for a good reas= on. Actually I am not completely sure whether this is undecidable.

E.g. the following equation cannot be proven using refl (it can be prov= en in cubical agda btw). The corresponding equation for Sigma types holds d= efinitionally.

infix 5 _=E2=88=B7_

record Stream (A : Set) : Set where
=C2=A0 constructor _=E2=88=B7_
=C2=A0 coinductive
=C2=A0 field
=C2=A0 =C2=A0 hd : A
=C2=A0 =C2=A0 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 decid= abilty status?

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
------=_Part_261_320179550.1550394885340-- ------=_Part_260_436407209.1550394885340--