[TYPES] Conversion irrelevance and extensionality
Stefan Monnier <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ 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