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

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

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