[Agda] Agda with the excluded middle is inconsistent ?

[Thierry Coquand]

 Hello,

 Martin-Lof type theory has a fixed collection of inductive types: typically Nat, List A,  W A B and Id A a1 a2 with a collection
of universes Set:Set1:Set2:....

 One other difference between Agda and Martin-Lof type theory, which seems relevant here, is that if one uses only the
elimination rule over Id, it does not seem possible to show that the set constructor I is injective. At least, the proof

data I : (Set -> Set) -> Set where

  Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y
  Iinj refleq1 = refleq1

uses some operations (unification of I x and I y and hence of x and y) that apparently go beyond the elimination
rule for the Id type.

 Can one then conjecture that in Martin-Lof type theory extended with a data type

 I F : Set     (F: Set -> Set)

(which is injective for -conversion-) one cannot prove the injectivity of I, in the sense
that one cannot prove

 Id Set (I F) (I G) -> Id (Set->Set) F G

and that this system is consistent with classical logic?  (This seems possible via the set theoretic model
by interpreting I F to be always the empty set.)

      Best regards,

                Thierry

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.


On Jan 7, 2010, at 11:01 AM, Chung Kil Hur wrote:

Dear Dan,

Thanks for your answer.
Ok, Agda is a kind of constructive math assuming an anti-classical axiom.

Then, I have a few more questions.

Does the orginal Martin-Lof type theory also assume the injectivity of inductive type constructors ? or Agda added it later?
If the latter is the case, has the consistency of Agda been shown?
Or, is there a set-theoretic model of Agda ?

Thanks,
Chung-Kil Hur

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100107/8258c31c/attachment.html