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