diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-01-26 15:15:23 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-01-26 15:15:23 +0000 |
| commit | 45a0e35acf9816c0c46ba85d5a84c2d0be6bb298 (patch) | |
| tree | 7af1b17beca6e500ececf6248cad4ea31b4b76f3 | |
| parent | 8dfd872384d32998886d9938f9c741002fd47253 (diff) | |
Provide a pointed coalgebra for variables.
| -rw-r--r-- | src/SOAS.idr | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/SOAS.idr b/src/SOAS.idr index 8540c83..80c5f7f 100644 --- a/src/SOAS.idr +++ b/src/SOAS.idr @@ -151,6 +151,13 @@ record (.PointedCoalgStruct) type (x : type.SortedFamily) where ren : x -|> [] x var : Var -|> x +%hint +(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var +type.VarPointedCoalgStruct = MkPointedCoalgStruct + { ren = \i, f => f i + , var = id + } + liftPos : (ctx : type.Ctx) -> (mon : type.PointedCoalgStruct p) => {ctx2 : type.Ctx} -> (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx) |