The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Hello fellow Coq'ers,

Suppose we have a type T and an equivalence relation E on T, and two 
elements t1 and t2 of type T.

There exists the axiom "classic" (in classical_prop.v I think) with 
which I can state that (t1 E t2) \/ ~ (t1 E t2).

This expression though, has type Prop. Its Set counterpart would be {t1 
E t2}+{~(t1 E t2)}. However it is known that adding the axiom 
(P:Prop){P}+{~P} make Coq inconsistent.

Now I was wondering if it is somehow possible to add an axiom to the 
Type level corresponding to the above excluded middle, that would allow 
me to decide whether t1 E t2 or not.


(I am trying to define the two vector vectorspace {v_1,v_2}, v_1 being 
the zero vector, so I need to define the action of some field on it. Now 
c.v_1 = v_1, but c.v_2 = v_2 only if c =/= zero. I need to provide an 
element v_i:(V::Type), so I'd need to eliminate the expression (t1 E t2) 
\/ ~ (t1 E t2) (::Prop) over V(::Type) which is not allowed. If I had 
(t1 E t2) \/ ~ (t1 E t2) :: Type, though, then I could.)

Jasper
--
+++ Out of Cheese error +++ MELON MELON MELON +++ Redo from Start +++