In the context of ICC/ICC* where conversion is strengthened by
ignoring erasable arguments, I bumped into the following comment:
as soon as one considers the extension to inductive types where
conversion irrelevance provides some form of weak extensionality.
Does someone here know what the above might be referring to?
Stefan