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 == <i> \ 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