From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 19 Sep 2016 05:40:18 -0700 (PDT) From: Robin Adams To: Homotopy Type Theory Message-Id: In-Reply-To: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> Subject: Re: A puzzle about "univalent equality" MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_364_940780207.1474288818161" ------=_Part_364_940780207.1474288818161 Content-Type: multipart/alternative; boundary="----=_Part_365_789471877.1474288818161" ------=_Part_365_789471877.1474288818161 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Very interesting thread. I'd like to add an observation: in cubical type theory, the terms X and Y are definitionally. equal. Proof: Let us use s == t to denote that s and t are the same expression, and s = t for definitional equality. Let e0 be the term such that x : Bool, y : Bool, i : I |- e0 : Path Bool (f x y) (g x y), so that e is the result of applying functional extensionality to e0, that is e == \ x y . e0 Note that e0[x := tt, y := tt] = Bool e0[x := tt, y := ff] = Unit e0[x := ff, y := tt] = Unit e0[x := ff, y := ff] = Unit Then we have Y == comp^i (psi (e i)) [] X = comp^i (phi (e i tt tt) x phi(e i tt ff) x phi(e i ff tt) x phi(e i ff ff)) [] X = comp^i (Bool x Unit x Unit x Unit) [] X = < comp^i Bool [] tt , comp^i Unit [] *, comp^i Unit [] *, comp^i Unit [] * > (computation rule for comp with Sigma) = < tt, *, *, * > (computation rule for comp with Bool and Unit) == X Note that this only works because X is a canonical object; it doesn't hold for an arbitrary term of type Psi f. (Because we don't, in general, have that comp maps 1_A to 1_A up to definitional equality; that is, we don't have comp^i A [] t = t where i does not occur free in A.) -- Robin On Monday, 5 September 2016 18:54:14 UTC+2, 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 > ------=_Part_365_789471877.1474288818161 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Very interesting thread.=C2=A0 I'd like to add an obse= rvation: in cubical type theory, the terms X and Y are definitionally. equa= l.

Proof: Let us use s =3D=3D t to denote that s and t are the same = expression, and s =3D t for definitional equality.

Let e0 be the ter= m such that x : Bool, y : Bool, i : I |- e0 : Path Bool (f x y) (g x y), so= that e is the result of applying functional extensionality to e0, that is<= br>
e =3D=3D <i> \ x y . e0

Note that

e0[x :=3D tt, = y :=3D tt] =3D Bool
e0[x :=3D tt, y :=3D ff] =3D Unit
e0[x :=3D ff, y= :=3D tt] =3D Unit
e0[x :=3D ff, y :=3D ff] =3D Unit

Then we have=

Y =3D=3D comp^i (psi (e i)) [] X
=C2=A0=C2=A0 =3D comp^i (phi (e= i tt tt) x phi(e i tt ff) x phi(e i ff tt) x phi(e i ff ff)) [] X
=C2= =A0=C2=A0 =3D comp^i (Bool x Unit x Unit x Unit) [] X
=C2=A0=C2=A0 =3D &= lt; comp^i Bool [] tt , comp^i Unit [] *, comp^i Unit [] *, comp^i Unit [] = * > (computation rule for comp with Sigma)
=C2=A0=C2=A0 =3D < tt, = *, *, * >=C2=A0 (computation rule for comp with Bool and Unit)
=C2=A0= =C2=A0 =3D=3D X

Note that this only works because X is a canonical o= bject; it doesn't hold for an arbitrary term of type Psi f.=C2=A0 (Beca= use we don't, in general, have that comp maps 1_A to 1_A up to definiti= onal equality; that is, we don't have comp^i A [] t =3D t where i does = not occur free in A.)

--
Robin

On Monday, 5 September 2016= 18:54:14 UTC+2, Andrew Polonsky wrote:
Hi,

There is a com= mon understanding that the "right" concept of equality in Martin-= Lof type theory is not the intensional identity type, but is a different no= tion of equality, which is extensional. =C2=A0The adjunction of the univale= nce axiom to standard MLTT makes the identity type behave like this "i= ntended" 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 *logi= cal properties* --- the things you can prove about it. =C2=A0But not its ac= tual computational behavior.

Since computational b= ehavior 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. =C2=A0How would a "truly comput= ational" equality type be different from it? =C2=A0(Other than satisfy= ing canonicity, etc.)

One precise example is that,= for the "right" notion of equality, the equivalences characteriz= ing path types of standard type constructors proved in Chapter 2 of the boo= k could perhaps hold definitionally. =C2=A0(The theorems proved there are t= hus "seeing" these equalities on the logical level.)
I tried to look for a more interesting example, and came up wi= th the following puzzle.

f, g : Bool -> Bool -&= gt; Bool
f x y =3D if x then y else ff
g x y =3D if y t= hen x else ff

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

Ph= i : 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 : Psi f
X =3D (tt,*,*,*)

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

QUESTION.
Can we prove, in "book Hott", that "proj1 Y =3D tt" i= s inhabited?

Cheers!
Andrew
<= /blockquote>
------=_Part_365_789471877.1474288818161-- ------=_Part_364_940780207.1474288818161--