From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.154.1 with SMTP id c1mr2652879wme.2.1473111630943; Mon, 05 Sep 2016 14:40:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.77.6 with SMTP id a6ls461179lfb.42.gmail; Mon, 05 Sep 2016 14:40:30 -0700 (PDT) X-Received: by 10.25.20.69 with SMTP id k66mr1735049lfi.3.1473111630190; Mon, 05 Sep 2016 14:40:30 -0700 (PDT) Return-Path: Received: from mail-lf0-x22f.google.com (mail-lf0-x22f.google.com. [2a00:1450:4010:c07::22f]) by gmr-mx.google.com with ESMTPS id e21si1115561wmc.2.2016.09.05.14.40.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 05 Sep 2016 14:40:30 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4010:c07::22f is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2a00:1450:4010:c07::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-lf0-x22f.google.com with SMTP id h127so30463064lfh.0 for ; Mon, 05 Sep 2016 14:40:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=sfqBvyJx4cN7xZ/JrCH2EEViXhu72ukbcCSpoJ7/OL8=; b=wDJhtH5sJfb14b6uzuIkMPiVnICm1x6Ux+RMZ41qbsitloCITBmABeNMRe39Wit4Y0 VXNoSgknhrdb9Pm+zmNb4Sgv86f3ce9SVgCtqRYRIOzfoJEYLb2TqukVFGnG/G8r7ABC e+7kiju0p8A7kzdz094bVLc7g3y2L9AR9FlHRvHVE9x6vZVf0BMz39FFsJfnq9s0TOUs KVo56MqOZgW72/QgsmIqYoqdsvzsIewKBA3+VTOiT3zU3uV0knDT6cFOh/I+ttijBu24 /DuoLLOBVCgJAkNqnrJDcze3RTdfgXw3y1p3ZGBBrap+jQAuaT3vZNReD25kA1v2Kcwx SICw== X-Gm-Message-State: AE9vXwM5G+67PPLWjPjFF6bb2v4ejy3B53jKRZ1RFSsVSo8beu4WNk/WSbjDN8Vo5N7Yk5on X-Received: by 10.25.196.3 with SMTP id u3mr2240330lff.164.1473111629419; Mon, 05 Sep 2016 14:40:29 -0700 (PDT) Return-Path: Received: from mail-lf0-f47.google.com (mail-lf0-f47.google.com. [209.85.215.47]) by smtp.gmail.com with ESMTPSA id 17sm1359598ljj.47.2016.09.05.14.40.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 05 Sep 2016 14:40:28 -0700 (PDT) Received: by mail-lf0-f47.google.com with SMTP id g62so133756778lfe.3 for ; Mon, 05 Sep 2016 14:40:28 -0700 (PDT) X-Received: by 10.25.143.137 with SMTP id r131mr11161395lfd.165.1473111627676; Mon, 05 Sep 2016 14:40:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Mon, 5 Sep 2016 14:40:06 -0700 (PDT) In-Reply-To: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> From: Michael Shulman Date: Mon, 5 Sep 2016 14:40:06 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A puzzle about "univalent equality" To: Andrew Polonsky Cc: Homotopy Type Theory Content-Type: multipart/mixed; boundary=001a114022444857fe053bc987a8 --001a114022444857fe053bc987a8 Content-Type: text/plain; charset=UTF-8 I assume that in the definition of Psi you meant to write "Phi (u tt tt)" and so on, since "u tt tt" is not a type, and otherwise Phi wouldn't be used anywhere. With this modification the answer is yes; see attached code. On Mon, Sep 5, 2016 at 9:54 AM, Andrew Polonsky wrote: > Hi, > > There is a common understanding that the "right" concept of equality in > Martin-Lof type theory is not the intensional identity type, but is a > different notion of equality, which is extensional. The adjunction of the > univalence axiom to standard MLTT makes the identity type behave like this > "intended" equality --- but it breaks the computational edifice of type > theory. > > More precisely, this "Hott book" approach only nails down the concept of > equality with respect to its *logical properties* --- the things you can > prove about it. But not its actual computational behavior. > > 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 book" > equality type is really (in)complete. How would a "truly computational" > equality type be different from it? (Other than satisfying canonicity, > etc.) > > One precise example is that, for the "right" notion of equality, the > equivalences characterizing path types of standard type constructors proved > in Chapter 2 of the book could perhaps hold definitionally. (The theorems > proved there are thus "seeing" these equalities on the logical level.) > > I tried to look for a more interesting example, and came up with the > following puzzle. > > f, g : Bool -> Bool -> Bool > f x y = if x then y else ff > g x y = if y then x else ff > > e : f = g > e = FE(...) [using UA to get Function Extensionality] > > Phi : Bool -> Type > Phi tt = Bool > Phi ff = Unit > > Psi : (Bool->Bool->Bool)->Type > Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff) > > X : Psi f > X = (tt,*,*,*) > > Y : Psi g > Y = subst Psi e X > > QUESTION. > Can we prove, in "book Hott", that "proj1 Y = tt" is inhabited? > > Cheers! > Andrew > > -- > 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. --001a114022444857fe053bc987a8 Content-Type: text/x-verilog; charset=US-ASCII; name="Puzzle.v" Content-Disposition: attachment; filename="Puzzle.v" Content-Transfer-Encoding: base64 X-Attachment-Id: f_isqkm26l0 UmVxdWlyZSBJbXBvcnQgSG9UVCBGdW5leHRBeGlvbS4KCkRlZmluaXRpb24gZiA6IEJvb2wgLT4g Qm9vbCAtPiBCb29sIDo9CiAgZnVuIHggeSA9PiBpZiB4IHRoZW4geSBlbHNlIGZhbHNlLgoKRGVm aW5pdGlvbiBnIDogQm9vbCAtPiBCb29sIC0+IEJvb2wgOj0KICBmdW4geCB5ID0+IGlmIHkgdGhl biB4IGVsc2UgZmFsc2UuCgpEZWZpbml0aW9uIGUgOiBmID0gZy4KICBhcHBseSBwYXRoX2ZvcmFs bDsgaW50cm9zIHg7IGFwcGx5IHBhdGhfZm9yYWxsOyBpbnRyb3MgeS4KICBkZXN0cnVjdCB4LCB5 OyByZWZsZXhpdml0eS4KRGVmaW5lZC4KCkRlZmluaXRpb24gUGhpIDogQm9vbCAtPiBUeXBlIDo9 CiAgZnVuIHggPT4gbWF0Y2ggeCB3aXRoIHRydWUgPT4gQm9vbCB8IGZhbHNlID0+IFVuaXQgZW5k LgoKRGVmaW5pdGlvbiBQc2kgOiAoQm9vbC0+Qm9vbC0+Qm9vbCktPlR5cGUgOj0KICBmdW4gdSA9 PiBQaGkgKHUgdHJ1ZSB0cnVlKSAqIFBoaSAodSB0cnVlIGZhbHNlKSAqIFBoaSAodSBmYWxzZSB0 cnVlKSAqIFBoaSAodSBmYWxzZSBmYWxzZSkuCgpEZWZpbml0aW9uIFggOiBQc2kgZiA6PSAodHJ1 ZSx0dCx0dCx0dCkuCgpEZWZpbml0aW9uIFkgOiBQc2kgZyA6PSB0cmFuc3BvcnQgUHNpIGUgWC4K CigqIEJpbmFyeSBwcm9kdWN0cyBpbiBDb3EgYXNzb2NpYXRlIHRvIHRoZSBsZWZ0ICopCkRlZmlu aXRpb24gcHV6emxlIDogZnN0IChmc3QgKGZzdCBZKSkgPSB0cnVlLgpQcm9vZi4KICB1bmZvbGQg WSwgWCwgUHNpLgogIHJld3JpdGUgIXRyYW5zcG9ydF9wcm9kOyBjYm4uCiAgcmV3cml0ZSB0cmFu c3BvcnRfY29tcG9zZS4KICByZXdyaXRlIChhcF9jb21wb3NlIChmdW4gdSA9PiB1IHRydWUpIChm dW4gdiA9PiB2IHRydWUpIGUpLgogIHJld3JpdGUgIWFwX2FwcGx5X2wuCiAgdW5mb2xkIGUuCiAg cmV3cml0ZSAhYXAxMF9wYXRoX2ZvcmFsbC4KICByZWZsZXhpdml0eS4KRGVmaW5lZC4K --001a114022444857fe053bc987a8--