Library lift

Structure Lift := mkLift {
         lift_S: Type;
         lift_T: Type;
         lift_prod : Type;
         lift_last: Type;
         lifted:> Type;
         lift_curry: lift_T -> lift_prod -> lift_last;
         lift_uncurry_open: ((lift_S -> lift_prod) -> (lift_S -> lift_last)) -> lifted
}.

Definition Tend (S: Type) (A: Type) :=
    mkLift S A unit A
          (S -> A)
          (fun f _ => f)
          (fun f => f (fun _: S => tt)).

Canonical Structure Tarrow (A: Type) (H: Lift) :=
    mkLift (lift_S H)
      (A -> lift_T H)
      (prod A (lift_prod H))
      (lift_last H)
      ((lift_S H -> A) -> lifted H)
      (fun f x => match x with (x1,x2) => lift_curry H (f x1) x2 end)
      (fun f x => lift_uncurry_open H (fun y: lift_S H -> lift_prod H => f (fun z => (x z, y z)))).

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Definition lift S {A B} (f : A -> B) (a : S -> A) (x: S) : B := f (a x).

Definition liftx' {H: Lift} (f: lift_T H) : lifted H :=
  lift_uncurry_open H (lift (lift_curry H f)).

Definition liftx {H: Lift} (f: lift_T H) : lifted H := @liftx' H f.
Global Opaque liftx.


Definition id_for_lift {A} (x: A) := x.
Tactic Notation "unfold_lift" :=
  change @liftx with @liftx'; unfold liftx' ;
  repeat match goal with
  | |- context [lift_uncurry_open (?F _)] => unfold F
  | |- context [Tarrow _ (?F _)] => unfold F
  end;
  unfold Tarrow, Tend, lift_S, lift_T, lift_prod, lift_last, lifted, lift_uncurry_open, lift_curry, lift.

Tactic Notation "unfold_lift" "in" hyp(H) :=
  change @liftx with @liftx' in H; unfold liftx' in H;
  repeat match type of H with
  | context [lift_uncurry_open (?F _)] => unfold F in H
  | context [Tarrow _ (?F _)] => unfold F in H
  end;
  unfold liftx', Tarrow, Tend, lift_S, lift_T, lift_prod, lift_last, lifted, lift_uncurry_open, lift_curry, lift in H.

Tactic Notation "unfold_lift" "in" "*" :=
  change @liftx with @liftx' in *; unfold liftx' in *;
  repeat match goal with
             | H: context [lift_uncurry_open (?F _)] |- _ => unfold F in H
             | |- context [Tarrow _ (?F _)] => unfold F
             end;
  unfold liftx', Tarrow, Tend, lift_S, lift_T, lift_prod, lift_last, lifted, lift_uncurry_open, lift_curry, lift in *.

Notation "'`' x" := (liftx x) (at level 9).
Notation "'`(' x ')'" := (liftx (x : _)).