Stlc.v

Inductive Ty : Set :=
| base
| fn (A B : Ty)
.

Inductive Ctx : Set :=
| cnil
| cext (Γ : Ctx) (A : Ty)
.

Inductive Var : Ctx -> Ty -> Type :=
| vz {Γ A}   : Var (cext Γ A) A
| vs {Γ A B} : Var Γ A -> Var (cext Γ B) A
.

Arguments vz {Γ A}.
Arguments vs {Γ A B} _.

Variant TmF (X : Ctx -> Ty -> Type) : Ctx -> Ty -> Type :=
| _lam {Γ A B} : X (cext Γ A) B -> TmF X Γ (fn A B)
| _app {Γ A B} : X Γ (fn A B) -> X Γ A -> TmF X Γ B
.

Arguments _lam {X Γ A B} _.
Arguments _app {X Γ A B} _ _.

Inductive TmM (X : Ctx -> Ty -> Type) (Γ : Ctx) (A : Ty) : Type :=
| var  : X Γ A -> TmM X Γ A
| cons : TmF (TmM X) Γ A -> TmM X Γ A
.

Arguments var  {X Γ A} _.
Arguments cons {X Γ A} _.

Definition Tm := TmM Var.

Definition map_TmF {X Y} (f : forall [Γ A], X Γ A -> Y Γ A) [Γ A] (t : TmF X Γ A) : TmF Y Γ A :=
  match t with
  | _lam t => _lam (f t)
  | _app t1 t2 => _app (f t1) (f t2)
  end.

Fixpoint map_TmM {X Y} (f : forall [Γ A], X Γ A -> Y Γ A) [Γ A] (t : TmM X Γ A) : TmM Y Γ A :=
  match t with
  | var x => var (f x)
  | cons t => cons (map_TmF (map_TmM f) t)
  end.

Definition ret_TmM {X} [Γ A] : X Γ A -> TmM X Γ A :=
  var.

Fixpoint μ_TmM {X} [Γ A] (t : TmM (TmM X) Γ A) : TmM X Γ A :=
  match t with
  | var x => x
  | cons t => cons (map_TmF μ_TmM t)
  end.

Definition bind_TmM {X Y} (f : forall [Γ A], X Γ A -> TmM Y Γ A) [Γ A] (t : TmM X Γ A) : TmM Y Γ A :=
  μ_TmM (map_TmM f t).

Notation lam t := (cons (_lam t)).
Notation app t1 t2 := (cons (_app t1 t2)).

Definition tm_x Γ A : Tm (cext Γ A) A := var vz.
Definition tm_id Γ A : Tm Γ (fn A A) := lam (var vz).