[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
