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