diff options
Diffstat (limited to 'src/SOAS/Family.idr')
| -rw-r--r-- | src/SOAS/Family.idr | 43 |
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 |