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/Algebra.idr | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 src/SOAS/Algebra.idr

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

diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr
new file mode 100644
index 0000000..7dff735
--- /dev/null
+++ b/src/SOAS/Algebra.idr
@@ -0,0 +1,40 @@
+module SOAS.Algebra
+
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Var
+
+public export
+record (.MonoidStruct)
+         (signature : type.SortedFunctor)
+         (x : type.SortedFamily) where
+  constructor MkSignatureMonoid
+  mon : type.MonStruct x
+  alg : signature x -|> x
+
+public export
+record (.MetaAlg)
+         (signature : type.SortedFunctor)
+         (meta : type.SortedFamily)
+         (a : type.SortedFamily) where
+  constructor MkMetaAlg
+  alg : signature a -|> a
+  var : Var -|> a
+  mvar : meta -|> (a ^ a)
+
+export
+traverse : {0 p,a : type.SortedFamily} ->
+      {0 signature : type.SortedFunctor} ->
+      (functoriality : signature.Map) =>
+      (str : Strength signature) =>
+      (coalg : type.PointedCoalgStruct p) =>
+      (alg : signature a -|> a) ->
+      (phi : p -|> a) ->
+      (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
+traverse {p,a} alg phi chi = MkMetaAlg
+      { alg = \h,s => alg $ str.str h s
+      , var = \v,s => phi (s v)
+      , mvar = \m,e,s => chi m (\v => e v s)
+      }
-- 
cgit v1.2.3