Require Import Autosubst2.syntax List.

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

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

Inductive lookup {A} : nat -> list A -> A -> Prop :=
| here A Γ : lookup 0 (cons A Γ) A
| there i Γ A B :
  lookup i Γ A ->
  lookup (S i) (cons B Γ) A.

Definition ctx := list (Level * Ty).

Definition squash a :=
  match a with
  | Fixed ℓ => false
  | Floating ℓ => true
  end.

Fixpoint fixed_ctx (Γ : ctx) :=
  match Γ with
  | nil => nil
  | (a, _) :: Γ => squash a :: 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 => lookup 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) ℓ ->
  lookup i Γ (ℓ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 ->
  liftable (fixed_ctx Γ) 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).