Re: [HoTT] A puzzle about "univalent equality"

[Dan Licata <d...@cs.cmu.edu>]

yes, see https://github.com/dlicata335/hott-agda/blob/master/misc/Andrew.agda

Using the notation 

e1 : (x : Bool) → (f True x) == (g True x)
e1 True = id
e1 False = id

eh : (x : _) → f x == g x
eh True = λ≃ e1
eh False = λ≃ (λ { True → id ; False → id })

e : f == g
e = λ≃ eh

the steps are

goal : fst Y == True
goal = fst Y                                                                              ≃〈 ... 〉 
       transport (λ u → Phi (u True True)) e (fst X)                       ≃〈 ... 〉 
       transport Phi (ap (λ u → u True True) e) (fst X)                    ≃〈 ... 〉 
       transport Phi (ap (λ f₁ → f₁ True) (ap (λ f₁ → f₁ True) e)) (fst X) ≃〈 ... 〉 
       transport Phi (ap (λ f₁ → f₁ True) (λ≃ e1)) (fst X)                 ≃〈 ... 〉 
       True ∎

I would be very surprised if there was something like this that was not provable in "book HoTT”.  

-Dan

> On Sep 5, 2016, at 12:54 PM, 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.