Cast algebraic structure as setoid homomorphisms.

2 files changed, 32 insertions, 0 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 97b6adc..982e54e 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -55,6 +55,11 @@ public export
 (.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
 
 public export
+(.semFunc) : (a : Algebra sig) -> {t : sig.T} -> (op : Op sig t)
+  -> index (Product a.setoid) op.arity ~> index a.setoid t
+a .semFunc op = MkSetoidHomomorphism (a.raw.sem op) (\_, _ => a.algebra.semCong op)
+
+public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index e7927ae..e52c945 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -4,6 +4,7 @@ import Data.List.Elem
 import Data.List.Sublist
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Pair
 import Data.Setoid.Product
 
 import Soat.SecondOrder.Signature
@@ -137,10 +138,36 @@ public export
 (.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
 
 public export
+(.renameFunc) : (a : Algebra sig) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
+  -> a.setoidAt ctx ~> a.setoidAt ctx'
+(.renameFunc) a f = MkIndexedSetoidHomomorphism
+  { H           = \t => a.raw.rename t f
+  , homomorphic = \t, _, _ => a.algebra.renameCong t f
+  }
+
+public export
+(.semFunc) : (a : Algebra sig) -> (ctx : _) -> {t : _} -> (op : Op sig t)
+  -> index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) op.arity
+       ~> index a.setoid (t, ctx)
+(.semFunc) a ctx op = MkSetoidHomomorphism
+  { H           = a.raw.sem ctx op
+  , homomorphic = \_, _ => a.algebra.semCong ctx op
+  }
+
+public export
 (.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
 (.varFunc) a ctx = mate (\_ => a.raw.var)
 
 public export
+(.substFunc) : (a : Algebra sig) -> (t : _) -> (ctx, ctx' : _)
+  -> Pair (index a.setoid (t, ctx')) (index (Product (a.setoidAt ctx)) ctx')
+       ~> index a.setoid (t, ctx)
+(.substFunc) a t ctx ctx' = MkSetoidHomomorphism
+  { H           = \x => a.raw.subst t ctx (fst x) (snd x)
+  , homomorphic = \_, _, eq => a.algebra.substCong t ctx (fst eq) (snd eq)
+  }
+
+public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism