Agda with the excluded middle is inconsistent ?

[Chung Kil Hur]

Hi everyone,

I proved the absurdity in Agda assuming the excluded middle.
Is it a well-known fact ?
It seems that Agda's set theory is weird.

This comes from the injectivity of inductive type constructors.

The proof sketch is as follows.

Define a family of inductive type

data I : (Set -> Set) -> Set where

with no constructors.

By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.

As you may see, there is a size problem with this injectivity.

So, I just used the cantor's diagonalization to derive absurdity in a classical way.

Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done intuitionistically ?
If the latter is true, then the Agda system is inconsistent.

Please have a look at the Agda code below, and let me know if there's any mistakes.

All comments are wellcome.

Thanks,
Chung-Kil Hur


============== Agda code ===============

module cantor where

data Empty : Set where

data One : Set where
one : One

data coprod (A : Set1) (B : Set1) : Set1 where
inl : ¢£ (a : A) -> coprod A B
inr : ¢£ (b : B) -> coprod A B

postulate exmid : ¢£ (A : Set1) -> coprod A (A -> Empty)

data Eq1 {A : Set1} (x : A) : A -> Set1 where
refleq1 : Eq1 x x

cast : ¢£ { A B } -> Eq1 A B -> A -> B
cast refleq1 a = a

Eq1cong : ¢£ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
Eq1cong a refleq1 = refleq1

Eq1sym : ¢£ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
Eq1sym refleq1 = refleq1

Eq1trans : ¢£ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
Eq1trans refleq1 refleq1 = refleq1

data I : (Set -> Set) -> Set where

Iinj : ¢£ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y
Iinj refleq1 = refleq1

data invimageI (a : Set) : Set1 where
invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a

J : Set -> (Set -> Set)
J a with exmid (invimageI a)
J a | inl (invelmtI x y) = x
J a | inr b = ¥ë x ¡æ Empty

data invimageJ (x : Set -> Set) : Set1 where
invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x

IJIeqI : ¢£ x -> Eq1 (I (J (I x))) (I x)
IJIeqI x with exmid (invimageI (I x))
IJIeqI x | inl (invelmtI x' y) = y
IJIeqI x | inr b with b (invelmtI x refleq1)
IJIeqI x | inr b | ()

J_srj : ¢£ (x : Set -> Set) -> invimageJ x
J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))

cantor : Set -> Set
cantor a with exmid (Eq1 (J a a) Empty)
cantor a | inl a' = One
cantor a | inr b = Empty

OneNeqEmpty : Eq1 One Empty -> Empty
OneNeqEmpty p = cast p one

cantorone : ¢£ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One
cantorone a p with exmid (Eq1 (J a a) Empty)
cantorone a p | inl a' = refleq1
cantorone a p | inr b with b p
cantorone a p | inr b | ()

cantorempty : ¢£ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
cantorempty a p with exmid (Eq1 (J a a) Empty)
cantorempty a p | inl a' with p a'
cantorempty a p | inl a' | ()
cantorempty a p | inr b = refleq1

cantorcase : ¢£ a -> Eq1 cantor (J a) -> Empty
cantorcase a pf with exmid (Eq1 (J a a) Empty)
cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))

absurd : Empty
absurd with (J_srj cantor)
absurd | invelmtJ a y = cantorcase a (Eq1sym y)

=====================================

[Dan Doel]

Post by Chung Kil Hur
Hi everyone,
I proved the absurdity in Agda assuming the excluded middle.
Is it a well-known fact ?
It seems that Agda's set theory is weird.
This comes from the injectivity of inductive type constructors.
The proof sketch is as follows.
Define a family of inductive type
data I : (Set -> Set) -> Set where
with no constructors.
By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.
As you may see, there is a size problem with this injectivity.
So, I just used the cantor's diagonalization to derive absurdity in a classical way.
Does anyone know whether cantor's diagonalization essentially needs the
classical axiom, or can be done intuitionistically ? If the latter is
true, then the Agda system is inconsistent.
Please have a look at the Agda code below, and let me know if there's any mistakes.

I could certainly be wrong, but I don't think your code can be done without
assuming the excluded middle. For instance, I know of no way to write J
without it, because it would involve examining the parameter 'a' to see if it
is of the form 'I f' for some f, and that is not an operation that Agda
provides. You use the LEM that way several times, so I'm not particularly
worried that type constructor injectivity might be inconsistent. :)

More to the point, there are a couple ways to approach
constructivism/intuitionism. On the one hand, you can eliminate the classical
axioms, and see what kind of things you can still prove. But, you don't
necessarily have to stop there; you can also add anti-classical axioms that
would lead to inconsistency in a classical setting, but don't (and, perhaps,
are intuitively 'true') in a constructive setting. For instance, I've heard
some intuitionistic mathematics adds "all functions are continuous" as an
axiom.* And from that, and another anti-classical axiom or two, you can prove
that Nat is isomorphic to (Nat -> Bool) -> Bool, which is rather weird.

Injectivity of type constructors seems to be another anti-classical axiom.
Engaging in some loose meta-reasoning about Agda, we know that Set -> Set is
really the same size as Set, because every element of both corresponds to a
finite character string---the Agda program(s) that denotes it. So there isn't
really a size paradox in saying that there are injective functions into Set
from Set -> Set. And, intuitively, it's pretty clear that if f is a Set ->
Set, then I f is a Set such that if it is equal to I g, then f is equal to g,
because I f and I g aren't subject to any kind of reduction beyond
normalization of f an g.

But, as you've demonstrated this cuts us off from postulating and reasoning
about classical things in our language. So I could see why Coq wouldn't want
it (since they turned off impredicative set by default for the same reason).
And, of course, I could be wrong, and it may not be intuitionistically valid,
either.

Cheers,
-- Dan

* http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/

[r***@theorem.ca]

I spent some time trying to extend Chung-Kil's proof to an outright
contradiction, but Agda's predicativity thwarted my attempts. If Agda had
an impredictiave Prop universe like Coq does, there would be an outright
contradiciton. Below is my proof that Coq has non-injective type
constructors:

Definition Type1 := Type.

Inductive I : (Type1 -> Type1) -> Type1 := .

Section ChungKil.

Hypothesis InjI : forall x y, I x = I y -> x = y.

Definition P (x:Type1) : Type1 := exists a, I a = x /\ (inhabited (a x) -> False).

Definition p := I P.

Lemma contradiction : inhabited (P p) <-> (inhabited (P p) -> False).
Proof.
unfold P at 1.
unfold p at 1.
split.
intros [[a [Ha0 Ha1]]].
replace a with P in Ha1; [assumption|].
firstorder.
intros H.
constructor.
exists P.
firstorder.
Qed.

Lemma absurd : False.
assert (Z:=contradiction).
tauto.
Qed.

End ChungKil.

[Chung Kil Hur]

----- Original Message -----
From: <***@theorem.ca>
To: "Chung Kil Hur" <***@cam.ac.uk>
Cc: "Agda mailing list" <***@lists.chalmers.se>; <coq-***@inria.fr>
Sent: Friday, January 08, 2010 3:50 PM
Subject: Re: [Coq-Club] Agda with the excluded middle is inconsistent ?

Post by r***@theorem.ca
I spent some time trying to extend Chung-Kil's proof to an outright
contradiction, but Agda's predicativity thwarted my attempts. If Agda had
an impredictiave Prop universe like Coq does, there would be an outright
contradiciton. Below is my proof that Coq has non-injective type
Definition Type1 := Type.
Inductive I : (Type1 -> Type1) -> Type1 := .
Section ChungKil.
Hypothesis InjI : forall x y, I x = I y -> x = y.
Definition P (x:Type1) : Type1 := exists a, I a = x /\ (inhabited (a x) -> False).
Definition p := I P.
Lemma contradiction : inhabited (P p) <-> (inhabited (P p) -> False).
Proof.
unfold P at 1.
unfold p at 1.
split.
intros [[a [Ha0 Ha1]]].
replace a with P in Ha1; [assumption|].
firstorder.
intros H.
constructor.
exists P.
firstorder.
Qed.
Lemma absurd : False.
assert (Z:=contradiction).
tauto.
Qed.
End ChungKil.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

Hi Russel,

I posted a similar proof yesterday, which is originally from Alexandre Miquel's idea.
But, I think I sent it to the Agda list only.

Here is what I wrote.

=============================================

Hi,

I need to mention one more thing.

Indeed, the injectivity of inductive type constructor is inconsistent in the prsence of Prop without LEM.

Actually, the original idea came from Alexandre Miquel.
He told Hugo that the injectivity of type constroctors for inductive familes of Prop is inconsistent without any help of axioms like "P <-> Q" -> "P = Q".

His proof in Coq is as follows:

----------------------------------------------------------------------
Inductive I : (Prop -> Prop) -> Prop := .

Axiom inj_I : forall x y, I x = I y -> x = y.

Definition R (x : Prop) := forall p, x = I p -> ~ p x.

Lemma R_eqv :
forall p, R (I p) <-> ~ p (I p).

Proof.
split; intros.
unfold R; apply H.
reflexivity.
unfold R; intros q H0.
rewrite <- (inj_I p q H0).
assumption.
Qed.

Lemma R_eqv_not_R :
R (I R) <-> ~ R (I R).

Proof (R_eqv R).

Lemma absurd : False.

Proof.
destruct R_eqv_not_R.
exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
-----------------------------------------------------

From this proof, I realized it can be applied to Set as well.

-----------------------------------------------------
Inductive I : (Set -> Set) -> Set :=
| i1 : I (fun x => x)
| i2 : I (fun x => x)
.

Axiom inj_I : forall x y, I x = I y -> x = y.

Definition R (x : Set) : Set := forall p: Set -> Set, x = I p -> p x -> False.

Lemma R_eqv_1 :
forall p, R (I p) -> (p (I p) -> False).

Proof.
intros ? ?.
apply H. reflexivity.
Qed.

Lemma R_eqv_2 :
forall p, (p (I p) -> False) -> R (I p).

intros.
unfold R; intros q H0.
rewrite <- (inj_I p q H0).
assumption.
Qed.

Lemma R_eqv_not_R_1 :
R (I R) -> R (I R) -> False.

Proof (R_eqv_1 R).

Lemma R_eqv_not_R_2 :
(R (I R) -> False) -> R (I R).

Proof (R_eqv_2 R).

Lemma absurd : False.

Proof.
set (H := R_eqv_not_R_1).
set (H0 := R_eqv_not_R_2).

exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
------------------------------------------------

But, in this proof, we need to notice that we use "False : Prop" rather than "Empty_set : Set".
If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it should "Set -> Type".
The reason why R is typable as Set -> Set is due to the impredicativity of Prop, because R is typepable as Set -> Prop, which is
coercible to Set -> Set.
This proof does not need any axiom, but just the impredicativity of Prop.

So, this idea does not aplly to Agda because it does not have any impredicative set like Prop.
So, I applied cantor's diagonalization assuming the law of excluded middle.

I think the presence of Prop is one of the fancy features of Coq as a proof assistant (at least to me).
So, the injectivity seems unatural to me in this view point.

Cheers,
Chung-Kil Hur

======================================================

[r***@theorem.ca]

Post by Chung Kil Hur
But, in this proof, we need to notice that we use "False : Prop" rather than "Empty_set : Set".
If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it should "Set -> Type".
The reason why R is typable as Set -> Set is due to the impredicativity of Prop, because R is typepable as Set -> Prop, which is
coercible to Set -> Set.

Ah, I didn't realize that Set was coercable to Prop otherwise I wouldn't
have done my Type1 nonsense.

Post by Chung Kil Hur
This proof does not need any axiom, but just the impredicativity of Prop.
So, this idea does not aplly to Agda because it does not have any impredicative set like Prop.
So, I applied cantor's diagonalization assuming the law of excluded middle.
I think the presence of Prop is one of the fancy features of Coq as a proof assistant (at least to me).
So, the injectivity seems unatural to me in this view point.

To be honest, the impredicativity of Prop in Coq worries me just a little
<http://r6.ca/blog/20091101T231201Z.html>

"Coq’s impredicative in Prop seems innocent because no information is
allowed to flow from the Prop universe to the Set universe; however Prop
values can witness termination of functions in Set. Perhaps there is an
inconsistency arising from the impredicativity of Prop that “proves” the
termination of some non-terminating function.

But worries about impredicativity is another story.

Thanks repeating the info on the Agda list for me.

[Chung Kil Hur]

----- Original Message -----
From: "Andrew Pitts" <***@cl.cam.ac.uk>
To: "Agda mailing list" <***@lists.chalmers.se>
Cc: "Andrew M Pitts" <***@cl.cam.ac.uk>
Sent: Sunday, January 10, 2010 3:34 PM
Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?

I have been following this thread with interest. What is needed most
is a simple yet expressive (and fixed!) core type theory with an
easily understandable (by users) semantics: we should not have to
"discover" the _logical_ consequences of an implementation---it's a
bit like saying the meaning of my programming language is given by my
compiler.
The rest of this message is speculation without reference to such a
semantics. :-)
Personally, my bet is that the version of Agda2 that allows one to
prove that type constructors are injective up to intensional equality
is inconsistent, without the need for any form of excluded middle
postulate.
I say this not because I think that the injectivity up to intensional
equality of type constructors is in itself contradictory---indeed I
believe it is quite a natural property to ask for....so long as the
universe in which the type constructor is valued is sufficiently
large. For example, in the presence of injectivity, allowing Set to
contain a (Set -> Set)-indexed family of mutually distinct names for
the empty set
data I : (Set -> Set) -> Set where
seems dangerous because Set is "too small"; whereas allowing it in Set1
data I1 : (Set -> Set) -> Set1 where
seems uncontentious. So I would advocate applying the same
predicativity/size considerations to (injective) type constructors as
Agda currently applies to data constructors. Another example: Agda2
allows
data J (f : Set -> Set) : Set where
unit : J f
almost by accident, since it doesn't allow
data K : (f : Set -> Set) -> Set where
unit : (f : Set -> Set) -> K f
because of predicativity restrictions on data constructors. I would
prefer to rule out both declarations while still allowing injective
type constructors like
data J1 (f : Set -> Set) : Set1 where
unit : J1 f
or
data K1 : (f : Set -> Set) -> Set1 where
unit : (f : Set -> Set) -> K1 f
Best wishes,
Andy

Hi,

I agree with Andy and I think the injectivity of type constructors is useful.
As long as Andy's idea, or a similar idea, is proven to be consistent, that can be used in reasoning about heterogeneous equality.

There are two well-known notions of heterogeneous equalitay: JMeq and eq_dep.
The definitions are as follows:

Inductive JMeq (A:Set) (a:A) : forall (B : Set), B -> Prop :=
| refljm : JMeq A a A a .

Inductive eq_dep (U:Set) (Sig: U -> Set) (x: U) (a: Sig x) : forall (y : U), Sig y -> Prop :=
| refldep : eq_dep U Sig x a x a .

Now, assume that you have the following heterogeneous eqaulities.

(1) JMeq (Vector n) l (Vector m) l'
(2) eq_dep nat Vector n l m l'

From (1), you can get the equation
Vector n = Vector m
but, not n = m as you don't have the injectivity of Vector.
On the contrary, from (2), you can get the equation
n = m
So, without the injectivity of Vector, the equation (1) does not have the same information as the equation (2).
But, the notion of JMeq is more homogeneous, general and convinient than that of eq_dep.

So, if you can enusre that some of your type constructors are injective, you can freely use JMeq instead of eq_dep for the data types.

Indeed, I have developed a library, called Heq, to support reasoning about heterogeneous (or, extensional) equality in Coq ,and going to be officially released in a few days.
This library basically supports both the notions of JMeq and eq_dep, but in a different uniform way.
For JMeq, if you add the injectivity of your type constructors to the database, the proof search engine uses the information.
Without the injectivity, the proof search engine does not do anything useful for JMeq.
The reason why I support for JMeq (though the extra code I added for supporting JMeq is several lines) is that I believed the injectivity until I find the inconsistency.
Anway, if we can somehow add the injectivity of some inductive type constructors, it is a quite useful thing for reasoning about heterogeneous equality.

Best wishes,
Chung-Kil Hur
Preuves, Programmes et Systèmes

[Andreas Abel]

Andy,

I agree we are in desperate need for a practical semantics for inductive
families.

With regard to what the criteria should be for legal data types or legal
injective data types, I did not fully understand your proposal. 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.

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, and you may have a more
liberal proposal in mind which I would be interested to learn more
about. Yet, I do not think it can be realized with the predicativity
restriction, since Set and Set -> Set are both part of the same universe
Set1, hence, need to be distinguished otherwise in order to separate the
good (Vec) from the bad (I, J). Probably that size check would be more
like the positivity test for data types.

Cheers,
Andreas

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

Post by Chung Kil Hur
----- Original Message -----
Sent: Sunday, January 10, 2010 3:34 PM
Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?

I have been following this thread with interest. What is needed most
is a simple yet expressive (and fixed!) core type theory with an
easily understandable (by users) semantics: we should not have to
"discover" the _logical_ consequences of an implementation---it's a
bit like saying the meaning of my programming language is given by my
compiler.
The rest of this message is speculation without reference to such a
semantics. :-)
Personally, my bet is that the version of Agda2 that allows one to
prove that type constructors are injective up to intensional equality
is inconsistent, without the need for any form of excluded middle
postulate.
I say this not because I think that the injectivity up to intensional
equality of type constructors is in itself contradictory---indeed I
believe it is quite a natural property to ask for....so long as the
universe in which the type constructor is valued is sufficiently
large. For example, in the presence of injectivity, allowing Set to
contain a (Set -> Set)-indexed family of mutually distinct names for
the empty set
data I : (Set -> Set) -> Set where
seems dangerous because Set is "too small"; whereas allowing it in Set1
data I1 : (Set -> Set) -> Set1 where
seems uncontentious. So I would advocate applying the same
predicativity/size considerations to (injective) type constructors as
Agda currently applies to data constructors. Another example: Agda2
allows
data J (f : Set -> Set) : Set where
unit : J f
almost by accident, since it doesn't allow
data K : (f : Set -> Set) -> Set where
unit : (f : Set -> Set) -> K f
because of predicativity restrictions on data constructors. I would
prefer to rule out both declarations while still allowing injective
type constructors like
data J1 (f : Set -> Set) : Set1 where
unit : J1 f
or
data K1 : (f : Set -> Set) -> Set1 where
unit : (f : Set -> Set) -> K1 f
Best wishes,
Andy

Hi,
I agree with Andy and I think the injectivity of type constructors is useful.
As long as Andy's idea, or a similar idea, is proven to be consistent, that can be used in reasoning about heterogeneous equality.
There are two well-known notions of heterogeneous equalitay: JMeq and eq_dep.
Inductive JMeq (A:Set) (a:A) : forall (B : Set), B -> Prop :=
| refljm : JMeq A a A a .
Inductive eq_dep (U:Set) (Sig: U -> Set) (x: U) (a: Sig x) : forall (y : U), Sig y -> Prop :=
| refldep : eq_dep U Sig x a x a .
Now, assume that you have the following heterogeneous eqaulities.
(1) JMeq (Vector n) l (Vector m) l'
(2) eq_dep nat Vector n l m l'
From (1), you can get the equation
Vector n = Vector m
but, not n = m as you don't have the injectivity of Vector.
On the contrary, from (2), you can get the equation
n = m
So, without the injectivity of Vector, the equation (1) does not have the same information as the equation (2).
But, the notion of JMeq is more homogeneous, general and convinient than that of eq_dep.
So, if you can enusre that some of your type constructors are injective, you can freely use JMeq instead of eq_dep for the data types.
Indeed, I have developed a library, called Heq, to support reasoning about heterogeneous (or, extensional) equality in Coq ,and going to be officially released in a few days.
This library basically supports both the notions of JMeq and eq_dep, but in a different uniform way.
For JMeq, if you add the injectivity of your type constructors to the database, the proof search engine uses the information.
Without the injectivity, the proof search engine does not do anything useful for JMeq.
The reason why I support for JMeq (though the extra code I added for supporting JMeq is several lines) is that I believed the injectivity until I find the inconsistency.
Anway, if we can somehow add the injectivity of some inductive type constructors, it is a quite useful thing for reasoning about heterogeneous equality.
Best wishes,
Chung-Kil Hur
Preuves, Programmes et Systèmes
------------------------------------------------------------------------
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Thorsten Altenkirch]

Post by Andreas Abel
I agree we are in desperate need for a practical semantics for
inductive families.

Not sure what practical means but what is the problem with the one in
our LICS paper?
http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf

Post by Andreas Abel
With regard to what the criteria should be for legal data types or
legal injective data types, I did not fully understand your
proposal. 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,
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.
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.

How do you prove that cartesian product is injective? Or List?

Cheers,
Thorsten

Post by Andreas Abel
Inferring injectivity from the definition is a very conservative
approach, and you may have a more liberal proposal in mind which I
would be interested to learn more about. Yet, I do not think it can
be realized with the predicativity restriction, since Set and Set ->
Set are both part of the same universe Set1, hence, need to be
distinguished otherwise in order to separate the good (Vec) from the
bad (I, J). Probably that size check would be more like the
positivity test for data types.
Cheers,
Andreas
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...

Post by Chung Kil Hur
Sent: Sunday, January 10, 2010 3:34 PM
Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?

I have been following this thread with interest. What is needed most
is a simple yet expressive (and fixed!) core type theory with an
easily understandable (by users) semantics: we should not have to
"discover" the _logical_ consequences of an implementation---it's a
bit like saying the meaning of my programming language is given by my
compiler.
The rest of this message is speculation without reference to such a
semantics. :-)
Personally, my bet is that the version of Agda2 that allows one to
prove that type constructors are injective up to intensional
equality
is inconsistent, without the need for any form of excluded middle
postulate.
I say this not because I think that the injectivity up to
intensional
equality of type constructors is in itself contradictory---indeed I
believe it is quite a natural property to ask for....so long as the
universe in which the type constructor is valued is sufficiently
large. For example, in the presence of injectivity, allowing Set to
contain a (Set -> Set)-indexed family of mutually distinct names for
the empty set
data I : (Set -> Set) -> Set where
seems dangerous because Set is "too small"; whereas allowing it in Set1
data I1 : (Set -> Set) -> Set1 where
seems uncontentious. So I would advocate applying the same
predicativity/size considerations to (injective) type constructors as
Agda currently applies to data constructors. Another example: Agda2
allows
data J (f : Set -> Set) : Set where
unit : J f
almost by accident, since it doesn't allow
data K : (f : Set -> Set) -> Set where
unit : (f : Set -> Set) -> K f
because of predicativity restrictions on data constructors. I would
prefer to rule out both declarations while still allowing injective
type constructors like
data J1 (f : Set -> Set) : Set1 where
unit : J1 f
or
data K1 : (f : Set -> Set) -> Set1 where
unit : (f : Set -> Set) -> K1 f
Best wishes,
Andy

Hi, I agree with Andy and I think the injectivity of type
constructors is useful.
As long as Andy's idea, or a similar idea, is proven to be
consistent, that can be used in reasoning about heterogeneous
equality.
There are two well-known notions of heterogeneous equalitay: JMeq and eq_dep.
Inductive JMeq (A:Set) (a:A) : forall (B : Set), B -> Prop :=
| refljm : JMeq A a A a .
Inductive eq_dep (U:Set) (Sig: U -> Set) (x: U) (a: Sig x) : forall
(y : U), Sig y -> Prop :=
| refldep : eq_dep U Sig x a x a .
Now, assume that you have the following heterogeneous eqaulities.
(1) JMeq (Vector n) l (Vector m) l' (2) eq_dep nat Vector n l
m l' From (1), you can get the equation
Vector n = Vector m
but, not n = m as you don't have the injectivity of Vector.
On the contrary, from (2), you can get the equation
n = m
So, without the injectivity of Vector, the equation (1) does not
have the same information as the equation (2).
But, the notion of JMeq is more homogeneous, general and convinient than that of eq_dep.
So, if you can enusre that some of your type constructors are
injective, you can freely use JMeq instead of eq_dep for the data
types.
Indeed, I have developed a library, called Heq, to support
reasoning about heterogeneous (or, extensional) equality in
Coq ,and going to be officially released in a few days.
This library basically supports both the notions of JMeq and
eq_dep, but in a different uniform way.
For JMeq, if you add the injectivity of your type constructors to
the database, the proof search engine uses the information.
Without the injectivity, the proof search engine does not do
anything useful for JMeq.
The reason why I support for JMeq (though the extra code I added
for supporting JMeq is several lines) is that I believed the
injectivity until I find the inconsistency.
Anway, if we can somehow add the injectivity of some inductive type
constructors, it is a quite useful thing for reasoning about
heterogeneous equality.
Best wishes,
Chung-Kil Hur
Preuves, Programmes et Systèmes
------------------------------------------------------------------------
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda