[Agda] Agda with excluded middle is inconsistent

[Thorsten Altenkirch]

>> We should justify principles like this (i.e. all type constructors are injective) by a semantic explanation or by a translation into a well understood core language e.g. (extensional) Marttin-Loef Type Theory with W-types and universes. I don't know any such explanation which would justify this principle. Moreover, Chung's example shows that this is not possible (without giving up something else) since pure type theory is consistent with EM.
> 
> Agreed that there should be a convincing explanation, but again, I do
> think there is a strong intuition behind the principle (what Dan Doel
> and I were getting at), and the fact that it plays an important role
> in typechecking suggests that we shouldn't jump to conclusions.

I am not sure about this. *Most* datatype constructors are injective on type names, hence in functional programming one overgeneralizes this to *all*. Indeed this is one of the reasons that it is not clear how to add lambda abstractions on type level to Haskell, because Haskell assumes that all functions on the type level are injective. 

>  I am
> not sure that Agda should be conservative over classical mathematics:
> it seems there is a fundamental tension between exploiting the full
> power of a constructive type theory and upholding the fictions of
> classical mathematics.  Chung-Kil's paradox shows that you can't
> reason classically in Agda just by adding the law of excluded middle
> -- okay, so don't do it that way.

I don't think this is an instance of a constructive principle which is not valid classically (such as continuity). It seems rather an instance of something being wrong but not wrong enough to make the theory inconsistent. Another example is the propositional axiom of choice which is wrong but it doesn't make the theory inconsistent but only entails EM (by the Diaconescu construction). I mean being able to derive either EM or ~ EM are indications that something is wrong in these cases,

> Could you explain what you meant by: "Also while we may accept that
> extensions of Type Theory may be anticlassical, we should expect that
> core Type Theory is consistent with EM."?

In Martin-Loef Type Theory you cannot refute EM and I would expect that the same holds for Agda. Thinking about this, I wouldn't insist on this too strongly, but I'd need a better reason than "injectivity of type constructors". E.g. the observation that a function of type (Nat -> Nat) -> Nat can only use a finite amount of information of its input (i.e. continuity) we may want to built into our type theory (but how ?).

Cheers,
Thorsten