Initial.

Bool/Properties.lidr

+> module Bool.Properties
+
+> import Data.Fin
+> import Control.Isomorphism
+
+> import Basic.Predicates
+> import Finite.Predicates
+> import Sigma.Sigma
+
+> %default total
+> %access public export
+> %auto_implicits off
+
+
+> ||| Bool is not empty
+> notEmptyBool : Not (Empty Bool)
+> notEmptyBool = \ contra => contra False
+
+
+> ||| Bool is finite
+> finiteBool : Finite Bool
+> finiteBool = MkSigma 2 (MkIso to from toFrom fromTo) where
+> 
+>   to : Bool -> Fin 2
+>   to False =    FZ
+>   to  True = FS FZ
+>   
+>   from : Fin 2 -> Bool
+>   from             FZ   = False
+>   from         (FS FZ)  = True
+>   from     (FS (FS  k)) = absurd k
+
+>   toFrom : (k : Fin 2) -> to (from k) = k
+>   toFrom             FZ   = Refl
+>   toFrom         (FS FZ)  = Refl
+>   toFrom     (FS (FS  k)) = absurd k
+
+>   fromTo : (b : Bool) -> from (to b) = b
+>   fromTo False = Refl
+>   fromTo  True = Refl
+
+
+> ||| Equality of Bools is decidable
+> decidableEqBool : DecEq Bool
+> decidableEqBool = %implementation