Prove Either is a setoid.

1 files changed, 37 insertions, 0 deletions

diff --git a/src/Data/Setoid/Either.idr b/src/Data/Setoid/Either.idr
new file mode 100644
index 0000000..682ac5a
--- /dev/null
+++ b/src/Data/Setoid/Either.idr
@@ -0,0 +1,37 @@
+module Data.Setoid.Either
+
+import public Data.Setoid
+
+public export
+data Either : (0 r : Rel a) -> (0 s : Rel b) -> Rel (Either a b) where
+  Left  : forall r, s . r x y -> Either r s (Left x) (Left y)
+  Right : forall r, s . s x y -> Either r s (Right x) (Right y)
+
+public export
+[eitherRefl] Reflexive a rel => Reflexive b rel' => Reflexive (Either a b) (Either rel rel') where
+  reflexive {x = (Left x)}  = Left reflexive
+  reflexive {x = (Right x)} = Right reflexive
+
+public export
+[eitherSym] Symmetric a rel => Symmetric b rel' => Symmetric (Either a b) (Either rel rel') where
+  symmetric (Left eq)  = Left $ symmetric eq
+  symmetric (Right eq) = Right $ symmetric eq
+
+public export
+[eitherTrans] Transitive a rel => Transitive b rel'
+  => Transitive (Either a b) (Either rel rel') where
+  transitive (Left eq)  (Left eq')  = Left $ transitive eq eq'
+  transitive (Right eq) (Right eq') = Right $ transitive eq eq'
+
+public export
+EitherEquivalence : Setoid.Equivalence a rel -> Setoid.Equivalence b rel'
+  -> Setoid.Equivalence (Either a b) (Either rel rel')
+EitherEquivalence eq eq' = MkEquivalence
+  { refl  = MkReflexive $ reflexive @{eitherRefl @{eq.refl} @{eq'.refl}}
+  , sym   = MkSymmetric $ symmetric @{eitherSym @{eq.sym} @{eq'.sym}}
+  , trans = MkTransitive $ transitive @{eitherTrans @{eq.trans} @{eq'.trans}}
+  }
+
+public export
+EitherSetoid : Setoid -> Setoid -> Setoid
+EitherSetoid x y = MkSetoid _ _ $ EitherEquivalence x.equivalence y.equivalence