[Agda] Agda with the excluded middle is inconsistent ?

[Thorsten Altenkirch]

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

It isn't even possible to prove that List : Set -> Set is injective  
(e.g. one can use W-types to define List), I think. The reason is that  
one can identify sets upto isomorphism (this can be justified by the  
groupoid model) and List is not injective upto isomorphism. However,  
if we add universe elimination then we should be able to show  
injectivity for List.

>  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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

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