Migrate to use idris-setoid library.

1 files changed, 0 insertions, 37 deletions

diff --git a/src/Data/Setoid/Either.idr b/src/Data/Setoid/Either.idr
deleted file mode 100644
index 682ac5a..0000000
--- a/src/Data/Setoid/Either.idr
+++ /dev/null
@@ -1,37 +0,0 @@
-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