blob: 8c5bb5d7717259d6474c169db309edad277cb50a (
plain)
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
44
45
46
47
48
49
50
51
52
53
|
module SOAS.Structure
import SOAS.Context
import SOAS.Family
import SOAS.Var
-- Pointed Coalgebra
public export
record (.PointedCoalgStruct) type (x : type.SortedFamily) where
constructor MkPointedCoalgStruct
ren : x -|> [] x
var : Var -|> x
%hint
(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var
type.VarPointedCoalgStruct = MkPointedCoalgStruct
{ ren = \i, f => f i
, var = id
}
export
lift :
(length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
(p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
lift length f = p.copair length (\v => mon.ren (f v) weakl) (mon.var . weakr)
-- Substitution Monoid
public export
record (.MonStruct) (type : Type) (m : type.SortedFamily) where
constructor MkSubstMonoidStruct
var : Var -|> m
mult : m -|> (m ^ m)
export
(.wkn) :
(0 m : type.SortedFamily) -> (mon : type.PointedCoalgStruct m) =>
m sy ctx -> m sy (ctx :< (n :- ty))
m.wkn t = mon.ren t (weakl {length = S Z})
export
(.sub) :
(0 m : type.SortedFamily) -> (mon : type.MonStruct m) =>
m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
m.sub t s = mon.mult t (m.extend s mon.var)
export
(.sub2) :
(0 m : type.SortedFamily) -> (mon : type.MonStruct m) =>
m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
m ty1 ctx -> m ty2 ctx -> m sy ctx
m.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var))
|
