1 files changed, 58 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Algebra/FreeExtension.idr b/src/Soat/FirstOrder/Algebra/FreeExtension.idr
new file mode 100644
index 0000000..675c65b
--- /dev/null
+++ b/src/Soat/FirstOrder/Algebra/FreeExtension.idr
@@ -0,0 +1,58 @@
+module Soat.FirstOrder.Algebra.FreeExtension
+
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
+
+import Soat.FirstOrder.Algebra
+import Soat.FirstOrder.Algebra.Coproduct
+import Soat.FirstOrder.Signature
+import Soat.FirstOrder.Term
+
+%default total
+
+public export
+FreeExtension : (a : RawAlgebra sig) -> (v : sig.T -> Type) -> RawAlgebra sig
+FreeExtension a v = Coproduct a (Free v)
+
+public export
+FreeExtensionAlgebra : (a : Algebra sig) -> (v : ISetoid sig.T) -> Algebra sig
+FreeExtensionAlgebra a v = CoproductAlgebra a (FreeAlgebra v)
+
+public export
+extend : {a : RawAlgebra sig} -> {u : sig.T -> Type} -> (f : IFunc v u)
+  -> IFunc (FreeExtension a v).U (FreeExtension a u).U
+extend f = coproduct {z = FreeExtension a u}
+  (\_ => Done . Left)
+  (\t => Done . Right . free f t)
+
+public export
+extendHomo : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
+  -> Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u)
+extendHomo f = coproductHomo {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))
+
+public export
+extendCong : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
+  -> (t : sig.T) -> {tm, tm' : (FreeExtension a.raw v.U).U t}
+  -> (FreeExtensionAlgebra a v).relation t tm tm'
+  -> ((FreeExtensionAlgebra a u).relation t `on` extend {a = a.raw} f.func t) tm tm'
+extendCong f = coproductCong {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))
+
+public export
+extendUnique : {a : Algebra sig} -> {v, u : ISetoid sig.T}
+  -> (f : IFunction v u)
+  -> (g : Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u))
+  -> (congL : {t : sig.T} -> (i : a.raw.U t)
+        -> (FreeExtensionAlgebra a u).relation t (g.func t (Done (Left i))) (Done (Left i)))
+  -> (congR : {t : sig.T} -> (i : Term sig v.U t)
+        -> (FreeExtensionAlgebra a u).relation t
+             (g.func t (Done (Right i)))
+             (Done (Right (free f.func t i))))
+  -> {t : sig.T} -> (tm : _)
+  -> (FreeExtensionAlgebra a u).relation t (g.func t tm) (extend {a = a.raw} f.func t tm)
+extendUnique f = coproductUnique {z = FreeExtensionAlgebra a u}
+  (injectLHomo {y = FreeAlgebra u})
+  (compHomo injectRHomo (freeHomo f))