[Agda] Agda with the excluded middle is inconsistent ?

[Thorsten Altenkirch]

Hi Dan,

> As for justifying the injectivity of I (in reference to Thorsen Altenkirch's 
> other mails), I suppose it rather depends on what you think data declarations 
> are. If
> 
>  data I : (Set -> Set) -> Set where
> 
> is sugar for something like
> 
>  I : (Set -> Set) -> Set
>  I _ = data {}
> 
> then no, it would appear to not be injective. But the type constructors 
> defined by data don't appear to compute like that, at least. If I ask for the 
> normal form of:
> 
>  I F -> I G
> 
> I don't get
> 
>  data {} -> data {}
> 
> I get what I put in. So all appearances indicate that type constructors 
> defined by data (and codata for that matter) declarations do behave rather 
> like the constructors of an inductive type, and that the normal form of "I F" 
> is just "I F'" where F' is the normal form of F. And presumably the built-in 
> equality judgment I F = I G does ensure that F = G.

I think you make a similar point as Noam, which I have just replied to. 

> But, of course, the above analysis may be overly specific to the sort of 
> direct implementation of inductives that is currently used. I have no idea if 
> it could survive elaboration into a core theory, which would, I assume, give 
> you something much more like the "data {}" stuff. And that's really the 
> direction to go in (it seems to me), because trusting a core theory is much 
> easier than trusting that you've directly implemented all the sugar correctly.

Indeed, this is my conclusion. The translation into a core language corresponds to a semantic justification of the principle. And without such a justification I don't see any reason why such a principle should be adopted. Just because it has been implemented by accident?

Cheers,
Thorsten