[Agda] Agda with excluded middle is inconsistent

[Noam Zeilberger]

On Thu, Jan 7, 2010 at 4:15 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>> ...I'm not sure about this expansion, and the analogy.  I think the
>> question is whether we view the declaration of type constructors in
>> the same way that we view the declaration of term constructors (i.e.,
>> as stipulating a new way of constructing things, in this case
>> inhabitants of Set).  If we do, then type constructors are by
>> definition injective.
>
> I don't see the analogy. A term constructor is injective because an inductive type is freely generated from constructors. Indeed, we can show that the structure map of an initial algebra is an isomorphism and hence injective. However the universe of sets is not freely constructed from type constructors but they are really definitions.

But freeness ("inductive type = no confusion + no junk") is only a
sufficient condition, right?  Injectivity = no confusion.

> 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 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.

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."?

Noam