From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.105.6 with SMTP id e6mr450019ywc.8.1473112271631; Mon, 05 Sep 2016 14:51:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.20.97 with SMTP id h88ls10022431oth.6.gmail; Mon, 05 Sep 2016 14:51:11 -0700 (PDT) X-Received: by 10.157.48.66 with SMTP id w2mr2043200otd.46.1473112270998; Mon, 05 Sep 2016 14:51:10 -0700 (PDT) Return-Path: Received: from smtp03.srv.cs.cmu.edu (smtp03.srv.cs.cmu.edu. [128.2.217.202]) by gmr-mx.google.com with ESMTPS id u193si1596904ywf.6.2016.09.05.14.51.10 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 05 Sep 2016 14:51:10 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.202 as permitted sender) client-ip=128.2.217.202; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.202 as permitted sender) smtp.mailfrom=d...@cs.cmu.edu; dmarc=fail (p=NONE dis=NONE) header.from=cmu.edu Received-SPF: none (cs.cmu.edu: No applicable sender policy available) receiver=smtp03.srv.cs.cmu.edu; identity=mailfrom; envelope-from="d...@cs.cmu.edu"; helo="[192.168.144.101]"; client-ip=73.142.151.116 Received: from [192.168.144.101] (c-73-142-151-116.hsd1.ct.comcast.net [73.142.151.116]) (authenticated bits=0) by smtp03.srv.cs.cmu.edu (8.13.6/8.13.6) with ESMTP id u85Lp7UK026001 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Mon, 5 Sep 2016 17:51:08 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] A puzzle about "univalent equality" From: Dan Licata In-Reply-To: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> Date: Mon, 5 Sep 2016 17:51:06 -0400 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> To: Andrew Polonsky X-Mailer: Apple Mail (2.3124) X-Scanned-By: mimedefang-cmuscs on 128.2.217.202 yes, see https://github.com/dlicata335/hott-agda/blob/master/misc/Andrew.ag= da Using the notation=20 e1 : (x : Bool) =E2=86=92 (f True x) =3D=3D (g True x) e1 True =3D id e1 False =3D id eh : (x : _) =E2=86=92 f x =3D=3D g x eh True =3D =CE=BB=E2=89=83 e1 eh False =3D =CE=BB=E2=89=83 (=CE=BB { True =E2=86=92 id ; False =E2=86=92 = id }) e : f =3D=3D g e =3D =CE=BB=E2=89=83 eh the steps are goal : fst Y =3D=3D True goal =3D fst Y = =E2=89=83=E2=8C=A9 ... =E2=8C=AA=20 transport (=CE=BB u =E2=86=92 Phi (u True True)) e (fst X) = =E2=89=83=E2=8C=A9 ... =E2=8C=AA=20 transport Phi (ap (=CE=BB u =E2=86=92 u True True) e) (fst X) = =E2=89=83=E2=8C=A9 ... =E2=8C=AA=20 transport Phi (ap (=CE=BB f=E2=82=81 =E2=86=92 f=E2=82=81 True) (ap = (=CE=BB f=E2=82=81 =E2=86=92 f=E2=82=81 True) e)) (fst X) =E2=89=83=E2=8C= =A9 ... =E2=8C=AA=20 transport Phi (ap (=CE=BB f=E2=82=81 =E2=86=92 f=E2=82=81 True) (=CE= =BB=E2=89=83 e1)) (fst X) =E2=89=83=E2=8C=A9 ... =E2=8C=AA= =20 True =E2=88=8E I would be very surprised if there was something like this that was not pro= vable in "book HoTT=E2=80=9D. =20 -Dan > On Sep 5, 2016, at 12:54 PM, Andrew Polonsky wrote= : >=20 > Hi, >=20 > There is a common understanding that the "right" concept of equality in M= artin-Lof type theory is not the intensional identity type, but is a differ= ent notion of equality, which is extensional. The adjunction of the unival= ence axiom to standard MLTT makes the identity type behave like this "inten= ded" equality --- but it breaks the computational edifice of type theory. >=20 > More precisely, this "Hott book" approach only nails down the concept of = equality with respect to its *logical properties* --- the things you can pr= ove about it. But not its actual computational behavior. >=20 > Since computational behavior can often be "seen" on the logical level, I = am trying to get a better understanding of the sense in which this "Hott bo= ok" equality type is really (in)complete. How would a "truly computational= " equality type be different from it? (Other than satisfying canonicity, e= tc.) >=20 > One precise example is that, for the "right" notion of equality, the equi= valences characterizing path types of standard type constructors proved in = Chapter 2 of the book could perhaps hold definitionally. (The theorems pro= ved there are thus "seeing" these equalities on the logical level.) >=20 > I tried to look for a more interesting example, and came up with the foll= owing puzzle. >=20 > f, g : Bool -> Bool -> Bool > f x y =3D if x then y else ff > g x y =3D if y then x else ff >=20 > e : f =3D g > e =3D FE(...) [using UA to get Function Extensionality] >=20 > Phi : Bool -> Type > Phi tt =3D Bool > Phi ff =3D Unit >=20 > Psi : (Bool->Bool->Bool)->Type > Psi =3D \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff) >=20 > X : Psi f > X =3D (tt,*,*,*) >=20 > Y : Psi g > Y =3D subst Psi e X >=20 > QUESTION. > Can we prove, in "book Hott", that "proj1 Y =3D tt" is inhabited? >=20 > Cheers! > Andrew >=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= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.