diff --git a/coq/terms.v b/coq/terms.v
index 5d81179..b998fa7 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -32,40 +32,62 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-Coercion type_var : string >-> type_term.
-Coercion expr_var : string >-> expr_term.
+(* values *)
+Inductive is_value : expr_term -> Prop :=
+  | V_ValAbs : forall x τ e,
+    (is_value (expr_tm_abs x τ e))
 
-(*
-Coercion type_var : string >-> type_term.
-Coercion expr_var : string >-> expr_term.
-*)
+  | V_TypAbs : forall τ e,
+    (is_value (expr_ty_abs τ e))
+
+  | V_Ascend : forall τ e,
+    (is_value e) ->
+    (is_value (expr_ascend τ e))
+.
 
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
+Declare Custom Entry ladder_expr.
 
-Notation "[ e ]" := e (e custom ladder_type at level 80) : ladder_type_scope.
+Notation "[ t ]" := t
+  (t custom ladder_type at level 80) : ladder_type_scope.
+Notation "'∀' x ',' t" := (type_univ x t)
+  (t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
+Notation "'<' σ τ '>'" := (type_spec σ τ)
+  (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
+Notation "'(' τ ')'" := τ
+  (in custom ladder_type at level 70) : ladder_type_scope.
+Notation "σ '->' τ" := (type_fun σ τ)
+  (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
+Notation "σ '->morph' τ" := (type_morph σ τ)
+  (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
+Notation "σ '~' τ" := (type_ladder σ τ)
+  (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
+Notation "'$' x '$'" := (type_id x%string)
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
+Notation "'%' x '%'" := (type_var x%string)
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
 
-(* TODO: allow any variable names in notation, not just α,β,γ *)
-Notation "'∀α.' τ" := (type_univ "α" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'∀β.' τ" := (type_univ "β" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'∀γ.' τ" := (type_univ "γ" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'<' σ τ '>'" := (type_spec σ τ) (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
-Notation "'(' τ ')'" := τ (in custom ladder_type at level 70) : ladder_type_scope.
-Notation "σ '->' τ" := (type_fun σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
-Notation "σ '->morph' τ" := (type_morph σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
-Notation "σ '~' τ" := (type_ladder σ τ) (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
-Notation "'α'" := (type_var "α") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
-Notation "'β'" := (type_var "β") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
-Notation "'γ'" := (type_var "γ") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
+Notation "[[ e ]]" := e
+  (e custom ladder_expr at level 80) : ladder_expr_scope.
+Notation "'%' x '%'" := (expr_var x%string)
+  (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
+Notation "'λ' x τ '↦' e" := (expr_tm_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
+Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
+  (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
 
 Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
 
-Definition t1 : type_term := [ ∀α.∀β.(α~β~γ)->β->(α->α)->β ].
+Check [ ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) ].
+
+Definition polymorphic_identity1 : expr_term := [[ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% ]].
+Definition polymorphic_identity2 : expr_term := [[ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% ]].
+
+Compute polymorphic_identity1.
 
-Compute t1.
 Close Scope ladder_type_scope.
-
-
+Close Scope ladder_expr_scope.
 
 End Terms.
diff --git a/coq/typing.v b/coq/typing.v
index e49b6af..a7e74e9 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -27,7 +27,7 @@ Reserved Notation "Gamma '|-' x '\compatible' X"  (at level 101, x at next level
 Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Var : forall Γ x τ,
     (context_contains Γ x τ) ->
-    (Γ |- x \is τ)
+    (Γ |- (expr_var x) \is τ)
 
   | T_Let : forall Γ s (σ:type_term) t τ x,
     (Γ |- s \is σ) ->