How can I go about creating distinct variables in Idris?

I am trying to reconstruct the axioms for Hilbert's geometry in Idris. I came up with the following code to represent his axioms:

interface (Eq point) => Plane line point where
  colinear : point -> point -> point -> Bool
  contains : line -> point -> point -> Bool
  axiom1a : (a,b : point) -> (a /= b) = True -> (l : line ** (contains l a b = True))
  axiom1b : contains l a b = True -> contains m a b = True -> l = m
  axiom2 : (a : point ** (colinear a b c = False) && (a /= b) = True && (b /= c) = True && (a /= c) = True)
  axiom3 : (l : line) -> (a ** (contains l a b = True))

axiom2 should read "There exists 3 distinct non-colinear points." I get the following error:

When checking type of Main.axiom2:
When checking argument P to type constructor Builtins.DPair:
        Type mismatch between
                Bool (Type of _ && _)
        and
                Type (Expected type)

If I remove && (a /= b) = True && (b /= c) = True && (a /= c) = True the code runs but then the qualification of "distinct" in the axiom is lost. Any help would be appreciated.

Solution

colinear a b c = False is a Type, not a Bool. Likewise for (a /= b) = True, (b /= c) = True, and (a /= c) = True.

Instead of using &&, you must use a "type-level &&", i.e. a tuple.

axiom2 : (a : point ** (colinear a b c = False, (a /= b) = True, (b /= c) = True, (a /= c) = True))

However, that would read "There exists a point a that is not colinear with any two other distinct points", which is not always the case. You could instead write this:

axiom2 : (a : point ** (b : point ** (c : point ** (colinear a b c = False, (a /= b) = True, (b /= c) = True, (a /= c) = True))))

That would read "There exist three distinct points that are not colinear". I'm not sure if it's possible to make that any nicer to look at, like (a, b, c : point ** ....