Define kinds and monotypes.

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Inky/OnlyWhen.idr b/src/Inky/OnlyWhen.idr
new file mode 100644
index 0000000..7bed91a
--- /dev/null
+++ b/src/Inky/OnlyWhen.idr
@@ -0,0 +1,44 @@
+module Inky.OnlyWhen
+
+import Data.DPair
+
+public export
+data OnlyWhen : Maybe a -> (a -> Type) -> Type where
+  Yes : forall x. (px : p x) -> Just x `OnlyWhen` p
+  No : ((x : a) -> Not (p x)) -> Nothing `OnlyWhen` p
+
+public export
+decDPair : (v **  v `OnlyWhen` p) <=> Dec (x : a ** p x)
+decDPair =
+  MkEquivalence
+    { leftToRight = \case
+      (Just x ** Yes px) => Yes (x ** px)
+      (Nothing ** No prf) => No (\(x ** px) => prf x px)
+    , rightToLeft = \case
+      Yes (x ** px) => (Just x ** Yes px)
+      No prf => (Nothing ** No (\x, px => prf (x ** px)))
+    }
+
+public export
+decExists : Exists (`OnlyWhen` p) <=> Dec (Exists p)
+decExists =
+  MkEquivalence
+    { leftToRight = \case
+      Evidence .(Just x) (Yes px) => Yes (Evidence x px)
+      Evidence .(Nothing) (No prf) => No (\(Evidence x px) => void (prf x px))
+    , rightToLeft = \case
+      Yes (Evidence x px) => Evidence (Just x) (Yes px)
+      No prf => Evidence Nothing (No (\x, px => prf (Evidence x px)))
+    }
+
+public export
+decSubset : Subset (Maybe a) (`OnlyWhen` p) <=> Dec (Subset a p)
+decSubset =
+  MkEquivalence
+    { leftToRight = \case
+      Element (Just x) prf => Yes (Element x (case prf of Yes px => px))
+      Element Nothing prf => No (\(Element x px) => void (case prf of No prf => prf x px))
+    , rightToLeft = \case
+      Yes (Element x px) => Element (Just x) (Yes px)
+      No prf => Element Nothing (No (\x, px => prf (Element x px)))
+    }