Define first-order algebras.

1 files changed, 63 insertions, 0 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
new file mode 100644
index 0000000..fef5871
--- /dev/null
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -0,0 +1,63 @@
+module Soat.FirstOrder.Algebra
+
+import Control.Relation
+
+import Soat.Data.Product
+import Soat.FirstOrder.Signature
+import Soat.Relation
+
+%default total
+%hide Control.Relation.Equivalence
+
+public export
+algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
+algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
+
+public export
+algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
+algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t
+
+public export
+record RawAlgebra (0 sig : Signature) where
+  constructor MakeRawAlgebra
+  0 U : sig.T -> Type
+  sem : sig `algebraOver` U
+
+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 IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
+  constructor MkIsAlgebra
+  0 equivalence : IEquivalence a.U rel
+  0 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')
+
+public export
+record Algebra (0 sig : Signature) where
+  constructor MkAlgebra
+  raw     : RawAlgebra sig
+  0 rel   : IRel raw.U
+  algebra : IsAlgebra sig raw rel
+
+public export
+(.setoid) : Algebra sig -> ISetoid sig.T
+(.setoid) a = MkISetoid a.raw.U a.rel a.algebra.equivalence
+
+public export
+record IsHomomorphism
+  {0 sig : Signature} (a, b : Algebra sig)
+  (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
+  where
+  constructor MkIsHomomorphism
+  0 cong    : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
+  0 semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+    -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
+
+public export
+record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
+  where
+  constructor MkHomomorphism
+  f    : (t : sig.T) -> a.raw.U t -> b.raw.U t
+  homo : IsHomomorphism a b f