diff --git a/coq/equiv.v b/coq/equiv.v
new file mode 100644
index 0000000..8df5e11
--- /dev/null
+++ b/coq/equiv.v
@@ -0,0 +1,308 @@
+(* This module defines an equivalence relation
+ * on type-terms.
+ *
+ * In general, we want distributivity of ladders
+ * over all other type constructors, e.g. type-
+ * specializations or function-types.
+ *
+ * Formally, we define two rewrite rules that
+ * shall define how we are able to rewrite type-terms
+ * such that they remain equivalent.
+ *
+ * (1) `-->distribute-ladder` which distributes
+ *    ladder types over other type constructors, e.g.
+ *    <S T~U>  -->distribute-ladder   <S T> ~ <S U>.
+ *
+ * (2) `-->condense-ladder` which does the
+ *    inverse operation, e.g.
+ *    <S T> ~ <S U>  -->condense-ladder  <S T~U>
+ *
+ * When applied exhaustively, each rewrite rule yields
+ * a normal form, namely *Ladder Normal Form (LNF)*, which
+ * is reached by exhaustive application of `-->distribute-ladder`,
+ * and *Parameter Normal Form (PNF)*, which is reached by exhaustive
+ * application of `-->condense-ladder`.
+ *
+ * The equivalence relation `===` over type-terms is then defined
+ * as the reflexive and transitive hull over `-->distribute-ladder`
+ * and `-->condense-ladder`. Since the latter two are the inverse
+ * rewrite-step of each other, `===` is symmetric and thus `===`
+ * satisfies all properties required of an equivalence relation.
+ *)
+Require Import terms.
+From Coq Require Import Strings.String.
+
+Include Terms.
+
+Module Equiv.
+
+
+(** Define all rewrite steps *)
+
+Reserved Notation "S '-->distribute-ladder' T" (at level 40).
+Inductive type_distribute_ladder : ladder_type -> ladder_type -> Prop :=
+  | L_DistributeOverApp : forall x y y',
+    (type_app x (type_rung y y'))
+    -->distribute-ladder
+    (type_rung (type_app x y) (type_app x y'))
+
+  | L_DistributeOverFun1 : forall x x' y,
+    (type_fun (type_rung x x') y)
+    -->distribute-ladder
+    (type_rung (type_fun x y) (type_fun x' y))
+
+  | L_DistributeOverFun2 : forall x y y',
+    (type_fun x (type_rung y y'))
+    -->distribute-ladder
+    (type_rung (type_fun x y) (type_fun x y'))
+
+where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
+
+
+
+Reserved Notation "S '-->condense-ladder' T" (at level 40).
+Inductive type_condense_ladder : ladder_type -> ladder_type -> Prop :=
+  | L_CondenseOverApp : forall x y y',
+    (type_rung (type_app x y) (type_app x y'))
+    -->condense-ladder
+    (type_app x (type_rung y y'))
+
+  | L_CondenseOverFun1 : forall x x' y,
+    (type_rung (type_fun x y) (type_fun x' y))
+    -->condense-ladder
+    (type_fun (type_rung x x') y)
+
+  | L_CondenseOverFun2 : forall x y y',
+    (type_rung (type_fun x y) (type_fun x y'))
+    -->condense-ladder
+    (type_fun x (type_rung y y'))
+
+where "S '-->condense-ladder' T" := (type_condense_ladder S T).
+
+
+(** Inversion Lemma:
+   `-->distribute-ladder` is the inverse of `-->condense-ladder
+*)
+Lemma distribute_inverse :
+  forall x y,
+  x -->distribute-ladder y ->
+  y -->condense-ladder x.
+Proof.
+  intros.
+  destruct H.
+  apply L_CondenseOverApp.
+  apply L_CondenseOverFun1.
+  apply L_CondenseOverFun2.
+Qed.
+
+(** Inversion Lemma:
+    `-->condense-ladder`  is the inverse of  `-->distribute-ladder`
+*)
+Lemma condense_inverse :
+  forall x y,
+  x -->condense-ladder y ->
+  y -->distribute-ladder x.
+Proof.
+  intros.
+  destruct H.
+  apply L_DistributeOverApp.
+  apply L_DistributeOverFun1.
+  apply L_DistributeOverFun2.
+Qed.
+
+
+(** Define the equivalence relation as reflexive, transitive hull. *)
+
+Reserved Notation " S '===' T " (at level 40).
+Inductive type_eq : ladder_type -> ladder_type -> Prop :=
+  | L_Refl : forall x,
+    x === x
+
+  | L_Trans : forall x y z,
+    x === y ->
+    y === z ->
+    x === z
+
+  | L_Distribute : forall x y,
+    x -->distribute-ladder y ->
+    x === y
+
+  | L_Condense : forall x y,
+    x -->condense-ladder y ->
+    x === y
+
+where "S '===' T" := (type_eq S T).
+
+
+
+(** Symmetry of === *)
+Lemma type_eq_is_symmetric :
+  forall x y,
+  (x === y) -> (y === x).
+Proof.
+  intros.
+  induction H.
+  
+  1:{
+    apply L_Refl.
+  }
+
+  2:{
+    apply L_Condense.
+    apply distribute_inverse.
+    apply H.
+  }
+  2:{
+    apply L_Distribute.
+    apply condense_inverse.
+    apply H.
+  }
+
+  apply L_Trans with (y:=y).
+  apply IHtype_eq2.
+  apply IHtype_eq1.
+Qed.
+
+(** "flat" types do not contain ladders *)
+Inductive type_is_flat : ladder_type -> Prop :=
+  | FlatUnit : (type_is_flat type_unit)
+  | FlatVar : forall x, (type_is_flat (type_var x))
+  | FlatNum : forall x, (type_is_flat (type_num x))
+  | FlatId : forall x, (type_is_flat (type_id x))
+  | FlatApp : forall x y,
+    (type_is_flat x) ->
+    (type_is_flat y) ->
+    (type_is_flat (type_app x y))
+
+  | FlatFun : forall x y,
+    (type_is_flat x) ->
+    (type_is_flat y) ->
+    (type_is_flat (type_fun x y))
+
+  | FlatSub : forall x v,
+    (type_is_flat x) ->
+    (type_is_flat (type_abs v x))
+.
+
+(** Ladder Normal Form:
+    exhaustive application of -->distribute-ladder
+ *)
+Inductive type_is_lnf : ladder_type -> Prop :=
+  | LNF : forall x : ladder_type,
+  (not (exists y:ladder_type, x -->distribute-ladder y))
+  -> (type_is_lnf x)
+.
+
+(** Parameter Normal Form:
+    exhaustive application of -->condense-ladder
+*)
+Inductive type_is_pnf : ladder_type -> Prop :=
+  | PNF : forall x : ladder_type,
+  (not (exists y:ladder_type, x -->condense-ladder y))
+  -> (type_is_pnf x)
+.
+
+(** Any term in LNF either is flat, or is a ladder T1~T2 where T1 is flat and T2 is in LNF *)
+Lemma lnf_shape :
+  forall τ:ladder_type,
+  (type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_rung τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2)))
+.
+Proof.
+  intros τ H.
+  induction τ.
+  
+  left.
+  apply FlatUnit.
+  
+  left.
+  apply FlatId.
+  
+  left.
+  apply FlatVar.
+
+  left.
+  apply FlatNum.
+
+  admit.
+  admit.
+  admit.
+  admit.
+Admitted.
+
+(** every type has an equivalent LNF *)
+Lemma lnf_normalizing :
+  forall t, exists t', (t === t') /\ (type_is_lnf t').
+Proof.
+  intros.
+  destruct t.
+
+  exists type_unit.
+  split. apply L_Refl.
+  apply LNF.
+  admit.
+  
+  exists (type_id s).
+  split. apply L_Refl.
+  apply LNF.
+  admit.
+  admit.
+  
+  exists (type_num n).
+  split. apply L_Refl.
+  apply LNF.
+  admit.
+  
+  exists (type_abs s t).
+  split. apply L_Refl.
+  apply LNF.
+  
+Admitted.
+
+(** every type has an equivalent PNF *)
+Lemma pnf_normalizing :
+  forall t, exists t', (t === t') /\ (type_is_pnf t').
+Proof.
+Admitted.
+
+Lemma lnf_uniqueness :
+  forall t t' t'',
+  (t === t') /\ (type_is_lnf t') /\ (t === t'') /\ (type_is_lnf t'')
+  -> t = t'.
+Proof.
+Admitted.
+
+
+
+
+
+(**
+ *  Examples
+ *)
+
+Example example_flat_type :
+    (type_is_flat (type_app (type_id "PosInt") (type_num 10))).
+Proof.
+    apply FlatApp.
+    apply FlatId.
+    apply FlatNum.
+Qed.
+
+Example example_lnf_type :
+    (type_is_lnf
+    (type_rung (type_app (type_id "Seq") (type_id "Char"))
+               (type_app (type_id "Seq") (type_id "Byte")))).
+Proof.
+Admitted.
+
+Example example_type_eq :
+    (type_app (type_id "Seq") (type_rung (type_id "Char") (type_id "Byte")))
+    ===
+    (type_rung (type_app (type_id "Seq") (type_id "Char"))
+               (type_app (type_id "Seq") (type_id "Byte"))).
+Proof.
+  apply L_Distribute.
+  apply L_DistributeOverApp.
+Qed.
+
+
+End Equiv.