From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 5 Sep 2016 09:54:14 -0700 (PDT) From: Andrew Polonsky To: Homotopy Type Theory Message-Id: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> Subject: A puzzle about "univalent equality" MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_257_943558210.1473094454263" ------=_Part_257_943558210.1473094454263 Content-Type: multipart/alternative; boundary="----=_Part_258_1513151604.1473094454263" ------=_Part_258_1513151604.1473094454263 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 ------=_Part_258_1513151604.1473094454263 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi,

There is a common unders= tanding that the "right" concept of equality in Martin-Lof type t= heory is not the intensional identity type, but is a different notion of eq= uality, which is extensional. =C2=A0The adjunction of the univalence axiom = to standard MLTT makes the identity type behave like this "intended&qu= ot; 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 proper= ties* --- the things you can prove about it. =C2=A0But not its actual compu= tational behavior.

Since computational behavior ca= n often be "seen" on the logical level, I am trying to get a bett= er understanding of the sense in which this "Hott book" equality = type is really (in)complete. =C2=A0How would a "truly computational&qu= ot; equality type be different from it? =C2=A0(Other than satisfying canoni= city, etc.)

One precise example is that, for the &= quot;right" notion of equality, the equivalences characterizing path t= ypes of standard type constructors proved in Chapter 2 of the book could pe= rhaps hold definitionally. =C2=A0(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 fol= lowing puzzle.

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

e : f =3D g
e =3D FE(...) =C2=A0[usi= ng UA to get Function Extensionality]

Phi : Bool -= > Type
Phi tt =3D Bool
Phi ff =3D Unit
Psi : (Bool->Bool->Bool)->Type
Psi =3D \u. (= u tt tt) x (u tt ff) x (u ff tt) x (u ff ff)

X : P= si f
X =3D (tt,*,*,*)

Y : Psi g
Y =3D subst Psi e X

QUESTION.
Can we p= rove, in "book Hott", that "proj1 Y =3D tt" is inhabite= d?

Cheers!
Andrew
------=_Part_258_1513151604.1473094454263-- ------=_Part_257_943558210.1473094454263--