search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.24k stars 189 forks source link

Fix HIT definitions. #122

Closed peterlefanulumsdaine closed 9 years ago

peterlefanulumsdaine commented 11 years ago

Rewrite the defined HIT eliminators as described to Yves’ email today, so that Anthony’s inconsistency isn’t available for them.

peterlefanulumsdaine commented 11 years ago

I’ve fixed Suspension, but I’m leaving other types for others to fix, since I found doing it somewhat instructive :-) Status of our local inductives:

jcmckeown commented 11 years ago

Out of curiosity, good Peter... what ought "Local" do to "Inductive", and why does my shiny new copy of HoTT/coq.trunk not like them?

andrejbauer commented 11 years ago

It's a modification by Yves Bertot which hides the induction principle for an inductive type when the module is closed. It lets us fake higher inductive types.

peterlefanulumsdaine commented 11 years ago

Expanding on what Andrej said: it means that outside the enclosing module, the recursor of the type (equivalently, its “match” construction) is not available. However, functions defined within the module (unless specifically marked as “Local”) will be available globally, and (importantly) they will retain their computational behaviour.

This allows us to fake higher inductive types by the approach Dan described 2 years ago.

peterlefanulumsdaine commented 11 years ago

Oh, and re the second half of your question: I’m not sure, I’m afraid — I’m on the current HoTT/coq trunk, and Local Inductives work fine for me.

JasonGross commented 11 years ago

What is Anthony's inconsisteny?

peterlefanulumsdaine commented 11 years ago

After we first added HIT definitions using Yves’ Local Inductives, Anthony Bordg pointed out that we were doing it in a way which let a bit too much information leak out (essentially, the fact that the eliminator didn’t really use its path-premise was visible), giving an easy inconsistency. Yves explained in a subsequent email how to write HIT definitions so that this leak doesn’t occur, so we made sure to use this way since then. (Although we still don’t, I believe, have theoretical grounds to be really confident that there are no more such leaks.)

Anthony’s original post: https://groups.google.com/forum/#!msg/univalent-foundations/Mp3fI3wdtEI/1cLwdyb65K4J

Yves’ explanation of how to avoid it: https://groups.google.com/d/msg/univalent-foundations/e2NyQ3QuvXs/_1DGPAKcmSkJ

–p.

On Mon, Aug 19, 2013 at 1:13 AM, Jason Gross notifications@github.comwrote:

What is Anthony's inconsisteny?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/122#issuecomment-22832058 .

JasonGross commented 10 years ago

Would a patch granting https://coq.inria.fr/bugs/show_bug.cgi?id=3191 bring back the information leak and break the Coq implementation of HITs? (I'm trying to get lemmas like projT1_path_sigma_uncurried to be true judgmentally.)

mikeshulman commented 9 years ago

Fixed by #550.

Re: https://coq.inria.fr/bugs/show_bug.cgi?id=3191, yes, I think it would.