[Agda] Agda with the excluded middle is inconsistent ?

[Andrew Pitts]

Dear Andreas,

2010/1/12 Andreas Abel <andreas.abel at ifi.lmu.de>:
> With regard to what the criteria should be for legal data types or legal
> injective data types, I did not fully understand your proposal.

Nor did I :-) I'm a beginner as far as the workings of Adga goes.
Specifically...

> The reason
> why parameters to data types (as opposed to indices) can be arbitrarily
> large is that in a "Section" (Coq-terminology) with
>
>  Hypothesis X : very_large_type.
>
>  data List : Set where
>    ...
>
> one can close the section and abstract over all hypotheses, including X,
> which will be added as a parameter to List:
>
>  data List (X : very_large_type) : Set
>
> Thus, example J is not accepted by accident.  The ability to abstract freely
> is crucial.  It does not lead to inconsistencies since the typing of
> constructors ensures that elements of X are never stored in Lists.

...I was unaware of this subtlety.

> Surely, Vec
>
>  data Vec (A : Set) : Nat -> Set where
>    vnil  : Vec A zero
>    vcons : A -> Vec A n -> Vec A (suc n)
>
> should be injective in both arguments, but I would not deduce this from size
> considerations.  In this case it holds even if Vec would be just a
> definition
>
>  Vec A zero    = 1
>  Vec A (suc n) = A * Vec n
>
> because the cartesian product is injective.  Inferring injectivity from the
> definition is a very conservative approach,

indeed---I was being conservative in the face of potential inconsistency.

> and you may have a more liberal
> proposal in mind which I would be interested to learn more about.

I don't. Whatever proposal someone comes up with, let's hope it is
simple for the user to understand.

> P.S.:  I would have expected that
>
>  data I : (Set -> Set) -> Set where
>
> is not even a well-formed inductive family in Agda, since the index (Set ->
> Set) is too large.  But since there are no constructors, it goes through...

Yes, before Gil (as Chung Kil is known) gave his example I would have
guessed that the declaration is not legal.

Best wishes,

Andy