blob: 8014bac290842c7cad86ae7f6c9c28dd110ed6c0 (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
module Data.Setoid
import public Control.Relation
%default total
public export
record Equivalence a (rel : Rel a) where
constructor MkEquivalence
refl : Reflexive a rel
sym : Symmetric a rel
trans : Transitive a rel
public export
record Setoid where
constructor MkSetoid
0 U : Type
0 relation : Rel U
equivalence : Data.Setoid.Equivalence U relation
public export
equiv : Control.Relation.Equivalence a rel => Data.Setoid.Equivalence a rel
equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive)
public export
[refl'] (eq : Data.Setoid.Equivalence a rel) => Reflexive a rel where
reflexive = reflexive @{eq.refl}
public export
[sym'] (eq : Data.Setoid.Equivalence a rel) => Symmetric a rel where
symmetric = symmetric @{eq.sym}
public export
[trans'] (eq : Data.Setoid.Equivalence a rel) => Transitive a rel where
transitive = transitive @{eq.trans}
public export
[equiv'] Data.Setoid.Equivalence a rel => Control.Relation.Equivalence a rel
using refl' sym' trans' where
public export
(.reflexive) : Data.Setoid.Equivalence a rel -> {x : a} -> rel x x
(.reflexive) eq = reflexive @{eq.refl}
public export
(.symmetric) : Data.Setoid.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x
(.symmetric) eq = symmetric @{eq.sym}
public export
(.transitive) : Data.Setoid.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z
(.transitive) eq = transitive @{eq.trans}
public export
(.equalImpliesEq) : Data.Setoid.Equivalence a rel -> {x, y : a} -> x = y -> rel x y
(.equalImpliesEq) eq Refl = eq.reflexive
|
