blob: 682ac5a7937c9fac5b6c4505db33c5a0d0444464 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
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
|
