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, 16 insertions, 0 deletions

diff --git a/src/Data/These/Decidable.idr b/src/Data/These/Decidable.idr
new file mode 100644
index 0000000..c044ca4
--- /dev/null
+++ b/src/Data/These/Decidable.idr
@@ -0,0 +1,16 @@
+module Data.These.Decidable
+
+import Data.Bool.Decidable
+import Data.These
+
+export
+viaEquivalence : a <=> b -> a `Reflects` x -> b `Reflects` x
+viaEquivalence eq (RTrue x) = RTrue (eq.leftToRight x)
+viaEquivalence eq (RFalse f) = RFalse (f . eq.rightToLeft)
+
+export
+reflectThese : a `Reflects` x -> b `Reflects` y -> These a b `Reflects` x || y
+reflectThese (RTrue x) (RTrue y) = RTrue (Both x y)
+reflectThese (RTrue x) (RFalse ny) = RTrue (This x)
+reflectThese (RFalse nx) (RTrue y) = RTrue (That y)
+reflectThese (RFalse nx) (RFalse ny) = RFalse (these nx ny $ const ny)