diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index 18fc19a77..0bb7825eb 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -24,13 +24,13 @@ structure semigroup [class] (A : Type) extends has_mul A :=
 
 attribute semigroup.is_hset_carrier [instance]
 
-theorem mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
+definition mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
 !semigroup.mul_assoc
 
 structure comm_semigroup [class] (A : Type) extends semigroup A :=
 (mul_comm : Πa b, mul a b = mul b a)
 
-theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
+definition mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
 !comm_semigroup.mul_comm
 
 theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
@@ -51,7 +51,7 @@ abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
 structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
 (mul_right_cancel : Πa b c, mul a b = mul c b → a = c)
 
-theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
+definition mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
   a * b = c * b → a = c :=
 !right_cancel_semigroup.mul_right_cancel
 
@@ -65,13 +65,13 @@ structure add_semigroup [class] (A : Type) extends has_add A :=
 
 attribute add_semigroup.is_hset_carrier [instance]
 
-theorem add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
+definition add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
 !add_semigroup.add_assoc
 
 structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_comm : Πa b, add a b = add b a)
 
-theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
+definition add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
 !add_comm_semigroup.add_comm
 
 theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
@@ -84,7 +84,7 @@ binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
 structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_left_cancel : Πa b c, add a b = add a c → b = c)
 
-theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
+definition add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
   a + b = a + c → b = c :=
 !add_left_cancel_semigroup.add_left_cancel
 
@@ -93,7 +93,7 @@ abbreviation eq_of_add_eq_add_left := @add.left_cancel
 structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_right_cancel : Πa b c, add a b = add c b → a = c)
 
-theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
+definition add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
   a + b = c + b → a = c :=
 !add_right_cancel_semigroup.add_right_cancel
 
@@ -104,9 +104,9 @@ abbreviation eq_of_add_eq_add_right := @add.right_cancel
 structure monoid [class] (A : Type) extends semigroup A, has_one A :=
 (one_mul : Πa, mul one a = a) (mul_one : Πa, mul a one = a)
 
-theorem one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul
+definition one_mul [s : monoid A] (a : A) : 1 * a = a := !monoid.one_mul
 
-theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
+definition mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
 
 structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 
@@ -115,9 +115,9 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
 (zero_add : Πa, add zero a = a) (add_zero : Πa, add a zero = a)
 
-theorem zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
+definition zero_add [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
 
-theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
+definition add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
 
 structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
 
@@ -160,7 +160,7 @@ section group
   variable [s : group A]
   include s
 
-  theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
+  definition mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
 
   theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
   by rewrite [-mul.assoc, mul.left_inv, one_mul]
diff --git a/hott/algebra/port.md b/hott/algebra/port.md
index db5b75e57..d4c1a157d 100644
--- a/hott/algebra/port.md
+++ b/hott/algebra/port.md
@@ -3,9 +3,18 @@ We port a lot of algebra files from the standard library to the HoTT library.
 Port instructions:
 - use the script port.pl in scripts/ to port the file. e.g. execute the following in the `scripts` folder: `./port.pl ../library/algebra/lattice.lean ../hott/algebra/lattice.hlean`
 - remove imports starting with `data.` or `logic.` (sometimes you need to replace a `data.` import by the corresponding `types.` import)
-- All of the algebraic hierarchy is in the algebra namespace in the HoTT library.
 - Open namespaces `eq` and `algebra` if needed
 - (optional) add option `set_option class.force_new true`
 - fix all remaining errors. Typical errors include
   - Replacing "and" by "prod" in comments
   - and.intro is replaced by prod.intro, which should be prod.mk.
+
+Currently, the following differences exist between the two libraries, relevant to porting:
+- All of the algebraic hierarchy is in the algebra namespace in the HoTT library (on top-level in the standard library).
+- The projections "zero" and "one" are reducible in HoTT. This was needed to allow type class inferences to infer
+```
+H : is_trunc 0 A |- is_trunc (succ (-1)) A
+H : is_trunc 1 A |- is_trunc (succ 0) A
+```
+- Projections of most algebraic structures are definitions instead of theorems in HoTT
+- Basic properties of `nat.add` have a simpler proof in HoTT (so that it computes better)
\ No newline at end of file
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index faf112e86..3657b2aa5 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -328,7 +328,7 @@ end
 structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
 (eq_zero_sum_eq_zero_of_mul_eq_zero : Πa b, mul a b = zero → a = zero ⊎ b = zero)
 
-theorem eq_zero_sum_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A}
+definition eq_zero_sum_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A}
     (H : a * b = 0) :
   a = 0 ⊎ b = 0 := !no_zero_divisors.eq_zero_sum_eq_zero_of_mul_eq_zero H
 
diff --git a/hott/function.hlean b/hott/function.hlean
index 2ac85a9e4..5b60eac26 100644
--- a/hott/function.hlean
+++ b/hott/function.hlean
@@ -37,19 +37,6 @@ structure is_conditionally_constant [class] (f : A → B) :=
   (g : ∥A∥ → B)
   (eq : Π(a : A), f a = g (tr a))
 
--- structure is_retract (g : A → B) :=
---   (X Y : Type)
---   (f : X → Y)
---   (s : A → X)
---   (r : X → A)
---   (s' : B → Y)
---   (r' : Y → B)
---   (R : Πa, r (s a) = a)
---   (R' : Πb, r' (s' b) = b)
---   (L : Πa, f (s a) = s' (g a))
---   (K : Πx, g (r x) = r' (f x))
---   (H : Πa, square (K (s a)) (R' (g a))⁻¹ (ap g (R a)) (ap r' (L a)))
-
 namespace function
 
   abbreviation sect          [unfold 4] := @is_retraction.sect
@@ -198,40 +185,7 @@ namespace function
   is_constant.mk b (λv, by induction v with a p;exact p)
 
   definition is_embedding_of_is_hprop_fiber [H : Π(b : B), is_hprop (fiber f b)] : is_embedding f :=
-  begin
-    intro a a',
-    fapply adjointify,
-    { intro p, exact ap point (is_hprop.elim (fiber.mk a p) (fiber.mk a' idp))},
-    { exact abstract begin
-      intro p, rewrite [-ap_compose],
-      apply @is_constant.eq _ _ _ (is_constant_ap (f ∘ point) (fiber.mk a p) (fiber.mk a' idp))
-      end end },
-    { intro p, induction p, rewrite [▸*,is_hprop_elim_self]},
-  end
-
-  -- definition is_embedding_of_is_section_inv' [H : is_section f] {a : A} {b : B} (p : f a = b) :
-  --   a = retr f b :=
-  -- (left_inverse f a)⁻¹ ⬝ ap (retr f) p
-
-  -- definition is_embedding_of_is_section_inv [H : is_section f] {a a' : A} (p : f a = f a') :
-  --   a = a' :=
-  -- is_embedding_of_is_section_inv' f p ⬝ left_inverse f a'
-
-  -- definition is_embedding_of_is_section [constructor] [instance] [H : is_section f]
-  --   : is_embedding f :=
-  -- begin
-  --   intro a a',
-  --   fapply adjointify,
-  --   { exact is_embedding_of_is_section_inv f},
-  --   { exact abstract begin
-  --     assert H2 : Π {b : B} (p : f a = b), ap f (is_embedding_of_is_section_inv' f p) = p ⬝ _,
-  --     { }
-  --           -- intro p, rewrite [+ap_con,-ap_compose],
-  --           -- check_expr natural_square (left_inverse f),
-  --           -- induction H with g q, esimp,
-  --           end end },
-  --   { intro p, induction p, esimp, apply con.left_inv},
-  -- end
+  is_embedding_of_is_hprop_fun _
 
   definition is_retraction_of_is_equiv [instance] [H : is_equiv f] : is_retraction f :=
   is_retraction.mk f⁻¹ (right_inv f)
@@ -303,6 +257,8 @@ namespace function
       is_surjective_of_is_equiv
       is_equiv_equiv_is_embedding_times_is_surjective
     are in types.trunc
+
+    See types.arrow_2 for retractions
   -/
 
 end function
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 387f2b618..3f28fff11 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -42,6 +42,11 @@ empty.rec _ H
 infix = := eq
 definition rfl {A : Type} {a : A} := eq.refl a
 
+/-
+  These notions are here only to make porting from the standard library easier.
+  They are defined again in init/path.hlean, and those definitions will be used
+  throughout the HoTT-library. That's why the notation for eq below is only local.
+-/
 namespace eq
   variables {A : Type} {a b c : A}
 
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index 369ebd8a6..5b0af1b13 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -22,8 +22,8 @@ structure has_dvd.{l} [class] (A : Type.{l}) : Type.{l+1} := (dvd : A → A →
 structure has_le.{l}  [class] (A : Type.{l}) : Type.{l+1} := (le : A → A → Type.{l})
 structure has_lt.{l}  [class] (A : Type.{l}) : Type.{l+1} := (lt : A → A → Type.{l})
 
-definition zero [reducible] {A : Type} [s : has_zero A] : A:= has_zero.zero A
-definition one              {A : Type} [s : has_one A]  : A            := has_one.one A
+definition zero [reducible] {A : Type} [s : has_zero A] : A            := has_zero.zero A
+definition one  [reducible] {A : Type} [s : has_one A]  : A            := has_one.one A
 definition add              {A : Type} [s : has_add A]  : A → A → A    := has_add.add
 definition mul              {A : Type} [s : has_mul A]  : A → A → A    := has_mul.mul
 definition sub              {A : Type} [s : has_sub A]  : A → A → A    := has_sub.sub
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 7c6c4bcd7..f95e47414 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -13,7 +13,7 @@ Ported from Coq HoTT.
 prelude
 import .nat .logic .equiv .pathover
 open eq nat sigma unit
-set_option class.force_new true
+--set_option class.force_new true
 
 namespace is_trunc
 
@@ -42,10 +42,10 @@ namespace is_trunc
   notation `ℕ₋₂` := trunc_index
 
   namespace trunc_index
-  definition add (n m : trunc_index) : trunc_index :=
+  definition add [reducible] (n m : trunc_index) : trunc_index :=
   trunc_index.rec_on m n (λ k l, l .+1)
 
-  definition leq (n m : trunc_index) : Type₀ :=
+  definition leq [reducible] (n m : trunc_index) : Type₀ :=
   trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
 
   definition has_le_trunc_index [instance] [reducible] : has_le trunc_index :=
@@ -106,10 +106,6 @@ namespace is_trunc
     (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) :=
   is_trunc.mk (is_trunc.to_internal (n.+1) A x y)
 
-  definition is_trunc_eq_zero [instance] [priority 1250] [H : is_trunc 1 A] (x y : A)
-    : is_hset (x = y) :=
-  @is_trunc_eq A 0 H x y
-
   /- contractibility -/
 
   definition is_contr.mk (center : A) (center_eq : Π(a : A), center = a) : is_contr A :=
@@ -143,9 +139,6 @@ namespace is_trunc
     A H
   --in the proof the type of H is given explicitly to make it available for class inference
 
-  theorem is_trunc_succ_zero [instance] [priority 950] (A : Type) [H : is_hset A] : is_trunc 1 A :=
-  !is_trunc_succ
-
   theorem is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m)
     [Hn : is_trunc n A] : is_trunc m A :=
   have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index 5b2473a67..e21fc957a 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -70,7 +70,6 @@ end sum
 -- Product type
 -- ------------
 
-
 namespace prod
 
   -- notation for n-ary tuples
@@ -154,10 +153,3 @@ namespace prod
   end
 
 end prod
-
-/- logic (ported from standard library as second half of logic file) -/
-
-/- iff -/
-
-variables {a b c d : Type}
-open prod sum unit
diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean
index 84da93050..baac4f210 100644
--- a/hott/types/nat/basic.hlean
+++ b/hott/types/nat/basic.hlean
@@ -103,48 +103,49 @@ general m
 
 /- addition -/
 
-protected theorem add_zero [simp] (n : ℕ) : n + 0 = n :=
+protected definition add_zero [simp] (n : ℕ) : n + 0 = n :=
 rfl
 
-theorem add_succ [simp] (n m : ℕ) : n + succ m = succ (n + m) :=
+definition add_succ [simp] (n m : ℕ) : n + succ m = succ (n + m) :=
 rfl
 
-protected theorem zero_add [simp] (n : ℕ) : 0 + n = n :=
-nat.rec_on n
-    !nat.add_zero
-    (take m IH, show 0 + succ m = succ m, from
-      calc
-        0 + succ m = succ (0 + m) : add_succ
-               ... = succ m       : IH)
+protected definition zero_add [simp] (n : ℕ) : 0 + n = n :=
+begin
+  induction n with n IH,
+    reflexivity,
+    exact ap succ IH
+end
 
-theorem succ_add [simp] (n m : ℕ) : (succ n) + m = succ (n + m) :=
-nat.rec_on m
-    (!nat.add_zero ▸ !nat.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)
+definition succ_add [simp] (n m : ℕ) : (succ n) + m = succ (n + m) :=
+begin
+  induction m with m IH,
+    reflexivity,
+    exact ap succ IH
+end
 
-protected theorem add_comm [simp] (n m : ℕ) : n + m = m + n :=
-nat.rec_on m
-    (by rewrite [nat.add_zero, nat.zero_add])
-    (take k IH, calc
-        n + succ k = succ (n+k)   : add_succ
-               ... = succ (k + n) : IH
-               ... = succ k + n   : succ_add)
+protected definition add_comm [simp] (n m : ℕ) : n + m = m + n :=
+begin
+  induction n with n IH,
+  { apply nat.zero_add},
+  { exact !succ_add ⬝ ap succ IH}
+end
 
-theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
-!succ_add ⬝ !add_succ⁻¹
+protected definition add_add (n l k : ℕ) : n + l + k = n + (k + l) :=
+begin
+  induction l with l IH,
+    reflexivity,
+    exact succ_add (n + l) k ⬝ ap succ IH
+end
 
-protected theorem add_assoc [simp] (n m k : ℕ) : (n + m) + k = n + (m + k) :=
-nat.rec_on k
-    (by rewrite +nat.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)
+definition succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
+!succ_add
+
+protected definition add_assoc [simp] (n m k : ℕ) : (n + m) + k = n + (m + k) :=
+begin
+  induction k with k IH,
+    reflexivity,
+    exact ap succ IH
+end
 
 protected theorem add_left_comm : Π (n m k : ℕ), n + (m + k) = m + (n + k) :=
 left_comm nat.add_comm nat.add_assoc