mortberg
commented
10 years ago The problem is that type checking is done on miniTT (MTT.hs) terms which don't know anything about the evaluation in the cubical set model (Eval.hs). Hence the typechecker can't figure out that the value of opBool3 false true is true. You can see this when looking at the (scary) output as everything is the same except for the third argument of Id which is opBool3 false true. A future goal is to develop a cubical type theory where the type checker knows how to compute with things in the cubical set model and in this language your example should work.
Also, I'm not sure that this can be proved with funExt either as you will most likely have to do some computations in the cubical set model for that proof as well. Maybe a better place to start if you want to play with funExt is to prove that two functions defined in standard type theory (ie that don't rely on computation in the cubical set model) are equal.
jonsterling
CohenCyril
I don't fully understand how the cubical sets stuff works, so forgive me if I'm noting something obvious. Anyway, I was trying to prove that
opBool3in theBoolEqBoolmodule was equivalent toorBool, defined as follows:I first tried using funext, which I had trouble with, so I broke it down to simply constructing a term in
Id Bool (orBool false true) (opBool3 false true); because the two evaluate to the same thing (true), I would have expected thatrefl Bool truewould have sufficed, but during type checking, it cast out a marvelous cacophony of noise: