Split monolithic file into modules.

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

1 files changed, 43 insertions, 0 deletions

diff --git a/src/SOAS/Family.idr b/src/SOAS/Family.idr
new file mode 100644
index 0000000..cd3ae58
--- /dev/null
+++ b/src/SOAS/Family.idr
@@ -0,0 +1,43 @@
+module SOAS.Family
+
+import SOAS.Context
+
+infixr 3 -|> , -||> , -<>, =||> , =|> , >>> , ^
+infixl 3 <<<
+
+public export
+(.Family), ( .SortedFamily) : Type -> Type
+type.Family = type.Ctx -> Type
+type.SortedFamily = type -> type.Family
+
+public export 0
+(-||>) : {type : Type} -> (src,tgt : type.Family) -> Type
+(src -||> tgt) = {0 ctx : type.Ctx} -> src ctx -> tgt ctx
+
+public export 0
+(-|>) : {type : Type} -> (src,tgt : type.SortedFamily) -> Type
+(src -|> tgt) = {0 ty : type} -> src ty -||> tgt ty
+
+public export
+(<<<) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
+
+public export
+(>>>) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f >>> ctx0) ty ctx = f ty (ctx0 ++ ctx)
+
+public export 0
+(-<>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src -<> tgt) ty ctx = src ty -||> (tgt >>> ctx) ty
+
+public export
+(=||>) : (src, tgt : type.Family) -> type.Family
+(src =||> tgt) ctx = src ctx -> tgt ctx
+
+public export
+(=|>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src =|> tgt) ty = src ty =||> tgt ty
+
+public export 0
+(.gensubst) : (type : Type) -> (from,to : type.SortedFamily) -> (src,tgt : type.Ctx) -> Type
+type.gensubst from to src tgt = {0 ty : type} -> from ty src -> to ty tgt