@@ -0,0 +1,32 @@
1+module Interfaces.Proposition
7+||| A canonical proof that some type containing no more than one value,
8+||| comprising a mere proposition.
9+interface Proposition t where
10+ ||| If there are two values of t, prove that they are actually the same
11+ atMostOneValue : (x : t) -> (y : t) -> x = y
14+ atMostOneValue () () = Refl
16+Proposition Void where
17+ atMostOneValue _ _ impossible
19+Proposition (x = y) where
20+ atMostOneValue Refl Refl = Refl
22+Proposition (LTE m n) where
23+ atMostOneValue {m=Z} LTEZero LTEZero = Refl
24+ atMostOneValue {m=S _} (LTESucc x) (LTESucc y) = cong $ atMostOneValue x y
26+Proposition (NonEmpty xs) where
27+ atMostOneValue IsNonEmpty IsNonEmpty = Refl
29+(Proposition a, Proposition b) => Proposition (a, b) where
30+ atMostOneValue (x1, y1) (x2, y2) =
31+ rewrite atMostOneValue x1 x2 in
32+ rewrite atMostOneValue y1 y2 in Refl