Define lifting of first-order signatures.

1 files changed, 14 insertions, 0 deletions

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)