diff --git a/coq/terms.v b/coq/terms.v
index 1930840..5d81179 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -36,10 +36,36 @@ Coercion type_var : string >-> type_term.
 Coercion expr_var : string >-> expr_term.
 
 (*
-Notation "( x )" := x (at level 70).
-Notation "x ~ y" := (type_rung x y) (at level 69, left associativity).
-Notation "< x y >" := (type_app x y) (at level 68, left associativity).
-Notation "'$' x" := (type_id x) (at level 66).
+Coercion type_var : string >-> type_term.
+Coercion expr_var : string >-> expr_term.
 *)
 
+Declare Scope ladder_type_scope.
+Declare Scope ladder_expr_scope.
+Declare Custom Entry ladder_type.
+
+Notation "[ e ]" := e (e custom ladder_type at level 80) : 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.
+
+Open Scope ladder_type_scope.
+
+Definition t1 : type_term := [ ∀α.∀β.(α~β~γ)->β->(α->α)->β ].
+
+Compute t1.
+Close Scope ladder_type_scope.
+
+
+
 End Terms.