From 45a0e35acf9816c0c46ba85d5a84c2d0be6bb298 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 26 Jan 2024 15:15:23 +0000
Subject: Provide a pointed coalgebra for variables.

---
 src/SOAS.idr | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

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)
-- 
cgit v1.2.3