From 00fcc3517b7f680d31028abe83664a96305101b6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 24 Nov 2022 14:13:43 +0000
Subject: Define lifting of first-order signatures.

---
 soat.ipkg                               |  1 +
 src/Soat/SecondOrder/Signature/Lift.idr | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 src/Soat/SecondOrder/Signature/Lift.idr

diff --git a/soat.ipkg b/soat.ipkg
index e913be6..908c9c9 100644
--- a/soat.ipkg
+++ b/soat.ipkg
@@ -10,3 +10,4 @@ modules = Soat.Data.Product
         , Soat.Relation
         , Soat.SecondOrder.Algebra
         , Soat.SecondOrder.Signature
+        , Soat.SecondOrder.Signature.Lift
diff --git a/src/Soat/SecondOrder/Signature/Lift.idr b/src/Soat/SecondOrder/Signature/Lift.idr
new file mode 100644
index 0000000..159cdb3
--- /dev/null
+++ b/src/Soat/SecondOrder/Signature/Lift.idr
@@ -0,0 +1,14 @@
+module Soat.SecondOrder.Signature.Lift
+
+import public Soat.FirstOrder.Signature
+import public Soat.SecondOrder.Signature
+
+%default total
+
+public export
+data LiftOp : (O : a -> List a -> Type) -> (i : a) -> (ctx : List (Pair (List a) a)) -> Type where
+  Op : forall i . {ctx : List a} -> (op : o i ctx) -> LiftOp o i (map (MkPair []) ctx)
+
+public export
+lift : FirstOrder.Signature.Signature -> SecondOrder.Signature.Signature
+lift sig = MkSignature sig.T (LiftOp sig.O)
-- 
cgit v1.2.3