The 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 imp

The 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...