4 ms·
> Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory
by CHY872 12y ago
> Actually, I am aware of another, much more serious problem with CoIC formalism which was found when Coq was tried to be used to formalize homotopy type theory. It was a bug in CoIC, not a software bug.
Do you have any references? Intrigued :)
- vilhelm_s 12y agoThe notion of guardedness (for structural recursion) was a bit too permissive. This lead to inconsistency if you assume e.g. (False->False = True) (which is implied by propositional extensionality, and by the univalence axiom). The same issue affected Agda also. It was discussed a lot on the Coq and Agda mailing lists, e.g. https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propositional-extensionality-the-return-of-the-revenge http://agda.chalmers.narkive.com/E2UeRTOx/re-coq-club-propos...