refactor: rename RawAlgebraWithRelation.

- RawAlgebraWithRelation -> RawSetoidAlgebra
- MkRawAlgebraWithRelation -> MkRawSetoidAlgebra
- rawWithRelation -> rawSetoid

2 files changed, 13 insertions, 13 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index f002dec..f0b23ea 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -19,8 +19,8 @@ record RawAlgebra (0 sig : Signature) where
   sem : sig `algebraOver` U
 
 public export
-record RawAlgebraWithRelation (0 sig : Signature) where
-  constructor MkRawAlgebraWithRelation
+record RawSetoidAlgebra (0 sig : Signature) where
+  constructor MkRawSetoidAlgebra
   raw        : RawAlgebra sig
   0 relation : IRel raw.U
 
@@ -43,8 +43,8 @@ public export
 (.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
 
 public export
-(.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig
-(.rawWithRelation) a = MkRawAlgebraWithRelation a.raw a.relation
+(.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
+(.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
 
 public export
 record IsHomomorphism
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 84ac436..736dc75 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -17,11 +17,11 @@ CoproductSet : (0 sig : Signature) -> (0 x, y : sig.T -> Type) -> sig.T -> Type
 CoproductSet sig x y = Term sig (\i => Either (x i) (y i))
 
 public export
-data (~=~) : (0 x, y : RawAlgebraWithRelation sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where
-  DoneL    : {0 x, y : RawAlgebraWithRelation sig}
+data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where
+  DoneL    : {0 x, y : RawSetoidAlgebra sig}
     -> {t : sig.T} -> {i, j : x.raw.U t} -> x.relation t i j
     -> (~=~) x y t (Done $ Left i) (Done $ Left j)
-  DoneR    : {0 x, y : RawAlgebraWithRelation sig}
+  DoneR    : {0 x, y : RawSetoidAlgebra sig}
     -> {t : sig.T} -> {i, j : y.raw.U t} -> y.relation t i j
     -> (~=~) x y t (Done $ Right i) (Done $ Right j)
   Call     : {t : sig.T} -> (op : Op sig t) -> {xs, ys : _} -> Pointwise ((~=~) x y) xs ys
@@ -30,12 +30,12 @@ data (~=~) : (0 x, y : RawAlgebraWithRelation sig) -> IRel (CoproductSet sig x.r
     -> (~=~) x y t (Done $ Left $ x.raw.sem op xs) (Call op (map (\_ => Done . Left) xs))
   InjectR  : {t : sig.T} -> (op : Op sig t) -> (xs : _)
     -> (~=~) x y t (Done $ Right $ y.raw.sem op xs) (Call op (map (\_ => Done . Right) xs))
-  Sym      : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm' : _}
+  Sym      : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {tm, tm' : _}
     -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm
-  Trans    : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm', tm'' : _}
+  Trans    : {0 x, y : RawSetoidAlgebra sig} -> {t : sig.T} -> {tm, tm', tm'' : _}
     -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm'' -> (~=~) x y t tm tm''
 
-parameters {0 x, y : RawAlgebraWithRelation sig}
+parameters {0 x, y : RawSetoidAlgebra sig}
   coprodRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
     -> {t : _} -> (tm : _) -> (~=~) x y t tm tm
   coprodsRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
@@ -75,7 +75,7 @@ Coproduct x y = MkRawAlgebra
 public export
 CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
   -> IsAlgebra sig (Coproduct x y)
-       ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel'))
+       ((~=~) (MkRawSetoidAlgebra x rel) (MkRawSetoidAlgebra y rel'))
 CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
   { equivalence = \t => MkEquivalence
     { refl  = MkReflexive $ coprodRelRefl
@@ -126,14 +126,14 @@ coproducts f g _ = bindTerms (\i => either (f i) (g i))
 public export
 coproductCong : {x, y, z : Algebra sig}
   -> (f : Homomorphism x z) -> (g : Homomorphism y z)
-  -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
+  -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
   -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
 
 public export
 coproductsCong : {x, y, z : Algebra sig}
   -> (f : Homomorphism x z) -> (g : Homomorphism y z)
   -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
-  -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms'
+  -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
   -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
 
 coproductCong f g _ (DoneL eq)       = f.homo.cong _ eq