blob: 5f9e1c92ad1ed5416f2384e3d37f8d291965f148 (
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
|
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
(.sub) :
(mon : type.MonStruct m) ->
m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
mon.sub t s = mon.mult t (m.extend s mon.var)
export
(.sub2) :
(mon : type.MonStruct m) ->
m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
m ty1 ctx -> m ty2 ctx -> m sy ctx
mon.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var))
|
