Restart.

- use De Bruijn, as Namely, Painless had more pain than promised;
- remove higher-kinded types;
- provide ill-typing predicates;
- prove substitution respects ill-typing;

1 files changed, 0 insertions, 44 deletions

diff --git a/src/Inky/OnlyWhen.idr b/src/Inky/OnlyWhen.idr
deleted file mode 100644
index 7bed91a..0000000
--- a/src/Inky/OnlyWhen.idr
+++ /dev/null
@@ -1,44 +0,0 @@
-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)))
-    }