The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

The following thread is related.

https://lists.chalmers.se/pipermail/agda/2010/001526.html

In summary, Agada used to support "the injectivity of inductive type constructors" and after I proved False using the feature, it was removed from Agda.

Best,

Gil

On Tue, Feb 28, 2017 at 3:12 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 27/02/2017 19:26, Cristóbal Camarero Coterillo wrote:
> Some time ago I found this inductive type plus axiom of injectivity that
> implies False with the help of dependent_unique_choice and classic.
>
> Inductive some {T:Type} (t:T) : Type:=
> |some_single: some t
> |some_more: Type -> some t-> some t.
>
> Axiom some_inj: forall (T:Type) (x y:T), some x=some y -> x=y.
>
>
> I had really expected that some being a newly introduced type, it could
> be made injective. I mean, it is alike if two vectors are equal they
> must have the same dimension.

Your analogy is wrong. Two equal vectors have the same dimension because
their dimension is actually the size (e.g. the number of constructors)
of their inductive values. Here you have absolutely no relation between
x and a value of type (some x). In fact, if you forget the types, you
will notice that (some x) is no different from a natural number. So any
some_inj axiom that allows for a type T with a larger cardinal than nat
is inconsistent.

Best regards,

Guillaume