atleasttwo.idr

import Decidable.Equality
%default total

AtLeastTwo : Type -> Type
AtLeastTwo ty = Sigma (ty,ty) (\(a,b) => Not (a = b))

atLeastTwoNats : AtLeastTwo Nat
atLeastTwoNats = ((0,1) ** absurd)

atLeastTwoBools : AtLeastTwo Bool
atLeastTwoBools = ((True,False) ** trueNotFalse)

notAtLeastTwoUnits : Not (AtLeastTwo ())
notAtLeastTwoUnits (((),()) ** prf) = prf Refl

notAtLeastTwoVoids : Not (AtLeastTwo Void)
notAtLeastTwoVoids ((a, _) ** prf) = a

foo : AtLeastTwo ty -> Not ((a : ty) -> (b : ty) -> a = b)
foo ((a, b) ** distinct) prf = distinct $ prf a b

-- AFAIK this is impossible. We have a proof that not all inhabitants are equal,
-- but no way to get any inhabitants.
bar : Not ((a : ty) -> (b : ty) -> a = b) -> AtLeastTwo ty
bar x = ?bar_rhs