Who needs constructivism? Make types out of Boolean predicates! (Encoded constructively...)

Guard.idr

module Guard

%default total
%access public export

data Guarded : (a -> Bool) -> a -> Type where
  Guard : (pred : a -> Bool) -> (subject : a) -> (prf : pred subject = True)
        -> Guarded pred subject

data GuardedIsBogus : Type where
  BogusIf : (pred : a -> Bool) -> (subject : a)
          -> (counter : pred subject = False) -> Guarded pred subject
          -> GuardedIsBogus

Uninhabited GuardedIsBogus where
  uninhabited (BogusIf pred subject counter (Guard pred subject prf)) =
    trueNotFalse $ trans (sym prf) counter