diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean
index 4100c3874..fe7390e99 100644
--- a/hott/hit/type_quotient.hlean
+++ b/hott/hit/type_quotient.hlean
@@ -10,7 +10,7 @@ Type quotients (quotient without truncation)
   The hit type_quotient is primitive, declared in init.hit.
   The constructors are
     class_of : A → A / R (A implicit, R explicit)
-    eq_of_rel : R a a' → a = a' (R explicit)
+    eq_of_rel : Π{a a' : A}, R a a' → a = a' (R explicit)
 -/
 
 open eq equiv sigma.ops
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index a2a7937ac..821c5d8e1 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -246,7 +246,6 @@ equiv.mk apd10 _
 definition eq_of_homotopy [reducible] : f ∼ g → f = g :=
 (@apd10 A P f g)⁻¹
 
---TODO: rename to eq_of_homotopy_idp
 definition eq_of_homotopy_idp (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f :=
 is_equiv.left_inv apd10 idp
 
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 2f3f25be8..a5247c36b 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -11,19 +11,37 @@ open eq decidable sum lift
 namespace nat
   notation `ℕ` := nat
 
-  inductive lt (a : nat) : nat → Type₀ :=
-  | base : lt a (succ a)
-  | step : Π {b}, lt a b → lt a (succ b)
+  /- basic definitions on natural numbers -/
+  inductive le (a : ℕ) : ℕ → Type₀ :=
+  | refl : le a a
+  | step : Π {b}, le a b → le a (succ b)
 
-  notation a < b := lt a b
+  infix `≤` := le
+  attribute le.refl [refl]
 
-  definition le [reducible] (a b : nat) : Type₀ := a < succ b
+  definition lt [reducible] (n m : ℕ) := succ n ≤ m
+  definition ge [reducible] (n m : ℕ) := m ≤ n
+  definition gt [reducible] (n m : ℕ) := succ m ≤ n
+  infix `<` := lt
+  infix `≥` := ge
+  infix `>` := gt
 
-  notation a ≤ b := le a b
-
-  definition pred (a : nat) : nat :=
+  definition pred [unfold-c 1] (a : nat) : nat :=
   nat.cases_on a zero (λ a₁, a₁)
 
+  -- add is defined in init.num
+  definition sub (a b : nat) : nat :=
+  nat.rec_on b a (λ b₁ r, pred r)
+
+  definition mul (a b : nat) : nat :=
+  nat.rec_on b zero (λ b₁ r, r + a)
+
+  notation a - b := sub a b
+  notation a * b := mul a b
+
+
+  /- properties of ℕ -/
+
   protected definition is_inhabited [instance] : inhabited nat :=
   inhabited.mk zero
 
@@ -37,200 +55,192 @@ namespace nat
       | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney)
       end
 
+  /- properties of inequality -/
+
+  definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n
+
+  definition le_succ (n : ℕ) : n ≤ succ n := by repeat constructor
+
+  definition pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor)
+
+  definition le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
+  by induction H2 with n H2 IH;exact H1;exact le.step IH
+
+  definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ
+
+  definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H
+
+  definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
+
+  definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
+  by induction H;reflexivity;exact le.step v_0
+
+  definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
+  by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
+
+  definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
+  pred_le_pred H
+
+  definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
+  by cases n;exact le.step H;exact succ_le_succ H
+
+  definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=
+  by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a
+
+  definition zero_le (n : ℕ) : 0 ≤ n :=
+  by induction n with n IH;apply le.refl;exact le.step IH
+
+  definition zero_lt_succ (n : ℕ) : 0 < succ n :=
+  by induction n with n IH;apply le.refl;exact le.step IH
+
+  definition lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
+  le.trans (le.step H1) H2
+
+  definition lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k :=
+  le.trans (succ_le_succ H1) H2
+
+  definition lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k :=
+  le.trans H1 H2
+
+  theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
+  begin
+    cases H1 with m' H1',
+    { reflexivity},
+    { cases H2 with n' H2',
+      { reflexivity},
+      { exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}},
+  end
+
+  definition not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero :=
+  by intro H; cases H
+
+  theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self
+
+  theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl
+  theorem lt.base (n : ℕ) : n < succ n := !le.refl
+
+  theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : empty :=
+  !lt.irrefl (lt_of_le_of_lt H1 H2)
+
+  theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : empty :=
+  le_lt_antisymm H2 H1
+
+  theorem lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : empty :=
+  le_lt_antisymm (le_of_lt H1) H2
+
+  theorem lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
+  begin
+    revert b H1 H2 H3, induction a with a IH,
+    { intros, cases b,
+        exact H2 idp,
+        exact H1 !zero_lt_succ},
+    { intros, cases b with b,
+        exact H3 !zero_lt_succ,
+      { apply IH,
+          intro H, exact H1 (succ_le_succ H),
+          intro H, exact H2 (ap succ H),
+          intro H, exact H3 (succ_le_succ H)}}
+  end
+
+  definition lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a :=
+  lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H))
+
+  theorem lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) :=
+  lt.by_cases inl (λH, inr (eq.rec_on H !le.refl)) (λH, inr (le_of_lt H))
+
+  definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
+  sum.rec_on (lt_or_ge a b) H1 H2
+
+  definition not_lt_zero (a : ℕ) : ¬ a < zero :=
+  by intro H; cases H
+
   -- less-than is well-founded
   definition lt.wf [instance] : well_founded lt :=
-  well_founded.intro (λn, nat.rec_on n
-    (acc.intro zero (λ (y : nat) (hlt : y < zero),
-      have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
-        λ n₁ hlt, nat.lt.cases_on hlt
-          (by contradiction)
-          (by contradiction),
-      aux hlt rfl))
-    (λ (n : nat) (ih : acc lt n),
-      acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
-        have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
-          λ n₁ hlt, nat.lt.cases_on hlt
-            (λ (sn_eq_sm : succ n = succ m),
-               by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih)
-            (λ b (hlt : m < b) (sn_eq_sb : succ n = succ b),
-               by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt),
-        aux hlt rfl)))
+  begin
+    constructor, intro n, induction n with n IH,
+    { constructor, intros n H, exfalso, exact !not_lt_zero H},
+    { constructor, intros m H,
+      assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m,
+        { intros n₁ hlt, induction hlt,
+          { intro p, injection p with q, exact q ▸ IH},
+          { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}},
+      apply aux H idp},
+  end
 
-  definition measure {A : Type} (f : A → nat) : A → A → Type₀ :=
+  definition measure {A : Type} (f : A → ℕ) : A → A → Type₀ :=
   inv_image lt f
 
-  definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
+  definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) :=
   inv_image.wf f lt.wf
 
-  definition not_lt_zero (a : nat) : ¬ a < zero :=
-  have aux : Π {b}, a < b → b = zero → empty, from
-    λ b H, lt.cases_on H
-      (by contradiction)
-      (by contradiction),
-  λ H, aux H rfl
+  theorem succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b :=
+  succ_le_succ H
 
-  definition zero_lt_succ (a : nat) : zero < succ a :=
-  nat.rec_on a
-    (lt.base zero)
-    (λ a (hlt : zero < succ a), lt.step hlt)
+  theorem lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b :=
+  le_of_succ_le H
 
-  definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
-  have aux : a < b → a < c, from
-    lt.rec_on H₂
-      (λ h₁, lt.step h₁)
-      (λ b₁ bb₁ ih h₁, lt.step (ih h₁)),
-  aux H₁
-
-  definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
-  lt.rec_on H
-    (lt.base (succ a))
-    (λ b hlt ih, lt.trans ih (lt.base (succ b)))
-
-  definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
-  lt.rec_on H
-    (lt.step (lt.base a))
-    (λ b h ih, lt.step ih)
-
-  definition lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
-  have aux : pred (succ a) < pred (succ b), from
-    lt.rec_on H
-      (lt.base a)
-      (λ (b : nat) (hlt : succ a < b) ih,
-        show pred (succ a) < pred (succ b), from
-        lt_of_succ_lt hlt),
-  aux
-
-  definition decidable_lt [instance] : decidable_rel lt :=
-  λ a b, nat.rec_on b
-    (λ (a : nat), inr (not_lt_zero a))
-    (λ (b₁ : nat) (ih : Π a, decidable (a < b₁)) (a : nat), nat.cases_on a
-       (inl !zero_lt_succ)
-       (λ a, decidable.rec_on (ih a)
-         (λ h_pos : a < b₁, inl (succ_lt_succ h_pos))
-         (λ h_neg : ¬ a < b₁,
-           have aux : ¬ succ a < succ b₁, from
-             λ h : succ a < succ b₁, h_neg (lt_of_succ_lt_succ h),
-           inr aux)))
-    a
-
-  definition le.refl (a : nat) : a ≤ a :=
-  lt.base a
-
-  definition le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
-  lt.step H
-
-  definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ⊎ a < b :=
-  begin
-    cases H with b hlt,
-      apply sum.inl rfl,
-      apply sum.inr hlt
-  end
-
-  definition le_of_eq_or_lt {a b : nat} (H : a = b ⊎ a < b) : a ≤ b :=
-  sum.rec_on H
-    (λ hl, eq.rec_on hl !le.refl)
-    (λ hr, le_of_lt hr)
+  theorem lt_of_succ_lt_succ {a b : ℕ} (H : succ a < succ b) : a < b :=
+  le_of_succ_le_succ H
 
   definition decidable_le [instance] : decidable_rel le :=
-  λ a b, decidable_iff_equiv _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le)
-
-  definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : Π b, a < b → P b) : P b :=
   begin
-    cases H with b hlt,
-      apply H₁,
-      apply H₂ b hlt
+    intros n, induction n with n IH,
+    { intro m, left, apply zero_le},
+    { intro m, cases m with m,
+      { right, apply not_succ_le_zero},
+      { let H := IH m, clear IH,
+        cases H with H H,
+          left, exact succ_le_succ H,
+          right, intro H2, exact H (le_of_succ_le_succ H2)}}
   end
 
-  definition lt.irrefl (a : nat) : ¬ a < a :=
-  nat.rec_on a
-    !not_lt_zero
-    (λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
-      ih (lt_of_succ_lt_succ h))
+  definition decidable_lt [instance] : decidable_rel lt := _
+  definition decidable_gt [instance] : decidable_rel gt := _
+  definition decidable_ge [instance] : decidable_rel ge := _
 
-  definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
-  lt.rec_on H
-    (λ h : succ a < a, !lt.irrefl (lt_of_succ_lt h))
-    (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h))
+  definition eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ⊎ a < b :=
+  by cases H with b' H; exact sum.inl rfl; exact sum.inr (succ_le_succ H)
 
-  definition lt.trichotomy (a b : nat) : a < b ⊎ a = b ⊎ b < a :=
-  nat.rec_on b
-    (λa, nat.cases_on a
-       (sum.inr (sum.inl rfl))
-       (λ a₁, sum.inr (sum.inr !zero_lt_succ)))
-    (λ b₁ (ih : Πa, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), nat.cases_on a
-       (sum.inl !zero_lt_succ)
-       (λ a, sum.rec_on (ih a)
-           (λ h : a < b₁, sum.inl (succ_lt_succ h))
-           (λ h, sum.rec_on h
-              (λ h : a = b₁, sum.inr (sum.inl (eq.rec_on h rfl)))
-              (λ h : b₁ < a, sum.inr (sum.inr (succ_lt_succ h))))))
-    a
 
-  definition eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ⊎ b < a :=
+  definition le_of_eq_or_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b :=
+  by cases H with H H; exact le_of_eq H; exact le_of_lt H
+
+  definition eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ⊎ b < a :=
   sum.rec_on (lt.trichotomy a b)
     (λ hlt, absurd hlt hnlt)
     (λ h, h)
 
-  definition lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
-  h
+  definition lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b :=
+  succ_le_succ h
 
-  definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
-  lt_of_succ_lt_succ h
+  definition lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h
 
-  definition le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
-  lt.step h
+  definition succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
 
-  definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
-  succ_lt_succ h
+  definition max (a b : ℕ) : ℕ := if a < b then b else a
+  definition min (a b : ℕ) : ℕ := if a < b then a else b
 
-  definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
-  begin
-    cases h₁ with b' hlt,
-      apply h₂,
-      apply lt.trans hlt h₂
-  end
-
-  definition lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
-  begin
-    cases h₁ with b' hlt,
-      apply h₂,
-      apply lt.trans hlt h₂
-  end
-
-  definition lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
-  begin
-    cases h₁ with b' hlt,
-      apply lt_of_succ_lt_succ h₂,
-      apply lt.trans hlt (lt_of_succ_lt_succ h₂)
-  end
-
-  definition max (a b : nat) : nat :=
-  if a < b then b else a
-
-  definition min (a b : nat) : nat :=
-  if a < b then a else b
-
-  definition max_self (a : nat) : max a a = a :=
+  definition max_self (a : ℕ) : max a a = a :=
   eq.rec_on !if_t_t rfl
 
-  definition max_eq_right {a b : nat} (H : a < b) : max a b = b :=
+  definition max_eq_right {a b : ℕ} (H : a < b) : max a b = b :=
   if_pos H
 
-  definition max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
+  definition max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a :=
   if_neg H
 
-  definition eq_max_right {a b : nat} (H : a < b) : b = max a b :=
+  definition eq_max_right {a b : ℕ} (H : a < b) : b = max a b :=
   eq.rec_on (max_eq_right H) rfl
 
-  definition eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
+  definition eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b :=
   eq.rec_on (max_eq_left H) rfl
 
-  definition le_max_left (a b : nat) : a ≤ max a b :=
+  definition le_max_left (a b : ℕ) : a ≤ max a b :=
   by_cases
     (λ h : a < b,   le_of_lt (eq.rec_on (eq_max_right h) h))
     (λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
 
-  definition le_max_right (a b : nat) : b ≤ max a b :=
+  definition le_max_right (a b : ℕ) : b ≤ max a b :=
   by_cases
     (λ h : a < b,   eq.rec_on (eq_max_right h) !le.refl)
     (λ h : ¬ a < b, sum.rec_on (eq_or_lt_of_not_lt h)
@@ -239,71 +249,36 @@ namespace nat
         have aux : a = max a b, from eq_max_left (lt.asymm h),
         eq.rec_on aux (le_of_lt h)))
 
-  definition gt [reducible] a b := lt b a
-  definition decidable_gt [instance] : decidable_rel gt :=
-  _
+  definition succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b :=
+  by induction b with b IH; reflexivity; apply ap pred IH
 
-  notation a > b := gt a b
-
-  definition ge [reducible] a b := le b a
-  definition decidable_ge [instance] : decidable_rel ge :=
-  _
-
-  notation a ≥ b := ge a b
-
-  -- add is defined in init.num
-
-  definition sub (a b : nat) : nat :=
-  nat.rec_on b a (λ b₁ r, pred r)
-
-  notation a - b := sub a b
-
-  definition mul (a b : nat) : nat :=
-  nat.rec_on b zero (λ b₁ r, r + a)
-
-  notation a * b := mul a b
-
-  section
-  local attribute sub [reducible]
-  definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
-  nat.rec_on b
-    rfl
-    (λ b₁ (ih : succ a - succ b₁ = a - b₁),
-      eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
-  end
-
-  definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
+  definition sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b :=
   eq.rec_on (succ_sub_succ_eq_sub a b) rfl
 
-  definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
+  definition zero_sub_eq_zero (a : ℕ) : zero - a = zero :=
   nat.rec_on a
     rfl
     (λ a₁ (ih : zero - a₁ = zero), ap pred ih)
 
-  definition zero_eq_zero_sub (a : nat) : zero = zero - a :=
+  definition zero_eq_zero_sub (a : ℕ) : zero = zero - a :=
   eq.rec_on (zero_sub_eq_zero a) rfl
 
-  definition sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
+  definition sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a :=
   have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
-    λa h₁, lt.rec_on h₁
-      (λb h₂, lt.cases_on h₂
+    λa h₁, le.rec_on h₁
+      (λb h₂, le.cases_on h₂
         (lt.base zero)
         (λ b₁ bpos,
           eq.rec_on (sub_eq_succ_sub_succ zero b₁)
            (eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
-      (λa₁ apos ih b h₂, lt.cases_on h₂
+      (λa₁ apos ih b h₂, le.cases_on h₂
         (lt.base a₁)
         (λ b₁ bpos,
           eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
             (lt.trans (@ih b₁ bpos) (lt.base a₁)))),
   λ h₁ h₂, aux h₁ h₂
 
-  definition pred_le (a : nat) : pred a ≤ a :=
-  nat.cases_on a
-    (le.refl zero)
-    (λ a₁, le_of_lt (lt.base a₁))
-
-  definition sub_le (a b : nat) : a - b ≤ a :=
+  definition sub_le (a b : ℕ) : a - b ≤ a :=
   nat.rec_on b
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 56794fcac..8d55e0896 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -141,38 +141,48 @@ namespace eq
     q ⬝ p = r → q = r ⬝ p⁻¹ :=
   eq.rec_on p (take r h, !con_idp⁻¹ ⬝ h ⬝ !con_idp⁻¹) r
 
-  definition eq_of_con_inv_eq_idp {p q : x = y} :
-    p ⬝ q⁻¹ = idp → p = q :=
+  definition eq_of_con_inv_eq_idp {p q : x = y} : p ⬝ q⁻¹ = idp → p = q :=
   eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p
 
-  definition eq_of_inv_con_eq_idp {p q : x = y} :
-    q⁻¹ ⬝ p = idp → p = q :=
+  definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q :=
   eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p
 
-  definition eq_inv_of_con_eq_idp' {p : x = y} {q : y = x} :
-    p ⬝ q = idp → p = q⁻¹ :=
+  definition eq_inv_of_con_eq_idp' {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ :=
   eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p
 
-  definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} :
-    q ⬝ p = idp → p = q⁻¹ :=
+  definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ :=
   eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p
 
-  definition eq_of_idp_eq_inv_con {p q : x = y} :
-    idp = p⁻¹ ⬝ q → p = q :=
+  definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q :=
   eq.rec_on p (take q h, h ⬝ !idp_con) q
 
-  definition eq_of_idp_eq_con_inv {p q : x = y} :
-    idp = q ⬝ p⁻¹ → p = q :=
+  definition eq_of_idp_eq_con_inv {p q : x = y} : idp = q ⬝ p⁻¹ → p = q :=
   eq.rec_on p (take q h, h ⬝ !con_idp) q
 
-  definition inv_eq_of_idp_eq_con {p : x = y} {q : y = x} :
-    idp = q ⬝ p → p⁻¹ = q :=
+  definition inv_eq_of_idp_eq_con {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q :=
   eq.rec_on p (take q h, h ⬝ !con_idp) q
 
-  definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} :
-    idp = p ⬝ q → p⁻¹ = q :=
+  definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q :=
   eq.rec_on p (take q h, h ⬝ !idp_con) q
 
+  definition con_inv_eq_idp {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp :=
+  by cases r;apply con.right_inv
+
+  definition inv_con_eq_idp {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp :=
+  by cases r;apply con.left_inv
+
+  definition con_eq_idp {p : x = y} {q : y = x} (r : p = q⁻¹) : p ⬝ q = idp :=
+  by cases q;exact r
+
+  definition idp_eq_inv_con {p q : x = y} (r : p = q) : idp = p⁻¹ ⬝ q :=
+  by cases r;exact !con.left_inv⁻¹
+
+  definition idp_eq_con_inv {p q : x = y} (r : p = q) : idp = q ⬝ p⁻¹ :=
+  by cases r;exact !con.right_inv⁻¹
+
+  definition idp_eq_con {p : x = y} {q : y = x} (r : p⁻¹ = q) : idp = q ⬝ p :=
+  by cases p;exact r
+
   /- Transport -/
 
   definition transport [subst] [reducible] [unfold-c 5] (P : A → Type) {x y : A} (p : x = y)
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 91f93def3..c943933a7 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -87,7 +87,7 @@ namespace is_trunc
 
   definition is_trunc_eq [instance] [priority 1200]
     (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 H x y)
+  is_trunc.mk (is_trunc.to_internal (n.+1) A x y)
 
   /- contractibility -/
 
@@ -95,10 +95,10 @@ namespace is_trunc
   is_trunc.mk (contr_internal.mk center center_eq)
 
   definition center (A : Type) [H : is_contr A] : A :=
-  @contr_internal.center A (@is_trunc.to_internal -2 A H)
+  contr_internal.center (is_trunc.to_internal -2 A)
 
   definition center_eq [H : is_contr A] (a : A) : !center = a :=
-  @contr_internal.center_eq A !is_trunc.to_internal a
+  contr_internal.center_eq !is_trunc.to_internal a
 
   definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y :=
   (center_eq x)⁻¹ ⬝ (center_eq y)
@@ -107,14 +107,14 @@ namespace is_trunc
   have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv),
   (K p)⁻¹ ⬝ K q
 
-  definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
+  theorem is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
   is_contr.mk !eq_of_is_contr (λ p, !hprop_eq_of_is_contr)
   local attribute is_contr_eq [instance]
 
   /- truncation is upward close -/
 
   -- n-types are also (n+1)-types
-  definition is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index)
+  theorem is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index)
     [H : is_trunc n A] : is_trunc (n.+1) A :=
   trunc_index.rec_on n
     (λ A (H : is_contr A), !is_trunc_succ_intro)
@@ -122,7 +122,7 @@ namespace is_trunc
     A H
   --in the proof the type of H is given explicitly to make it available for class inference
 
-  definition is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m)
+  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
     λ k A, trunc_index.cases_on k
@@ -139,16 +139,16 @@ namespace is_trunc
   trunc_index.rec_on m base step n A Hnm Hn
 
   -- the following cannot be instances in their current form, because they are looping
-  definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
+  theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
   trunc_index.rec_on n H _
 
-  definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
+  theorem is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
       : is_trunc (n.+1) A :=
-  @is_trunc_of_leq A (-2.+1) _ star _
+  is_trunc_of_leq A (star : -1 ≤ n.+1)
 
-   definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
+  theorem is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
       : is_trunc (n.+2) A :=
-  @is_trunc_of_leq A (-2.+1.+1) _ star _
+  is_trunc_of_leq A (star : 0 ≤ n.+2)
 
   /- hprops -/
 
@@ -158,19 +158,21 @@ namespace is_trunc
   definition is_contr_of_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A :=
   is_contr.mk x (λy, !is_hprop.elim)
 
-  --Coq has the following as instance, but doesn't look too useful
-  definition is_hprop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
+  theorem is_hprop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
   @is_trunc_succ_intro A -2
     (λx y,
       have H2 [visible] : is_contr A, from H x,
       !is_contr_eq)
 
-  definition is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A :=
+  theorem is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A :=
   is_hprop_of_imp_is_contr (λ x, is_contr.mk x (H x))
 
+  theorem is_hprop_elim_self {A : Type} {H : is_hprop A} (x : A) : is_hprop.elim x x = idp :=
+  !is_hprop.elim
+
   /- hsets -/
 
-  definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A :=
+  theorem is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A :=
   @is_trunc_succ_intro _ _ (λ x y, is_hprop.mk (H x y))
 
   definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q :=
@@ -218,15 +220,15 @@ namespace is_trunc
     : (is_contr B) :=
   is_contr.mk (f (center A)) (λp, eq_of_eq_inv !center_eq)
 
-  theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
-  @is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _
+  definition is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
+  is_contr_is_equiv_closed (to_fun H)
 
   definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
   equiv.mk
     (λa, center B)
     (is_equiv.adjointify (λa, center B) (λb, center A) center_eq center_eq)
 
-  definition is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f]
+  theorem is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f]
     [HA : is_trunc n A] : is_trunc n B :=
   trunc_index.rec_on n
     (λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f)
@@ -246,15 +248,15 @@ namespace is_trunc
     : is_trunc n A :=
   is_trunc_is_equiv_closed n (to_inv f)
 
-  definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
-    : is_equiv f :=
+  definition is_equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B]
+    (f : A → B) (g : B → A) : is_equiv f :=
   is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim)
 
-  definition equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
-    : A ≃ B :=
+  definition equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B]
+    (f : A → B) (g : B → A) : A ≃ B :=
   equiv.mk f (is_equiv_of_is_hprop f g)
 
-  definition equiv_of_iff_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
+  definition equiv_of_iff_of_is_hprop [unfold-c 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
   equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H)
 
   end
diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean
index 7d7982dd4..cedfaf40a 100644
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@@ -8,25 +8,44 @@ Theorems about the natural numbers specific to HoTT
 
 import .basic
 
-open is_trunc unit empty eq
+open is_trunc unit empty eq equiv
 
 namespace nat
 
-  definition is_hprop_lt [instance] (n m : ℕ) : is_hprop (n < m) :=
+  definition is_hprop_le [instance] (n m : ℕ) : is_hprop (n ≤ m) :=
   begin
-    assert H : Π{n m : ℕ} (p : n < m) (q : succ n = m), p = q ▸ lt.base n,
+    assert lem : Π{n m : ℕ} (p : n ≤ m) (q : n = m), p = q ▸ le.refl n,
     { intros, cases p,
       { assert H' : q = idp, apply is_hset.elim,
         cases H', reflexivity},
-      { cases q, exfalso, exact lt.irrefl b a}},
-    apply is_hprop.mk, intros p q,
-    induction q,
-    { apply H},
-    { cases p,
-        exfalso, exact lt.irrefl b a,
-        exact ap lt.step !v_0}
+      { cases q, exfalso, apply not_succ_le_self a}},
+    apply is_hprop.mk, intro H1 H2, induction H2,
+    { apply lem},
+    { cases H1,
+      { exfalso, apply not_succ_le_self a},
+      { exact ap le.step !v_0}},
   end
+  definition le_equiv_succ_le_succ (n m : ℕ) : (n ≤ m) ≃ (succ n ≤ succ m) :=
+  equiv_of_is_hprop succ_le_succ le_of_succ_le_succ
+  definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) :=
+  equiv_of_is_hprop pred_le_pred le_succ_of_pred_le
 
-  definition is_hprop_le (n m : ℕ) : is_hprop (n ≤ m) := !is_hprop_lt
+
+  -- definition is_hprop_lt [instance] (n m : ℕ) : is_hprop (n < m) :=
+  -- begin
+  --   assert H : Π{n m : ℕ} (p : n < m) (q : succ n = m), p = q ▸ lt.base n,
+  --   { intros, cases p,
+  --     { assert H' : q = idp, apply is_hset.elim,
+  --       cases H', reflexivity},
+  --     { cases q, exfalso, exact lt.irrefl b a}},
+  --   apply is_hprop.mk, intros p q,
+  --   induction q,
+  --   { apply H},
+  --   { cases p,
+  --       exfalso, exact lt.irrefl b a,
+  --       exact ap lt.step !v_0}
+  -- end
+
+  -- definition is_hprop_le (n m : ℕ) : is_hprop (n ≤ m) := !is_hprop_lt
 
 end nat
diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean
index 8e6c1e2a2..d7337d69c 100644
--- a/hott/types/nat/order.hlean
+++ b/hott/types/nat/order.hlean
@@ -5,11 +5,11 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
 
 The order relation on the natural numbers.
 
-Ported from standard library
+Note: this file has significant differences than the standard library version
 -/
 
 import .basic algebra.ordered_ring
-open prod decidable sum eq
+open prod decidable sum eq sigma sigma.ops
 
 namespace nat
 
@@ -18,12 +18,6 @@ namespace nat
 theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ⊎ m = n) : m ≤ n :=
 sum.rec_on H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
 
-theorem lt.by_cases {a b : ℕ} {P : Type}
-  (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
-sum.rec_on !lt.trichotomy
-  (assume H, H1 H)
-  (assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
-
 theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ⊎ m = n :=
 lt.by_cases
   (assume H1 : m < n, sum.inl H1)
@@ -58,15 +52,7 @@ theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
 h ▸ le_add_right n k
 
 theorem le.elim {n m : ℕ} (h : n ≤ m) : Σk, n + k = m :=
-le.rec_on h
-  (sigma.mk 0 rfl)
-  (λ m (h : n < m), lt.rec_on h
-    (sigma.mk 1 rfl)
-    (λ b hlt (ih : Σ (k : ℕ), n + k = b),
-      sigma.rec_on ih (λ(k : ℕ) (h : n + k = b),
-      sigma.mk (succ k) (calc
-        n + succ k = succ (n + k) : add_succ
-               ... = succ b       : h))))
+by induction h with m h ih;exact ⟨0, idp⟩;exact ⟨succ ih.1, ap succ ih.2⟩
 
 theorem le.total {m n : ℕ} : m ≤ n ⊎ n ≤ m :=
 lt.by_cases
@@ -123,25 +109,6 @@ lt_of_lt_of_le H2 H3
 theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
 !mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
 
-theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
-sigma.rec_on (le.elim H1) (λ(k : ℕ) (Hk : n + k = m),
-sigma.rec_on (le.elim H2) (λ(l : ℕ) (Hl : m + l = n),
-have L1 : k + l = 0, from
-  add.cancel_left
-    (calc
-      n + (k + l) = n + k + l : (!add.assoc)⁻¹
-        ... = m + l           : {Hk}
-        ... = n               : Hl
-        ... = n + 0           : (!add_zero)⁻¹),
-have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
-calc
-  n = n + 0  : (!add_zero)⁻¹
-... = n  + k : {L2⁻¹}
-... = m      : Hk))
-
-theorem zero_le (n : ℕ) : 0 ≤ n :=
-le.intro !zero_add
-
 /- nat is an instance of a linearly ordered semiring -/
 
 section
@@ -224,17 +191,6 @@ eq_zero_of_add_eq_zero_right Hk
 theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
 iff.intro succ_le_of_lt lt_of_succ_le
 
-theorem not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 :=
-(assume H : succ n ≤ 0,
-  have H2 : succ n = 0, from eq_zero_of_le_zero H,
-  absurd H2 !succ_ne_zero)
-
-theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
-!add_one ▸ !add_one ▸ add_le_add_right H 1
-
-theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
-le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
-
 theorem self_le_succ (n : ℕ) : n ≤ succ n :=
 le.intro !add_one
 
@@ -243,14 +199,6 @@ sum.rec_on (lt_or_eq_of_le H)
   (assume H1 : n < m, sum.inl (succ_le_of_lt H1))
   (assume H1 : n = m, sum.inr H1)
 
-theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
-nat.cases_on n
-  (assume H : pred 0 ≤ m, !zero_le)
-  (take n',
-    assume H : pred (succ n') ≤ m,
-    have H1 : n' ≤ m, from pred_succ n' ▸ H,
-    succ_le_succ H1)
-
 theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
 nat.cases_on n
   (assume H, !pred_zero⁻¹ ▸ zero_le m)
diff --git a/hott/types/square.hlean b/hott/types/square.hlean
index d82508502..a0a9bc547 100644
--- a/hott/types/square.hlean
+++ b/hott/types/square.hlean
@@ -91,6 +91,10 @@ namespace eq
     { intro s, cases s, apply idp},
   end
 
+  definition naturality [unfold-c 8] {f g : A → B} (p : f ∼ g) (q : a = a') :
+    square (p a) (p a') (ap f q) (ap g q) :=
+  eq.rec_on q vrfl
+
   definition rec_on_b [recursor] {a₀₀ : A}
     {P : Π{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}, square t idp l r → Type}
     {a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}
@@ -141,10 +145,21 @@ namespace eq
     from eq.rec_on (eq_of_square s : idp ⬝ r = l) (by cases r; exact H),
   left_inv (to_fun !square_equiv_eq) s ▸ H2
 
-  definition naturality [unfold-c 8] {f g : A → B} (p : f ∼ g) (q : a = a') :
-    square (p a) (p a') (ap f q) (ap g q) :=
-  eq.rec_on q vrfl
+  definition rec_on_lr [recursor] {a : A}
+    {P : Π{a' : A} {t : a = a'} {b : a = a'}, square t b idp idp → Type}
+    {a' : A} {t : a = a'} {b : a = a'}
+      (s : square t b idp idp) (H : P ids) : P s :=
+  let p : idp ⬝ b = t := (eq_of_square s)⁻¹ in
+  assert H2 : P (square_of_eq (eq_of_square s)⁻¹⁻¹),
+    from @eq.rec_on _ _ (λx q, P (square_of_eq q⁻¹)) _ p (by cases b; exact H),
+  to_left_inv (!square_equiv_eq) s ▸ !inv_inv ▸ H2
 
-  --we can also do the other recursors (lr, tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
+definition eq_of_hdeg_square {p q : a = a'} (s : square idp idp p q) : p = q :=
+  rec_on_tb s idp
+
+definition eq_of_vdeg_square {p q : a = a'} (s : square p q idp idp) : p = q :=
+  rec_on_lr s idp
+
+  --we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
 
 end eq