diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean
index 9645529e0..c3ee595b8 100644
--- a/hott/algebra/binary.hlean
+++ b/hott/algebra/binary.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2014-15 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.binary
@@ -8,7 +8,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 General properties of binary operations.
 -/
 
-open eq
+open eq.ops function
 
 namespace binary
   section
@@ -19,26 +19,29 @@ namespace binary
     local notation a ⁻¹  := inv a
     local notation 1     := one
 
-    definition commutative := ∀a b, a*b = b*a
-    definition associative := ∀a b c, (a*b)*c = a*(b*c)
-    definition left_identity := ∀a, 1 * a = a
-    definition right_identity := ∀a, a * 1 = a
-    definition left_inverse := ∀a, a⁻¹ * a = 1
-    definition right_inverse := ∀a, a * a⁻¹ = 1
-    definition left_cancelative := ∀a b c, a * b = a * c → b = c
-    definition right_cancelative := ∀a b c, a * b = c * b → a = c
+    definition commutative [reducible] := ∀a b, a * b = b * a
+    definition associative [reducible] := ∀a b c, (a * b) * c = a * (b * c)
+    definition left_identity [reducible] := ∀a, 1 * a = a
+    definition right_identity [reducible] := ∀a, a * 1 = a
+    definition left_inverse [reducible] := ∀a, a⁻¹ * a = 1
+    definition right_inverse [reducible] := ∀a, a * a⁻¹ = 1
+    definition left_cancelative [reducible] := ∀a b c, a * b = a * c → b = c
+    definition right_cancelative [reducible] := ∀a b c, a * b = c * b → a = c
 
-    definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b
-    definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b
-    definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b =  a
-    definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a
+    definition inv_op_cancel_left [reducible] := ∀a b, a⁻¹ * (a * b) = b
+    definition op_inv_cancel_left [reducible] := ∀a b, a * (a⁻¹ * b) = b
+    definition inv_op_cancel_right [reducible] := ∀a b, a * b⁻¹ * b =  a
+    definition op_inv_cancel_right [reducible] := ∀a b, a * b * b⁻¹ = a
 
     variable (op₂ : A → A → A)
 
     local notation a + b := op₂ a b
 
-    definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
-    definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
+    definition left_distributive [reducible] := ∀a b c, a * (b + c) = a * b + a * c
+    definition right_distributive [reducible] := ∀a b c, (a + b) * c = a * c + b * c
+
+    definition right_commutative [reducible] {B : Type} (f : B → A → B) := ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
+    definition left_commutative [reducible] {B : Type}  (f : A → B → B) := ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
   end
 
   section
@@ -47,13 +50,13 @@ namespace binary
     variable H_comm : commutative f
     variable H_assoc : associative f
     local infixl `*` := f
-    theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
+    theorem left_comm : left_commutative f :=
     take a b c, calc
       a*(b*c) = (a*b)*c  : H_assoc
         ...   = (b*a)*c  : H_comm
         ...   = b*(a*c)  : H_assoc
 
-    theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
+    theorem right_comm : right_commutative f :=
     take a b c, calc
       (a*b)*c = a*(b*c) : H_assoc
         ...   = a*(c*b) : H_comm
@@ -71,4 +74,11 @@ namespace binary
               ... = a*((b*c)*d) : H_assoc
   end
 
+  definition right_commutative_compose_right [reducible]
+    {A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (compose_right f g) :=
+  λ a b₁ b₂, !rcomm
+
+  definition left_commutative_compose_left [reducible]
+    {A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (compose_left f g) :=
+  λ a b₁ b₂, !lcomm
 end binary
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 96332d355..27e3d57de 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -8,7 +8,7 @@ Authors: Floris van Doorn, Jakob von Raumer
 
 import .iso types.pi
 
-open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext iso
+open function category eq prod prod.ops equiv is_equiv sigma sigma.ops is_trunc funext iso
 open pi
 
 structure functor (C D : Precategory) : Type :=
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index f04050a50..3af17582e 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -9,27 +9,27 @@ Authors: Leonardo de Moura
 prelude
 import init.reserved_notation
 
+/- not -/
+
 definition not.{l} (a : Type.{l}) := a → empty.{l}
 prefix `¬` := not
 
-definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b :=
+definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=
 empty.rec (λ e, b) (H₂ H₁)
 
 definition mt {a b : Type} (H₁ : a → b) (H₂ : ¬b) : ¬a :=
 assume Ha : a, absurd (H₁ Ha) H₂
 
-/- not -/
-
 protected definition not_empty : ¬ empty :=
 assume H : empty, H
 
 definition not_not_intro {a : Type} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna
 
-definition not.intro {a : Type} (H : a → empty) : ¬a := H
-
 definition not.elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂
 
+definition not.intro {a : Type} (H : a → empty) : ¬a := H
+
 definition not_not_of_not_implies {a b : Type} (H : ¬(a → b)) : ¬¬a :=
 assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
 
@@ -42,8 +42,7 @@ notation a = b := eq a b
 definition rfl {A : Type} {a : A} := eq.refl a
 
 namespace eq
-  variables {A : Type}
-  variables {a b c a' : A}
+  variables {A : Type} {a b c : A}
 
   definition subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
   eq.rec H₂ H₁
@@ -61,7 +60,7 @@ namespace eq
   end ops
 end eq
 
-theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
+definition congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
 eq.subst H₁ (eq.subst H₂ rfl)
 
 section
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index 88384957f..c63bcca5f 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -7,7 +7,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
 -/
 
 prelude
-import .logic .num .wf
+import .num .wf
 
 -- Empty type
 -- ----------
@@ -147,3 +147,126 @@ namespace prod
   end
 
 end prod
+
+/- logic using prod and sum -/
+
+variables {a b c d : Type}
+open prod sum unit
+
+/- prod -/
+
+definition not_prod_of_not_left (b : Type) (Hna : ¬a) : ¬(a × b) :=
+assume H : a × b, absurd (pr1 H) Hna
+
+definition not_prod_of_not_right (a : Type) {b : Type} (Hnb : ¬b) : ¬(a × b) :=
+assume H : a × b, absurd (pr2 H) Hnb
+
+definition prod.swap (H : a × b) : b × a :=
+pair (pr2 H) (pr1 H)
+
+definition prod_of_prod_of_imp_of_imp (H₁ : a × b) (H₂ : a → c) (H₃ : b → d) : c × d :=
+by cases H₁ with aa bb; exact (H₂ aa, H₃ bb)
+
+definition prod_of_prod_of_imp_left (H₁ : a × c) (H : a → b) : b × c :=
+by cases H₁ with aa cc; exact (H aa, cc)
+
+definition prod_of_prod_of_imp_right (H₁ : c × a) (H : a → b) : c × b :=
+by cases H₁ with cc aa; exact (cc, H aa)
+
+definition prod.comm : a × b ↔ b × a :=
+iff.intro (λH, prod.swap H) (λH, prod.swap H)
+
+definition prod.assoc : (a × b) × c ↔ a × (b × c) :=
+iff.intro
+  (assume H, pair
+    (pr1 (pr1 H))
+    (pair (pr2 (pr1 H)) (pr2 H)))
+  (assume H, pair
+    (pair (pr1 H) (pr1 (pr2 H)))
+    (pr2 (pr2 H)))
+
+definition prod_unit (a : Type) : a × unit ↔ a :=
+iff.intro (assume H, pr1 H) (assume H, pair H star)
+
+definition unit_prod (a : Type) : unit × a ↔ a :=
+iff.intro (assume H, pr2 H) (assume H, pair star H)
+
+definition prod_empty.{l} (a : Type.{l}) : a × empty.{l} ↔ empty.{l} :=
+iff.intro (assume H, pr2 H) (assume H, !empty.elim H)
+
+definition empty_prod (a : Type) : empty × a ↔ empty :=
+iff.intro (assume H, pr1 H) (assume H, !empty.elim H)
+
+definition prod_self (a : Type) : a × a ↔ a :=
+iff.intro (assume H, pr1 H) (assume H, pair H H)
+
+/- sum -/
+
+definition not_sum (Hna : ¬a) (Hnb : ¬b) : ¬(a ⊎ b) :=
+assume H : a ⊎ b, sum.rec_on H
+  (assume Ha, absurd Ha Hna)
+  (assume Hb, absurd Hb Hnb)
+
+definition sum_of_sum_of_imp_of_imp (H₁ : a ⊎ b) (H₂ : a → c) (H₃ : b → d) : c ⊎ d :=
+sum.rec_on H₁
+  (assume Ha : a, sum.inl (H₂ Ha))
+  (assume Hb : b, sum.inr (H₃ Hb))
+
+definition sum_of_sum_of_imp_left (H₁ : a ⊎ c) (H : a → b) : b ⊎ c :=
+sum.rec_on H₁
+  (assume H₂ : a, sum.inl (H H₂))
+  (assume H₂ : c, sum.inr H₂)
+
+definition sum_of_sum_of_imp_right (H₁ : c ⊎ a) (H : a → b) : c ⊎ b :=
+sum.rec_on H₁
+  (assume H₂ : c, sum.inl H₂)
+  (assume H₂ : a, sum.inr (H H₂))
+
+definition sum.elim3 (H : a ⊎ b ⊎ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
+sum.rec_on H Ha (assume H₂, sum.rec_on H₂ Hb Hc)
+
+definition sum_resolve_right (H₁ : a ⊎ b) (H₂ : ¬a) : b :=
+sum.rec_on H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb)
+
+definition sum_resolve_left (H₁ : a ⊎ b) (H₂ : ¬b) : a :=
+sum.rec_on H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
+
+definition sum.swap (H : a ⊎ b) : b ⊎ a :=
+sum.rec_on H (assume Ha, sum.inr Ha) (assume Hb, sum.inl Hb)
+
+definition sum.comm : a ⊎ b ↔ b ⊎ a :=
+iff.intro (λH, sum.swap H) (λH, sum.swap H)
+
+definition sum.assoc : (a ⊎ b) ⊎ c ↔ a ⊎ (b ⊎ c) :=
+iff.intro
+  (assume H, sum.rec_on H
+    (assume H₁, sum.rec_on H₁
+      (assume Ha, sum.inl Ha)
+      (assume Hb, sum.inr (sum.inl Hb)))
+    (assume Hc, sum.inr (sum.inr Hc)))
+  (assume H, sum.rec_on H
+    (assume Ha, (sum.inl (sum.inl Ha)))
+    (assume H₁, sum.rec_on H₁
+      (assume Hb, sum.inl (sum.inr Hb))
+      (assume Hc, sum.inr Hc)))
+
+definition sum_unit (a : Type) : a ⊎ unit ↔ unit :=
+iff.intro (assume H, star) (assume H, sum.inr H)
+
+definition unit_sum (a : Type) : unit ⊎ a ↔ unit :=
+iff.intro (assume H, star) (assume H, sum.inl H)
+
+definition sum_empty (a : Type) : a ⊎ empty ↔ a :=
+iff.intro
+  (assume H, sum.rec_on H (assume H1 : a, H1) (assume H1 : empty, !empty.elim H1))
+  (assume H, sum.inl H)
+
+definition empty_sum (a : Type) : empty ⊎ a ↔ a :=
+iff.intro
+  (assume H, sum.rec_on H (assume H1 : empty, !empty.elim H1) (assume H1 : a, H1))
+  (assume H, sum.inr H)
+
+definition sum_self (a : Type) : a ⊎ a ↔ a :=
+iff.intro
+  (assume H, sum.rec_on H (assume H1, H1) (assume H1, H1))
+  (assume H, sum.inl H)
diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean
new file mode 100644
index 000000000..217ff0974
--- /dev/null
+++ b/hott/types/nat/basic.hlean
@@ -0,0 +1,291 @@
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.nat.basic
+Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
+
+Basic operations on the natural numbers.
+
+-/
+import algebra.binary
+open eq sum sigma prod binary
+
+namespace nat
+
+/- a variant of add, defined by recursion on the first argument -/
+
+definition addl (x y : ℕ) : ℕ :=
+nat.rec y (λ n r, succ r) x
+infix `⊕`:65 := addl
+
+theorem addl_succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
+nat.rec_on n
+  rfl
+  (λ n₁ ih, calc
+    succ n₁ ⊕ succ m = succ (n₁ ⊕ succ m)   : rfl
+             ...     = succ (succ (n₁ ⊕ m)) : ih
+             ...     = succ (succ n₁ ⊕ m)   : rfl)
+
+theorem add_eq_addl (x : ℕ) : ∀y, x + y = x ⊕ y :=
+nat.rec_on x
+  (λ y, nat.rec_on y
+    rfl
+    (λ y₁ ih, calc
+      zero + succ y₁ = succ (zero + y₁)  : rfl
+              ...    = succ (zero ⊕ y₁) : {ih}
+              ...    = zero ⊕ (succ y₁) : rfl))
+  (λ x₁ ih₁ y, nat.rec_on y
+    (calc
+      succ x₁ + zero  = succ (x₁ + zero)  : rfl
+                  ... = succ (x₁ ⊕ zero) : {ih₁ zero}
+                  ... = succ x₁ ⊕ zero   : rfl)
+    (λ y₁ ih₂, calc
+      succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
+                   ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
+                   ...  = succ x₁ ⊕ succ y₁   : addl_succ_right))
+
+/- successor and predecessor -/
+
+theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
+by contradiction
+
+-- add_rewrite succ_ne_zero
+
+theorem pred_zero : pred 0 = 0 :=
+rfl
+
+theorem pred_succ (n : ℕ) : pred (succ n) = n :=
+rfl
+
+theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ⊎ n = succ (pred n) :=
+nat.rec_on n
+  (sum.inl rfl)
+  (take m IH, sum.inr
+    (show succ m = succ (pred (succ m)), from ap succ !pred_succ⁻¹))
+
+theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : Σk : ℕ, n = succ k :=
+⟨_, sum.rec_on (eq_zero_or_eq_succ_pred n) (λH2, absurd H2 H) function.id⟩
+
+theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m :=
+lift.down (nat.no_confusion H (λe, e))
+
+theorem succ_ne_self {n : ℕ} : succ n ≠ n :=
+nat.rec_on n
+  (take H : 1 = 0,
+    have ne : 1 ≠ 0, from !succ_ne_zero,
+    absurd H ne)
+  (take k IH H, IH (succ_inj H))
+
+theorem discriminate {B : Type} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
+have H : n = n → B, from nat.cases_on n H1 H2,
+H rfl
+
+theorem two_step_induction_on {P : ℕ → Type} (a : ℕ) (H1 : P 0) (H2 : P 1)
+    (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
+have stronger : P a × P (succ a), from
+  nat.rec_on a
+    (H1, H2)
+    (take k IH,
+      have IH1 : P k, from pr1 IH,
+      have IH2 : P (succ k), from pr2 IH,
+        (IH2, (H3 k IH1 IH2))),
+  pr1 stronger
+
+theorem sub_induction {P : ℕ → ℕ → Type} (n m : ℕ) (H1 : ∀m, P 0 m)
+   (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m :=
+have general : ∀m, P n m, from nat.rec_on n
+  (take m : ℕ, H1 m)
+  (take k : ℕ,
+    assume IH : ∀m, P k m,
+    take m : ℕ,
+    nat.cases_on m (H2 k) (take l, (H3 k l (IH l)))),
+general m
+
+/- addition -/
+
+theorem add_zero (n : ℕ) : n + 0 = n :=
+rfl
+
+theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) :=
+rfl
+
+theorem zero_add (n : ℕ) : 0 + n = n :=
+nat.rec_on n
+    !add_zero
+    (take m IH, show 0 + succ m = succ m, from
+      calc
+        0 + succ m = succ (0 + m) : add_succ
+               ... = succ m       : IH)
+
+theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) :=
+nat.rec_on m
+    (!add_zero ▸ !add_zero)
+    (take k IH, calc
+      succ n + succ k = succ (succ n + k)    : add_succ
+                  ... = succ (succ (n + k))  : IH
+                  ... = succ (n + succ k)    : add_succ)
+
+theorem add.comm (n m : ℕ) : n + m = m + n :=
+nat.rec_on m
+    (!add_zero ⬝ !zero_add⁻¹)
+    (take k IH, calc
+        n + succ k = succ (n+k)   : add_succ
+               ... = succ (k + n) : IH
+               ... = succ k + n   : succ_add)
+
+theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
+!succ_add ⬝ !add_succ⁻¹
+
+theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) :=
+nat.rec_on k
+    (!add_zero ▸ !add_zero)
+    (take l IH,
+      calc
+        (n + m) + succ l = succ ((n + m) + l)  : add_succ
+                     ... = succ (n + (m + l))  : IH
+                     ... = n + succ (m + l)    : add_succ
+                     ... = n + (m + succ l)    : add_succ)
+
+theorem add.left_comm (n m k : ℕ) : n + (m + k) = m + (n + k) :=
+left_comm add.comm add.assoc n m k
+
+theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m :=
+right_comm add.comm add.assoc n m k
+
+theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k :=
+nat.rec_on n
+  (take H : 0 + m = 0 + k,
+    !zero_add⁻¹ ⬝ H ⬝ !zero_add)
+  (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
+    have H2 : succ (n + m) = succ (n + k),
+    from calc
+      succ (n + m) = succ n + m   : succ_add
+               ... = succ n + k   : H
+               ... = succ (n + k) : succ_add,
+    have H3 : n + m = n + k, from succ_inj H2,
+    IH H3)
+
+theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
+have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm,
+  add.cancel_left H2
+
+theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 :=
+nat.rec_on n
+  (take (H : 0 + m = 0), rfl)
+  (take k IH,
+    assume H : succ k + m = 0,
+    absurd
+      (show succ (k + m) = 0, from calc
+         succ (k + m) = succ k + m : succ_add
+                  ... = 0          : H)
+      !succ_ne_zero)
+
+theorem eq_zero_of_add_eq_zero_left {n m : ℕ} (H : n + m = 0) : m = 0 :=
+eq_zero_of_add_eq_zero_right (!add.comm ⬝ H)
+
+theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 × m = 0 :=
+(eq_zero_of_add_eq_zero_right H, eq_zero_of_add_eq_zero_left H)
+
+theorem add_one (n : ℕ) : n + 1 = succ n :=
+!add_zero ▸ !add_succ
+
+theorem one_add (n : ℕ) : 1 + n = succ n :=
+!zero_add ▸ !succ_add
+
+/- multiplication -/
+
+theorem mul_zero (n : ℕ) : n * 0 = 0 :=
+rfl
+
+theorem mul_succ (n m : ℕ) : n * succ m = n * m + n :=
+rfl
+
+-- commutativity, distributivity, associativity, identity
+
+theorem zero_mul (n : ℕ) : 0 * n = 0 :=
+nat.rec_on n
+  !mul_zero
+  (take m IH, !mul_succ ⬝ !add_zero ⬝ IH)
+
+theorem succ_mul (n m : ℕ) : (succ n) * m = (n * m) + m :=
+nat.rec_on m
+  (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹)
+  (take k IH, calc
+    succ n * succ k = succ n * k + succ n   : mul_succ
+                ... = n * k + k + succ n    : IH
+                ... = n * k + (k + succ n)  : add.assoc
+                ... = n * k + (succ n + k)  : add.comm
+                ... = n * k + (n + succ k)  : succ_add_eq_succ_add
+                ... = n * k + n + succ k    : add.assoc
+                ... = n * succ k + succ k   : mul_succ)
+
+theorem mul.comm (n m : ℕ) : n * m = m * n :=
+nat.rec_on m
+  (!mul_zero ⬝ !zero_mul⁻¹)
+  (take k IH, calc
+    n * succ k = n * k + n    : mul_succ
+           ... = k * n + n    : IH
+           ... = (succ k) * n : succ_mul)
+
+theorem mul.right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k :=
+nat.rec_on k
+  (calc
+    (n + m) * 0 = 0             : mul_zero
+            ... = 0 + 0         : add_zero
+            ... = n * 0 + 0     : mul_zero
+            ... = n * 0 + m * 0 : mul_zero)
+  (take l IH, calc
+    (n + m) * succ l = (n + m) * l + (n + m)    : mul_succ
+                 ... = n * l + m * l + (n + m)  : IH
+                 ... = n * l + m * l + n + m    : add.assoc
+                 ... = n * l + n + m * l + m    : add.right_comm
+                 ... = n * l + n + (m * l + m)  : add.assoc
+                 ... = n * succ l + (m * l + m) : mul_succ
+                 ... = n * succ l + m * succ l  : mul_succ)
+
+theorem mul.left_distrib (n m k : ℕ) : n * (m + k) = n * m + n * k :=
+calc
+  n * (m + k) = (m + k) * n    : mul.comm
+          ... = m * n + k * n  : mul.right_distrib
+          ... = n * m + k * n  : mul.comm
+          ... = n * m + n * k  : mul.comm
+
+theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) :=
+nat.rec_on k
+  (calc
+    (n * m) * 0 = n * (m * 0) : mul_zero)
+  (take l IH,
+    calc
+      (n * m) * succ l = (n * m) * l + n * m : mul_succ
+                   ... = n * (m * l) + n * m : IH
+                   ... = n * (m * l + m)     : mul.left_distrib
+                   ... = n * (m * succ l)    : mul_succ)
+
+theorem mul_one (n : ℕ) : n * 1 = n :=
+calc
+  n * 1 = n * 0 + n : mul_succ
+    ... = 0 + n     : mul_zero
+    ... = n         : zero_add
+
+theorem one_mul (n : ℕ) : 1 * n = n :=
+calc
+  1 * n = n * 1 : mul.comm
+    ... = n     : mul_one
+
+theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : ℕ} : n * m = 0 → n = 0 ⊎ m = 0 :=
+nat.cases_on n
+  (assume H, sum.inl rfl)
+  (take n',
+    nat.cases_on m
+      (assume H, sum.inr rfl)
+      (take m',
+        assume H : succ n' * succ m' = 0,
+        absurd
+          ((calc
+            0 = succ n' * succ m' : H
+             ... = succ n' * m' + succ n' : mul_succ
+             ... = succ (succ n' * m' + n') : add_succ)⁻¹)
+          !succ_ne_zero))
+
+end nat
diff --git a/script/port.pl b/script/port.pl
new file mode 100755
index 000000000..fdc8387d8
--- /dev/null
+++ b/script/port.pl
@@ -0,0 +1,111 @@
+#!/usr/bin/env perl
+
+# SEE ALSO THE DOCUMENTATION IN port.sh
+#
+# This perl script is for porting files from the standard library to the HoTT library
+#
+# (1) create a file "port.txt", with a list of entries "foo:bar" (or "foo;bar"),
+#     one per line
+# (2) put this script and port.txt in the same directory, and make sure
+#     the script is executable.
+# (3) use "[path]/port.pl [path]/source [path]/target" to do the renaming.
+#     On a Unix system, at least, you can use wildcards.
+#
+# -> You can write foo;bar to replace all occurrences,
+#    even if they are a substring of a longer expression (useful for e.g. notation)
+#
+# Example: if you put rename.pl and port.txt in lean/library, then
+# from that directory type
+#
+#   ./rename.pl data/nat/*.lean
+#
+# to do all the renamings in data/nat. Alternative, change to that directory,
+# and type
+#
+# ../../rename.pl *.lean
+#
+# Notes:
+#
+# We assume identifiers have only letters, numbers, _, or "'" or ".".
+#
+# See http://perldoc.perl.org/perlfaq5.html, "How can I use Perl's i option from
+# within a program?" for information on the method used to change a file in place.
+#
+# See also http://perldoc.perl.org/File/Find.html for information on how to write
+# a subroutine that will traverse a directory tree.
+#
+use strict;
+use warnings;
+use Cwd 'abs_path';
+use File::Basename;
+use File::Spec::Functions;
+use File::Copy;
+use feature 'unicode_strings';
+
+# the global list of renamings
+my %renamings = ();
+my %literalrenamings = ();
+my %literalrenamings2 = ();
+
+# get the list of renamings from the file
+sub get_renamings {
+    if (scalar(@ARGV)%2==1) {die "ERROR: odd number of arguments provided"}
+    %literalrenamings2 = @ARGV;
+    my $fullname = catfile(dirname(abs_path($0)), "port.txt");
+    open (my $renaming_file, "<", $fullname) or die $!;
+    while (<$renaming_file>) {
+	if (/([\w'.]+)[:]([\w'.]+)\n/) {
+	    $renamings{$1} = $2;
+	} elsif (/(.+)[;](.+)\n/) {
+	    $literalrenamings{$1} = $2;
+	}
+    }
+    close $renaming_file or die $!;
+}
+
+# print them out - for debugging
+sub show_renamings {
+    foreach my $key (keys %renamings) {
+	print $key, " => ", $renamings{$key}, "\n";
+    }
+    print "\n";
+    foreach my $lkey (keys %literalrenamings2) {
+	print $lkey, " -> ", $literalrenamings2{$lkey}, "\n";
+    }
+    foreach my $lkey (keys %literalrenamings) {
+	print $lkey, " -> ", $literalrenamings{$lkey}, "\n";
+    }
+}
+
+# rename all identifiers a file; original goes in file.orig
+sub rename_in_file {
+    my $filename = shift;
+    local($^I, @ARGV) = ('.orig', $filename);
+    while (<>) {
+	foreach my $lkey (keys %literalrenamings2) {
+	    # replace all instances of lkey
+	    if (/$lkey/) {print STDOUT "renamed ", $lkey, "\n"; }
+	    # else {print STDOUT "WARNING: didn't rename ", $lkey, " to ", $literalrenamings2{$lkey}, "\n";}
+	    s/$lkey/$literalrenamings2{$lkey}/g
+	}
+	foreach my $key (keys %renamings) {
+	    # replace instances of key, not preceeded by a letter, and not
+	    # followed by a letter, number, or '
+	    s/(?<![a-zA-z])$key(?![\w'])/$renamings{$key}/g;
+	}
+	foreach my $lkey (keys %literalrenamings) {
+	    # replace all instances of lkey
+	    s/$lkey/$literalrenamings{$lkey}/g;
+	}
+	print;
+    }
+}
+
+my $oldfile = shift;
+my $newfile = shift;
+print "copying ", $oldfile, " to ",$newfile, ".\n";
+copy($oldfile,$newfile) or die "Copy failed: $!";
+get_renamings;
+# show_renamings;
+rename_in_file $newfile;
+unlink $newfile.".orig";
diff --git a/script/port.sh b/script/port.sh
new file mode 100755
index 000000000..ff2d19aa1
--- /dev/null
+++ b/script/port.sh
@@ -0,0 +1,26 @@
+# usage:
+# Make sure port.sh and port.pl are executable (chmod u+x port.pl port.sh)
+# in the scripts directory, type ./port.sh to port the files specified below
+# from the standard library to the HoTT library
+# This file requires both port.pl and port.txt to be in the scripts folder
+#
+# WARNING: This will overwrite all destination files without warning!
+#
+# to add a new file to port to this file, add a new line of the form 
+#
+#  ./port.pl ../library/path/to/source.lean ../hott/path/to/destination.hlean "from1" "to1" "from2" "to2" [...]
+#
+# This will port the file ../library/path/to/source.lean to ../hott/path/to/destination.hlean 
+# renaming core definitions form the standard library to core definitions in the HoTT library. 
+# These renamings are specified in port.txt. Additional changes can be added by the extra arguments.
+# The extra arguments will replace "fromi" by "toi" in the specified file, 
+# before doing any other renamings.
+#
+# Note: parentheses (and other characters with a special meaning in regular expressions)
+# have to be escaped
+
+now=$(date +"%B %d, %Y")
+./port.pl ../library/data/nat/basic.lean ../hott/types/nat/basic.hlean "Module: data.nat.basic" "Module: types.nat.basic
+(Ported from standard library file data.nat.basic on $now)" "import logic.connectives data.num algebra.binary algebra.ring" "import algebra.binary" "open binary eq.ops" "open core prod binary" "nat.no_confusion H \(λe, e\)" "lift.down (nat.no_confusion H (λe, e))"
+
+# ./port.pl ../library/logic/connectives.lean ../hott/logic.hlean
diff --git a/script/port.txt b/script/port.txt
new file mode 100644
index 000000000..f18d4727c
--- /dev/null
+++ b/script/port.txt
@@ -0,0 +1,21 @@
+Prop:Type
+theorem:definition
+induction:rec
+induction_on:rec_on
+∨;⊎
+or.elim:sum.rec_on
+or.inl:sum.inl
+or.inr:sum.inr
+∧;×
+and.intro:pair
+and.left:
+and.elim_left:pr1
+and.elim_right:pr2
+∃;Σ
+exists.intro:sigma.mk
+congr_arg:ap
+or_resolve_right:sum_resolve_right
+or_resolve_left:sum_resolve_left
+true:unit
+trivial:star
+false:empty
diff --git a/script/rename.pl b/script/rename.pl
index e1ecc9faf..08726f6fb 100755
--- a/script/rename.pl
+++ b/script/rename.pl
@@ -2,14 +2,17 @@
 
 # This perl script is for doing batch renamings of identifiers. To use it:
 #
-# (1) create a file "renamings.txt", with a list of entries "foo:bar",
+# (1) create a file "renamings.txt", with a list of entries "foo:bar" (or "foo;bar"),
 #     one per line
 # (2) put this script and renamings.txt in the same directory, and make sure
 #     the script is executable.
 # (3) use "[path]/rename.pl [path]/file" to do the renaming.
 #     On a Unix system, at least, you can use wildcards.
 #
-# Example: if you put rename.pl and renamings.txt in lean/library, then 
+# -> You can write foo;bar to replace all occurrences,
+#    even if they are a substring of a longer expression (useful for e.g. notation)
+#
+# Example: if you put rename.pl and renamings.txt in lean/library, then
 # from that directory type
 #
 #   ./rename.pl data/nat/*.lean
@@ -23,7 +26,7 @@
 #
 # We assume identifiers have only letters, numbers, _, or "'" or ".".
 #
-# See http://perldoc.perl.org/perlfaq5.html, "How can I use Perl's i option from 
+# See http://perldoc.perl.org/perlfaq5.html, "How can I use Perl's i option from
 # within a program?" for information on the method used to change a file in place.
 #
 # See also http://perldoc.perl.org/File/Find.html for information on how to write
@@ -37,6 +40,7 @@ use File::Spec::Functions;
 
 # the global list of renamings
 my %renamings = ();
+my %literalrenamings = (); # renamings which have
 
 # get the list of renamings from the file
 sub get_renamings {
@@ -45,7 +49,10 @@ sub get_renamings {
     while (<$renaming_file>) {
 	if (/([\w'.]+)[:]([\w'.]+)\n/) {
 	    $renamings{$1} = $2;
-	}
+	} else
+      { if (/(.+)[;](.+)\n/) {
+	    $literalrenamings{$1} = $2;
+	  }}
     }
     close $renaming_file or die $!;
 }
@@ -55,6 +62,10 @@ sub show_renamings {
     foreach my $key (keys %renamings) {
 	print $key, " => ", $renamings{$key}, "\n";
     }
+    print "\n";
+    foreach my $lkey (keys %literalrenamings) {
+	print $lkey, " -> ", $literalrenamings{$lkey}, "\n";
+    }
 }
 
 # rename all identifiers a file; original goes in file.orig
@@ -64,9 +75,13 @@ sub rename_in_file {
     while (<>) {
 	foreach my $key (keys %renamings) {
 	    # replace instances of key, not preceeded by a letter, and not
-	    # followed by a letter, number, ', or .
+	    # followed by a letter, number, or '
 	    s/(?<![a-zA-z])$key(?![\w'])/$renamings{$key}/g;
 	}
+	foreach my $lkey (keys %literalrenamings) {
+	    # replace all instances of lkey
+	    s/$lkey/$literalrenamings{$lkey}/g;
+	}
 	print;
     }
 }
@@ -76,4 +91,3 @@ get_renamings;
 foreach (@ARGV) {
     rename_in_file $_;
 }
-