search

HoTT / book

A textbook on informal homotopy type theory
2.03k stars 359 forks source link

type errors in freudcompute1, freudcompute2 (8.6.11,8.6.12) #391

Closed ecavallo closed 11 years ago

ecavallo commented 11 years ago

In 8.6.11, t has the type _transport^B (merid(x_0), transport^B (merid(x0)^−1 , q)) = q, which means that r should be of type _merid x_2 ∙ (merid x_0)^-1 = transport B ((merid x0)^-1) q. However, r is specified as having type _merid x_2 ∙ (merid x_0)^-1 == q ∙ (merid x0)^-1. Since B ≡ λy. (N = y) the two are propositionally equal, but they're certainly not the same. The same problem appears in 8.6.12.

I'm not sure what the right fix is so that it works when used in the next proof.

mikeshulman commented 11 years ago

I'm glad someone is reading this proof carefully!

I don't think it matters how we fix this for the next proof, since where it gets used, r is just an unnamed coherence path. Probably the simplest thing to do would be to just specify the type of r correctly.

I also wonder whether the occurrence of r-double-prime in (8.6.11) ought to be r-single-prime?

andrejbauer commented 11 years ago

And this is where proof assistants come in very handy.

mikeshulman commented 11 years ago

Also where a version of type theory with judgmental computation rules for transport etc. would come in very handy. (-: