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
<andrew....@gmail.com> 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.