The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> I think it should be possible to have both features, that is simulate
> definitional proof-irrelevance which is basically "extensional" type theory
> on the set level via a powerful tactic but don't put this into the
> foundations of the proof system.

I'm not sure how that can work.

IIUC you're suggesting to distinguish the proof-relevant equality `Eq(T) A B`
from the proof-irrelevant equality `isSet T ∧ Eq(T) A B`, and
then arrange for tactics to automatically provide the `isSet T` proof.

Personally, I'm not so much interested in proof-irrelevance as I'm
interested in erasing proofs, and the above doesn't seem able to
distinguish a proof that `α` is *equal* to `Nat` from one where `α` is
*equivalent* to `Nat` (where *equal* means that an object of
type `F α` can be cast at no runtime cost to type `F Nat` where
*equivalent* means that such a conversion can be made for all `F` but
it's not guaranteed to be a no-op).


        Stefan