1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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
|
