Hidden Functional Extensionality

[Ailrun]

Equations introduce functional extensionality for per_univ_elem_equation_1, so basically all proofs are under the axiom.
It would be possible to remove the axiom by replacing Equations with some manual definitions.

C.C. @HuStmpHrrr

[Ailrun]

Note: There is Unset Equations With Funext. option but it just removes per_univ_elem_equation_1 or so, thus does not help.

[HuStmpHrrr]

what? I don't get it, why doesn't it help? where else is it used?

[HuStmpHrrr]

do you mean it's left as a proof obligation, or what?

in any case, why can't we have functional extensionality, though?

[Ailrun]

@HuStmpHrrr I mean it doesn't help in the sense that it completely removes per_univ_elem_equation_1 and effect of simp. Without those, yes, we can prove the relationship between per_univ_elem and per_univ_elem_core, but why would we use Equations to define per_univ_elem if we do not get those?

[Ailrun]

in any case, why can't we have functional extensionality, though?

Having functional extensionality itself is not a problem. This issue is more that we should note (and leave a comment or so) that our current approach based on Equations requires functional extensionality.

[HuStmpHrrr]

in any case, why can't we have functional extensionality, though?

Having functional extensionality itself is not a problem. This issue is more that we should note (and leave a comment or so) that our current approach based on Equations requires functional extensionality.

That's fine. We can do that. Not using functional extensionality is quite unnecessary.