Is Prop extensionality inconsistent in Coq?

I noticed a discussion on a mailing list about this topic from quite a while ago where they gave an example to show propositional extensionality was inconsistent:
link

However, I was not able to recreate it, as in further discussion it was noted that it was more an issue related to the definition of recursive functions, which seems to have been changed.

Is there a consensus on whether propositional extensionality is consistent or not?

The consensus is that propositional extensionality is consistent.

Inconsistencies in Coq are generally documented in dev/doc/critical-bugs; this one is documented here:
> component: library of extensional sets, guard condition
>
> summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets
>
> introduced: not a bug per se but an incompatibility discovered late
>
> impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it
>
> impacted coqchk versions: ?
>
> fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès)
>
> found by: Schepler, Dénès, Azevedo de Amorim
>
> exploit: ?
>
> GH issue number: none
>
> risk: unlikely to be exploited by chance (?)

So indeed this one has been fixed.

Propositional extensionality is easily shown to be consistent with the intended classical model of Coq (interpret Prop as bool), and Coq is widely believed to support this model (though of course there may be more bugs like the above).

Furthermore, propositional extensionality can be seen as a restricted version of univalence from Homotopy Type Theory, which posits roughly that isomorphic types are equal (more precisely, it defines a particular notion of isomorphism which has the property that, assuming functional extensionality, any two proofs of "f is an isomorphism" are equal, and then posits that the map from equality of types to isomorphism of types is itself an isomorphism). Univalence has been proven consistent (with pen and paper), and is widely held to be consistent with Coq without Prop (Homotopy Type Theory uses a different variant of Prop which is different in subtle ways from the Prop in Coq). Furthermore, univalence is widely believed to be consistent with a "propositional resizing axiom", which is believed to be adequate to model impredicative Prop when -indices-matter is turned on (which forces equality out of Prop).