From 580970d11a4e754c0c8e6f42c8312bffb1edc2db Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 5 Dec 2022 15:00:39 +0000
Subject: Move IsAlgebra relation from type to body.

---
 src/Soat/FirstOrder/Algebra.idr | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'src/Soat/FirstOrder/Algebra.idr')

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index f0b23ea..6f9389b 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -25,18 +25,22 @@ record RawSetoidAlgebra (0 sig : Signature) where
   0 relation : IRel raw.U
 
 public export
-record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  equivalence : IEquivalence a.U rel
+  0 relation  : IRel a.U
+  equivalence : IEquivalence a.U relation
   semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-    -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
+    -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms')
 
 public export
 record Algebra (0 sig : Signature) where
   constructor MkAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel raw.U
-  algebra    : IsAlgebra sig raw relation
+  algebra    : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> IRel a.raw.U
+(.relation) a = a.algebra.relation
 
 public export
 (.setoid) : Algebra sig -> ISetoid sig.T
-- 
cgit v1.2.3