From e8d6ac1f1d9c05b71bb9098a1590e29e5c93b0b8 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Nov 2022 14:53:03 +0000
Subject: Add a bundle for raw algebra with a relation.

---
 src/Soat/FirstOrder/Algebra.idr | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src')

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6f25f59..245af6d 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -26,6 +26,12 @@ public export
 MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
 MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
 
+public export
+record RawAlgebraWithRelation (0 sig : Signature) where
+  constructor MkRawAlgebraWithRelation
+  raw        : RawAlgebra sig
+  0 relation : IRel raw.U
+
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
   constructor MkIsAlgebra
@@ -44,6 +50,10 @@ public export
 (.setoid) : Algebra sig -> ISetoid sig.T
 (.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
+
 public export
 record IsHomomorphism
   {0 sig : Signature} (a, b : Algebra sig)
-- 
cgit v1.2.3