[Agda] Agda with excluded middle is inconsistent

[Noam Zeilberger]

2010/1/7 Thorsten Altenkirch <txa at cs.nott.ac.uk>:
> Dear Chung,
> congratulations! I didn't know about this problem and I think it is a
> serious issue indeed. Maybe it is a known issue? Nisse? Ulf?

I agree this is a very interesting observation, but...

> Surely, type constructors should not be injective in general. A definition
> of the form
> data I : (Set -> Set) -> Set where
> should be expandable by an annonymous declaration
> I : (Set -> Set) -> Set
> I F = data {}
> in an analogous way a named function definition can be expanded by
> definition and a lambda abstraction

...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.  Whereas if we view type constructors as
syntactic sugar for type definitions, then we can make the analogy you
made, and not all type constructors are injective.

Noam