[Agda] Agda with excluded middle is inconsistent

[Thorsten Altenkirch]

On 7 Jan 2010, at 17:17, Andreas Abel wrote:

> I agree with Thorstens analysis.  There is nothing like a "constructor", the machine only nows bits and sequences, so ultimately you need to explain everything but just these two principles: alternatives (bits) and composition (pairing).

and functions, i.e. pieces of code in a black box!


>  This is realized in so called structural type system, where a type is just an expression made of constants, +, \times, fixpoints, and function types.  Thorsten analyses Agda data declarations into structural expressions, so
> 
>  I = \ X. 0
> 
> which is not injective.  Named type systems, which use constructors (Agda) or class names (Java), restrict the power of structural type systems to make subtyping, unification, type checking etc. decidable and maybe your code more readable.  But I do not think that named type systems are foundational, they need to be explained in terms of structure.
> 
> So the problem at hand can be solved in conjunction with giving a semantics for Agda data types.  Using the semantics one can identify sufficient criteria for injectivity.
> 
> For a pragmatic solution, I suggest to consider the problem of injective type constructors in a simply-typed setting and then extrapolate to a dependently typed setting.
> 
> Cheers,
> Andreas
> 
> 
> On Jan 7, 2010, at 4:15 PM, Thorsten Altenkirch wrote:
> 
>> Hi Noam,
>> 
>>>> 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.
>> 
>> I don't see the analogy. A term constructor is injective because an inductive type is freely generated from constructors. Indeed, we can show that the structure map of an initial algebra is an isomorphism and hence injective. However the universe of sets is not freely constructed from type constructors but they are really definitions.
>> 
>> We should justify principles like this (i.e. all type constructors are injective) by a semantic explanation or by a translation into a well understood core language e.g. (extensional) Marttin-Loef Type Theory with W-types and universes. I don't know any such explanation which would justify this principle. Moreover, Chung's example shows that this is not possible (without giving up something else) since pure type theory is consistent with EM.
>> 
>> Cheers,
>> Thorsten
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda