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)