From 933b1cffc6d83dfd89b83ff6dd8f37731c5de1aa Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 29 Nov 2022 14:58:56 +0000 Subject: Prove Either is a setoid. --- src/Data/Setoid/Either.idr | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 src/Data/Setoid/Either.idr (limited to 'src') 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 -- cgit v1.2.3