Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.

1 files changed, 33 insertions, 0 deletions

diff --git a/src/SOAS/Strength.idr b/src/SOAS/Strength.idr
new file mode 100644
index 0000000..f902ad4
--- /dev/null
+++ b/src/SOAS/Strength.idr
@@ -0,0 +1,33 @@
+module SOAS.Strength
+
+import SOAS.Family
+import SOAS.Structure
+import SOAS.Var
+
+public export
+0
+(.SortedFunctor) : (type : Type) -> Type
+type.SortedFunctor = type.SortedFamily -> type.SortedFamily
+
+public export
+record Strength (f : type.SortedFunctor) where
+  constructor MkStrength
+  strength :
+    (0 p,x : type.SortedFamily) ->
+    (mon : type.PointedCoalgStruct p) ->
+    (f (x ^ p)) -|> ((f x) ^ p)
+
+export
+(.str) :
+  Strength f ->
+  {0 p,x : type.SortedFamily} ->
+  (mon : type.PointedCoalgStruct p) =>
+  (f (x ^ p)) -|> ((f x) ^ p)
+strength.str {p,x,mon} = strength.strength p x mon
+
+public export
+record (.Map) (signature : type.SortedFunctor) where
+  constructor MkMap
+  map :
+    {0 a,b : type.SortedFamily} -> (a -|> b) ->
+    signature a -|> signature b