[Agda] Agda with the excluded middle is inconsistent ?

[Noam Zeilberger]

On Thu, Jan 7, 2010 at 10:40 PM, Thierry Coquand <coquand at chalmers.se> wrote:
> PS:  For proving the injectivity of S : Nat -> Nat using only the
> elimination rule over Id, one can for instance define a function
>  pred : Nat -> Nat
>  pred (S x) = x
>  pred 0 = 0
> and then prove Id Nat (S x) (S y) -> Id Nat x y using this function pred.
> Even if we consider I as a constructor for building elements of the type
> Set, this type Set is not
> "closed" as the type Nat (only constructors 0 and S) and one cannot define
> functions by case on the type Set.

That was my point, that it may be misleading to ask whether Set is
initial, i.e., whether one can define functions on Set by
case-analysis.  Sure, one can give a proof of the injectivity of S in
this way, but isn't it kind of a strange proof?  The case pred 0 = 0
is actually irrelevant.

Noam