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