From 6dde244c14410ede6d41e9a8607016e23c19e320 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 15:23:47 +0000
Subject: Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.
---
 src/SOAS/Strength.idr | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 src/SOAS/Strength.idr

(limited to 'src/SOAS/Strength.idr')

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
-- 
cgit v1.2.3