diff options
Diffstat (limited to 'src/SOAS/Structure.idr')
| -rw-r--r-- | src/SOAS/Structure.idr | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr index 854725f..5f9e1c9 100644 --- a/src/SOAS/Structure.idr +++ b/src/SOAS/Structure.idr @@ -19,18 +19,11 @@ type.VarPointedCoalgStruct = MkPointedCoalgStruct , var = id } -liftPos : - (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) => - (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx) -liftPos Z f x = f x.toVar -liftPos (S l) f Here = mon.var (Here .toVar) -liftPos (S l) f (There pos) = mon.ren (liftPos l f pos) ThereVar - export lift : (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) => (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx) -lift ctx f v = liftPos ctx f v.pos +lift length f = p.copair length (\v => mon.ren (f v) weakl) (mon.var . weakr) -- Substitution Monoid @@ -44,11 +37,11 @@ export (.sub) : (mon : type.MonStruct m) -> m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx -mon.sub t s = mon.mult t (extend m s mon.var) +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 (extend m s2 (extend m s1 mon.var)) +mon.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var)) |