@@ -0,0 +1,32 @@
1+module Interfaces.Proposition
2+
3+%default total
4+%access public export
5+
6+
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
12+
13+Proposition () where
14+ atMostOneValue () () = Refl
15+
16+Proposition Void where
17+ atMostOneValue _ _ impossible
18+
19+Proposition (x = y) where
20+ atMostOneValue Refl Refl = Refl
21+
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
25+
26+Proposition (NonEmpty xs) where
27+ atMostOneValue IsNonEmpty IsNonEmpty = Refl
28+
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