Require Import Autosubst2.syntax List.

Reserved Notation "Γ ⊢ a ;; ℓ ∈ A" (at level 70).

Definition get_level a :=
  match a with
  | Fixed ℓ => ℓ
  | Floating ℓ => ℓ
  end.

Definition ctx := list (Level * Ty).

Fixpoint fix_ctx (Γ : ctx) :=
  match Γ with
  | nil => nil
  | (Fixed ℓ, A) :: Γ => (Fixed ℓ, A) :: fix_ctx Γ
  | (Floating ℓ, A) :: Γ => (Fixed ℓ, A) :: fix_ctx Γ
  end.

Fixpoint fixed_ctx (Γ : ctx) :=
  match Γ with
  | nil => nil
  | (Fixed ℓ, A) :: Γ => false :: fixed_ctx Γ
  | (Floating ℓ, A) :: Γ => true :: fixed_ctx Γ
  end.

(* false <= true *)
(* A term is liftable if it remains well-typed raising the levels of the floating levels to the current level *)
Fixpoint liftable Φ (a : Tm) :=
  match a with
  | VarTm i => nth_default true Φ i = false
  | FlApp a b => liftable Φ a /\ liftable Φ b
  | App a b => liftable Φ a
  | FlAbs a => liftable (false :: Φ) a
  | Abs a => liftable (false :: Φ) a
  end.

Inductive Wt (Γ : ctx) : Tm -> bool -> Ty -> Prop :=
| T_Var ℓ i ℓ0 A :
  Bool.le (get_level ℓ0) ℓ ->
  nth_error Γ i = Some (ℓ0, A) ->
  Γ ⊢ VarTm i ;; ℓ ∈ A

| T_FlApp ℓ a b A B :
  Γ ⊢ b ;; ℓ ∈ FlFun A B ->
  Γ ⊢ a ;; ℓ ∈ A ->
  Γ ⊢ FlApp b a ;; ℓ ∈ B

| T_FlAbs ℓ a A B :
  (Floating ℓ, A) :: Γ ⊢ a ;; ℓ ∈ B  ->
  Γ ⊢ FlAbs a ;; ℓ ∈ FlFun A B

| T_App ℓ ℓ0 a b A B :
  Γ ⊢ b ;; ℓ ∈ Fun ℓ0 A B ->
  Γ ⊢ a ;; ℓ0 ∈ A ->
  Γ ⊢ App b a ;; ℓ ∈ A

| T_Abs ℓ ℓ0 b A B :
  (Fixed ℓ0, A) :: Γ ⊢ b ;; ℓ ∈ B ->
  Γ ⊢ Abs b ;; ℓ ∈ Fun ℓ0 A B

where "Γ ⊢ a ;; ℓ ∈ A" := (Wt Γ a ℓ A).