The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

It seems odd that any property would be understood as a line.  More
over, what would be the meaning of your axiom when instantiated for
the predicate (fun x => True).  Even if you manage to pass through
the problem of having your sigma-types being accepted, this would
tantamount (after decomposition of the axiom) to working in the
following context.

Parameter Point :Set.
Definition Line := Point ->Prop.
Parameter A:Point.
Parameter B:Point.
Parameter C:Point.
Parameter I4: forall D:Line, {~(D A)}+{~(D B)}+{~(D C)}.

But this context implies False: just take the following
proof:

Theorem the_contradiction : False.
Proof.
destruct (my_algo (fun x => True)) as [[H | H]| H]; apply H;exact I.
Qed. 

I would rather believe you need to have a predicate on predicates
that distinguishes the lines from other propositions 
and you should work in a context of this form:

Parameter Point : Set.
Parameter is_a_line : (Point -> Prop) -> Prop.

Now, to pass through the problem of having your sigma-types accepted,
replace any instance of { x : A & B} with sigT(fun x : A => B).

Here is an example which is accepted in my version of Coq

Axiom I4 :
  sigT (fun A:Point =>
         sigT (fun B:Point => 
                sigT (fun C:Point =>
                       forall D:Point->Prop, is_a_line D ->
                         {~(D A)}+{~(D B)}+{~(D B)}))).

I guess you have a clearer idea than me about what should be in the
definition of "is_a_line", to make sure you capture the geometrical
intuition you have in mind.

Yves