Re: A puzzle about "univalent equality"

[Robin Adams <robin....@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3103 bytes --]

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
>

[-- Attachment #1.2: Type: text/html, Size: 3835 bytes --]