[Agda] Agda with excluded middle is inconsistent

[Ulf Norell]

On Fri, Jan 8, 2010 at 11:48 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk>wrote:

> On 8 Jan 2010, at 02:58, Nils Anders Danielsson wrote:
>
> I don't think so, but there was some scepticism when injectivity of type
> constructors was introduced. See the following thread:
>
> heterogeneous equality
> https://lists.chalmers.se/pipermail/agda/2008/000153.html
>
>
> I missed this thread. Interesting, especially Conor's comments.
>
> I wanted to see how often I have used this feature, so I reverted the
> change Ulf mentions in that thread. It turned out that I only had to
> modify two functions to make the 168 files of the standard library type
> check.
>
>
> This is good news.
>
> If reverting this change really is all that is needed to remove
> automatic type constructor injectivity (Ulf?), then I suggest that we
> make this feature optional, or remove it entirely.
>
>
> I'd be in favour to pragmafy it.
>

Done. There's now an option --injective-type-constructors which you need to
switch on if you want injective type constructors. Without it, Chung's proof
doesn't type check. Indeed, there are only two places in the standard
libraries which break without the option switched on.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100108/b1de84b9/attachment-0001.html