diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 2fd0ca8ed1..bd7e7dcbe2 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -56,7 +56,7 @@ namespace functor
   functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq'))
 
   definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
-    {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ∼ F₂)
+    {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ~ F₂)
     (pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f)
       : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
   begin
@@ -66,7 +66,7 @@ namespace functor
       rewrite [+pi_transport_constant,-pH,-transport_hom]}
   end
 
-  definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
+  definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ~ to_fun_ob F₂),
     (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
   functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq))
 
@@ -165,7 +165,7 @@ namespace functor
     (r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ :=
   by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim
 
-  definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ∼ ap010 to_fun_ob q)
+  definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ~ ap010 to_fun_ob q)
     : p = q :=
   begin
     cases F₁ with ob₁ hom₁ id₁ comp₁,
@@ -183,8 +183,8 @@ namespace functor
       : ap010 to_fun_ob (apd01111 functor.mk pF pH pid pcomp) c = ap10 pF c :=
   by cases pF; cases pH; cases pid; cases pcomp; apply idp
 
-  definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
-    (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ∼3 to_fun_hom F₂) (c : C) :
+  definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ~ to_fun_ob F₂)
+    (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ~3 to_fun_hom F₂) (c : C) :
     ap010 to_fun_ob (functor_eq p q) c = p c :=
   begin
     cases F₁ with F₁o F₁h F₁id F₁comp, cases F₂ with F₂o F₂h F₂id F₂comp,
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index c833ac96a5..8bc5b0dcd4 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -205,7 +205,7 @@ namespace iso
       : p ▸ f = hom_of_eq (apd10 p y) ∘ f ∘ inv_of_eq (apd10 p x) :=
     eq.rec_on p !id_leftright⁻¹
 
-    definition transport_hom (p : F ∼ G) (f : hom (F x) (F y))
+    definition transport_hom (p : F ~ G) (f : hom (F x) (F y))
       : eq_of_homotopy p ▸ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) :=
     calc
       eq_of_homotopy p ▸ f =
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index 7098113c70..5ee35dac49 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -40,11 +40,11 @@ namespace nat_trans
   definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)}
     (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f)
     (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f)
-    (p : η₁ ∼ η₂)
+    (p : η₁ ~ η₂)
       : nat_trans.mk η₁ nat₁ = nat_trans.mk η₂ nat₂ :=
   apd011 nat_trans.mk (eq_of_homotopy p) !is_hprop.elim
 
-  definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ∼ natural_map η₂ → η₁ = η₂ :=
+  definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ~ natural_map η₂ → η₁ = η₂ :=
   nat_trans.rec_on η₁ (λf₁ nat₁, nat_trans.rec_on η₂ (λf₂ nat₂ p, !nat_trans_mk_eq p))
 
   protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
diff --git a/hott/arity.hlean b/hott/arity.hlean
index c852b0b00e..e982bcfa83 100644
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@@ -48,8 +48,8 @@ namespace eq
   definition homotopy4 [reducible] (f g : Πa b c d, E a b c d) : Type :=
   Πa b c d, f a b c d = g a b c d
 
-  notation f `∼2`:50 g := homotopy2 f g
-  notation f `∼3`:50 g := homotopy3 f g
+  notation f `~2`:50 g := homotopy2 f g
+  notation f `~3`:50 g := homotopy3 f g
 
   definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' :=
   by cases Hu; congruence; repeat assumption
@@ -72,13 +72,13 @@ namespace eq
       : f u v w x y z = f u' v' w' x' y' z' :=
   by cases Hu; congruence; repeat assumption
 
-  definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ∼ f x' :=
+  definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ~ f x' :=
   by intros; cases Hx; reflexivity
 
-  definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ∼2 f x' :=
+  definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ~2 f x' :=
   by intros; cases Hx; reflexivity
 
-  definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' :=
+  definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ~3 f x' :=
   by intros; cases Hx; reflexivity
 
   definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : transport B Ha b = b')
@@ -121,10 +121,10 @@ namespace eq
   --   : f a b c d e ff g h = f a' b' c' d' e' f' g' h' :=
   -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity
 
-  definition apd100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
+  definition apd100 {f g : Πa b, C a b} (p : f = g) : f ~2 g :=
   λa b, apd10 (apd10 p a) b
 
-  definition apd1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g :=
+  definition apd1000 {f g : Πa b c, D a b c} (p : f = g) : f ~3 g :=
   λa b c, apd100 (apd10 p a) b c
 
   /- some properties of these variants of ap -/
@@ -141,10 +141,10 @@ namespace eq
 
   /- the following theorems are function extentionality for functions with multiple arguments -/
 
-  definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
+  definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ~2 g) : f = g :=
   eq_of_homotopy (λa, eq_of_homotopy (H a))
 
-  definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ∼3 g) : f = g :=
+  definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ~3 g) : f = g :=
   eq_of_homotopy (λa, eq_of_homotopy2 (H a))
 
   definition eq_of_homotopy2_id (f : Πa b, C a b)
@@ -200,12 +200,12 @@ end funext
 namespace eq
   open funext
   local attribute funext.is_equiv_apd100 [instance]
-  protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type}
-    (p : f ∼2 g) (H : Π(q : f = g), P (apd100 q)) : P p :=
+  protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ~2 g) → Type}
+    (p : f ~2 g) (H : Π(q : f = g), P (apd100 q)) : P p :=
   right_inv apd100 p ▸ H (eq_of_homotopy2 p)
 
-  protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type}
-    (p : f ∼3 g) (H : Π(q : f = g), P (apd1000 q)) : P p :=
+  protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ~3 g) → Type}
+    (p : f ~3 g) (H : Π(q : f = g), P (apd1000 q)) : P p :=
   right_inv apd1000 p ▸ H (eq_of_homotopy3 p)
 
   definition apd10_ap (f : X → Πa, B a) (p : x = x')
@@ -216,7 +216,7 @@ namespace eq
     : eq_of_homotopy (ap010 f p) = ap f p :=
   inv_eq_of_eq !apd10_ap⁻¹
 
-  definition ap_eq_ap_of_homotopy {f : X → Πa, B a} {p q : x = x'} (H : ap010 f p ∼ ap010 f q)
+  definition ap_eq_ap_of_homotopy {f : X → Πa, B a} {p q : x = x'} (H : ap010 f p ~ ap010 f q)
     : ap f p = ap f q :=
   calc
     ap f p = eq_of_homotopy (ap010 f p) : eq_of_homotopy_ap010
diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean
index 9ff84d609e..c38898a34e 100644
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@@ -10,7 +10,7 @@ import .sphere
 import types.bool types.int.hott types.equiv
 import algebra.fundamental_group algebra.hott
 
-open eq suspension bool sphere_index is_equiv equiv equiv.ops is_trunc pi
+open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi
 
 definition circle : Type₀ := sphere 1
 
diff --git a/hott/hit/interval.hlean b/hott/hit/interval.hlean
index 9fee3b4a7a..67447ad6d9 100644
--- a/hott/hit/interval.hlean
+++ b/hott/hit/interval.hlean
@@ -6,21 +6,21 @@ Authors: Floris van Doorn
 Declaration of the interval
 -/
 
-import .suspension types.eq types.prod types.cubical.square
-open eq suspension unit equiv equiv.ops is_trunc nat prod
+import .susp types.eq types.prod types.cubical.square
+open eq susp unit equiv equiv.ops is_trunc nat prod
 
-definition interval : Type₀ := suspension unit
+definition interval : Type₀ := susp unit
 
 namespace interval
 
-  definition zero : interval := !north
-  definition one  : interval := !south
+  definition zero : interval := north
+  definition one  : interval := south
   definition seg  : zero = one := merid star
 
   protected definition rec {P : interval → Type} (P0 : P zero) (P1 : P one)
     (Ps : P0 =[seg] P1) (x : interval) : P x :=
   begin
-    fapply suspension.rec_on x,
+    fapply susp.rec_on x,
     { exact P0},
     { exact P1},
     { intro x, cases x, exact Ps}
diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean
index 2abb6e2478..63482382ce 100644
--- a/hott/hit/sphere.hlean
+++ b/hott/hit/sphere.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn
 Declaration of the n-spheres
 -/
 
-import .suspension types.trunc
+import .susp types.trunc
 
-open eq nat suspension bool is_trunc unit pointed
+open eq nat susp bool is_trunc unit pointed
 
 /-
   We can define spheres with the following possible indices:
@@ -78,11 +78,11 @@ open sphere_index equiv
 
 definition sphere : sphere_index → Type₀
 | -1   := empty
-| n.+1 := suspension (sphere n)
+| n.+1 := susp (sphere n)
 
 namespace sphere
 
-  definition base {n : ℕ} : sphere n := !north
+  definition base {n : ℕ} : sphere n := north
   definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) :=
   pointed.mk base
   definition Sphere [constructor] (n : ℕ) : Pointed := pointed.mk' (sphere n)
@@ -94,24 +94,24 @@ namespace sphere
   open sphere.ops
 
   definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) :=
-  pointed_map.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv
+  pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv
 
   definition surf {n : ℕ} : Ω[n] S. n :=
   nat.rec_on n (by esimp [Iterated_loop_space]; exact base)
-               (by intro n s;exact apn (equator n) s)
+               (by intro n s;exact apn n (equator n) s)
 
   definition bool_of_sphere [reducible] : S 0 → bool :=
-  suspension.rec ff tt (λx, empty.elim x)
+  susp.rec ff tt (λx, empty.elim x)
 
   definition sphere_of_bool [reducible] : bool → S 0
-  | ff := !north
-  | tt := !south
+  | ff := north
+  | tt := south
 
   definition sphere_equiv_bool : S 0 ≃ bool :=
   equiv.MK bool_of_sphere
            sphere_of_bool
            (λb, match b with | tt := idp | ff := idp end)
-           (λx, suspension.rec_on x idp idp (empty.rec _))
+           (λx, susp.rec_on x idp idp (empty.rec _))
 
   definition sphere_eq_bool : S 0 = bool :=
   ua sphere_equiv_bool
@@ -119,20 +119,20 @@ namespace sphere
   definition sphere_eq_bool_pointed : S. 0 = Bool :=
   Pointed_eq sphere_equiv_bool idp
 
-  definition pointed_map_sphere (A : Pointed) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
+  definition pmap_sphere (A : Pointed) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
   begin
     revert A, induction n with n IH,
-    { intro A, rewrite [sphere_eq_bool_pointed], apply pointed_map_bool_equiv},
-    { intro A, transitivity _, apply suspension_adjoint_loop (S. n) A, apply IH}
+    { intro A, rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv},
+    { intro A, transitivity _, apply susp_adjoint_loop (S. n) A, apply IH}
   end
 
   protected definition elim {n : ℕ} {P : Pointed} (p : Ω[n] P) : map₊ (S. n) P :=
-  to_inv !pointed_map_sphere p
+  to_inv !pmap_sphere p
 
-  definition elim_surf {n : ℕ} {P : Pointed} (p : Ω[n] P) : apn (sphere.elim p) surf = p :=
+  definition elim_surf {n : ℕ} {P : Pointed} (p : Ω[n] P) : apn n (sphere.elim p) surf = p :=
   begin
     induction n with n IH,
-    { esimp [apn,surf,sphere.elim,pointed_map_sphere], apply sorry},
+    { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry},
     { apply sorry}
   end
 
@@ -141,20 +141,21 @@ end sphere
 open sphere sphere.ops
 
 structure weakly_constant [class] {A B : Type} (f : A → B) := --move
-  (is_constant : Πa a', f a = f a')
+  (is_weakly_constant : Πa a', f a = f a')
+abbreviation wconst := @weakly_constant.is_weakly_constant
 
-namespace trunc
+namespace is_trunc
   open trunc_index
   variables {n : ℕ} {A : Type}
-  definition is_trunc_of_pointed_map_sphere_constant
+  definition is_trunc_of_pmap_sphere_constant
     (H : Π(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
   begin
     apply iff.elim_right !is_trunc_iff_is_contr_loop,
     intro a,
-    apply is_trunc_equiv_closed, apply pointed_map_sphere,
+    apply is_trunc_equiv_closed, apply pmap_sphere,
     fapply is_contr.mk,
-    { exact pointed_map.mk (λx, a) idp},
-    { intro f, fapply pointed_map_eq,
+    { exact pmap.mk (λx, a) idp},
+    { intro f, fapply pmap_eq,
       { intro x, esimp, refine !respect_pt⁻¹ ⬝ (!H ⬝ !H⁻¹)},
       { rewrite [▸*,con.right_inv,▸*,con.left_inv]}}
   end
@@ -162,22 +163,30 @@ namespace trunc
   definition is_trunc_iff_map_sphere_constant
     (H : Π(f : S n → A) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
   begin
-    apply is_trunc_of_pointed_map_sphere_constant,
+    apply is_trunc_of_pmap_sphere_constant,
     intros, cases f with f p, esimp at *, apply H
   end
 
-  definition pointed_map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+  definition pmap_sphere_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A]
     (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base :=
   begin
     let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a,
-    let H'' := @is_trunc_equiv_closed_rev _ _ _ !pointed_map_sphere H',
-    assert p : (f = pointed_map.mk (λx, f base) (respect_pt f)),
+    let H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H',
+    assert p : (f = pmap.mk (λx, f base) (respect_pt f)),
       apply is_hprop.elim,
-    exact ap10 (ap pointed_map.map p) x
+    exact ap10 (ap pmap.map p) x
   end
 
-  definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
-    (f : S n → A) (x : S n) : f x = f base :=
-  pointed_map_sphere_constant_of_is_trunc (f base) (pointed_map.mk f idp) x
+  definition pmap_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+    (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x y : S n) : f x = f y :=
+  let H := pmap_sphere_constant_of_is_trunc' a f in !H ⬝ !H⁻¹
 
-end trunc
+  definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+    (f : S n → A) (x y : S n) : f x = f y :=
+  pmap_sphere_constant_of_is_trunc (f base) (pmap.mk f idp) x y
+
+  definition map_sphere_constant_of_is_trunc_self [H : is_trunc (n.-2.+1) A]
+    (f : S n → A) (x : S n) : map_sphere_constant_of_is_trunc f x x = idp :=
+  !con.right_inv
+
+end is_trunc
diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean
new file mode 100644
index 0000000000..29dbb6e6f6
--- /dev/null
+++ b/hott/hit/susp.hlean
@@ -0,0 +1,309 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Declaration of suspension
+-/
+
+import .pushout types.pointed types.cubical.square
+
+open pushout unit eq equiv equiv.ops
+
+definition susp (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
+
+namespace susp
+  variable {A : Type}
+
+  definition north {A : Type} : susp A :=
+  inl _ _ star
+
+  definition south {A : Type} : susp A :=
+  inr _ _ star
+
+  definition merid (a : A) : @north A = @south A :=
+  glue _ _ a
+
+  protected definition rec {P : susp A → Type} (PN : P north) (PS : P south)
+    (Pm : Π(a : A), PN =[merid a] PS) (x : susp A) : P x :=
+  begin
+    fapply pushout.rec_on _ _ x,
+    { intro u, cases u, exact PN},
+    { intro u, cases u, exact PS},
+    { exact Pm},
+  end
+
+  protected definition rec_on [reducible] {P : susp A → Type} (y : susp A)
+    (PN : P north) (PS : P south) (Pm : Π(a : A), PN =[merid a] PS) : P y :=
+  susp.rec PN PS Pm y
+
+  theorem rec_merid {P : susp A → Type} (PN : P north) (PS : P south)
+    (Pm : Π(a : A), PN =[merid a] PS) (a : A)
+      : apdo (susp.rec PN PS Pm) (merid a) = Pm a :=
+  !rec_glue
+
+  protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
+    (x : susp A) : P :=
+  susp.rec PN PS (λa, pathover_of_eq (Pm a)) x
+
+  protected definition elim_on [reducible] {P : Type} (x : susp A)
+    (PN : P) (PS : P)  (Pm : A → PN = PS) : P :=
+  susp.elim PN PS Pm x
+
+  theorem elim_merid {P : Type} {PN PS : P} (Pm : A → PN = PS) (a : A)
+    : ap (susp.elim PN PS Pm) (merid a) = Pm a :=
+  begin
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)),
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑susp.elim,rec_merid],
+  end
+
+  protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
+    (x : susp A) : Type :=
+  susp.elim PN PS (λa, ua (Pm a)) x
+
+  protected definition elim_type_on [reducible] (x : susp A)
+    (PN : Type) (PS : Type)  (Pm : A → PN ≃ PS) : Type :=
+  susp.elim_type PN PS Pm x
+
+  theorem elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
+    (a : A) : transport (susp.elim_type PN PS Pm) (merid a) = Pm a :=
+  by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,elim_merid];apply cast_ua_fn
+
+end susp
+
+attribute susp.north susp.south [constructor]
+attribute susp.rec susp.elim [unfold-c 6] [recursor 6]
+attribute susp.elim_type [unfold-c 5]
+attribute susp.rec_on susp.elim_on [unfold-c 3]
+attribute susp.elim_type_on [unfold-c 2]
+
+namespace susp
+  open pointed
+
+  definition pointed_susp [instance] [constructor] (A : Type) : pointed (susp A) :=
+  pointed.mk north
+
+  definition Susp [constructor] (A : Type) : Pointed :=
+  pointed.mk' (susp A)
+
+  definition Susp_functor {X Y : Pointed} (f : X →* Y) : Susp X →* Susp Y :=
+  begin
+    fapply pmap.mk,
+    { intro x, induction x,
+        apply north,
+        apply south,
+        exact merid (f a)},
+    { reflexivity}
+  end
+
+  definition Susp_functor_compose {X Y Z : Pointed} (g : Y →* Z) (f : X →* Y)
+    : Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction a,
+      { reflexivity},
+      { reflexivity},
+      { apply pathover_eq, apply hdeg_square,
+        rewrite [▸*,ap_compose' (Susp_functor f),↑Susp_functor,+elim_merid]}},
+    { reflexivity}
+  end
+
+  -- adjunction from Coq-HoTT
+
+  definition loop_susp_unit [constructor] (X : Pointed) : X →* Ω(Susp X) :=
+  begin
+    fapply pmap.mk,
+    { intro x, exact merid x ⬝ (merid pt)⁻¹},
+    { apply con.right_inv},
+  end
+
+  definition loop_susp_unit_natural {X Y : Pointed} (f : X →* Y)
+    : loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X :=
+  begin
+    induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
+    fapply phomotopy.mk,
+    { intro x', esimp [Susp_functor],
+      refine _ ⬝ !idp_con⁻¹,
+      refine _ ⬝ !ap_con⁻¹,
+      exact (!elim_merid ◾ (!ap_inv ⬝ inverse2 !elim_merid))⁻¹},
+    { rewrite [▸*,idp_con (con.right_inv _)],
+      exact sorry}, --apply inv_con_eq_of_eq_con,
+  end
+
+-- p ⬝ q ⬝ r means (p ⬝ q) ⬝ r
+
+  definition susp_adjoint_loop (A B : Pointed)
+    : map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) := sorry
+
+exit
+
+Definition loop_susp_unit_natural {X Y : pType} (f : X ->* Y)
+: loop_susp_unit Y o* f
+  ==* loops_functor (psusp_functor f) o* loop_susp_unit X.
+Proof.
+  pointed_reduce.
+  refine (Build_pHomotopy _ _); cbn.
+  - intros x; symmetry.
+    refine (concat_1p _@ (concat_p1 _ @ _)).
+    refine (ap_pp (Susp_rec North South (merid o f))
+                  (merid x) (merid (point X))^ @ _).
+    refine ((1 @@ ap_V _ _) @ _).
+    refine (Susp_comp_nd_merid _ @@ inverse2 (Susp_comp_nd_merid _)).
+  - cbn. rewrite !inv_pp, !concat_pp_p, concat_1p; symmetry.
+    apply moveL_Vp.
+    refine (concat_pV_inverse2 _ _ (Susp_comp_nd_merid (point X)) @ _).
+    do 2 apply moveL_Vp.
+    refine (ap_pp_concat_pV _ _ @ _).
+    do 2 apply moveL_Vp.
+    rewrite concat_p1_1, concat_1p_1.
+    cbn; symmetry.
+    refine (concat_p1 _ @ _).
+    refine (ap_compose (fun p' => (ap (Susp_rec North South (merid o f))) p' @ 1)
+                       (fun p' => 1 @ p')
+                       (concat_pV (merid (point X))) @ _).
+    apply ap.
+    refine (ap_compose (ap (Susp_rec North South (merid o f)))
+                       (fun p' => p' @ 1) _).
+Qed.
+
+Definition loop_susp_counit (X : pType) : psusp (loops X) ->* X.
+Proof.
+  refine (Build_pMap (psusp (loops X)) X
+                     (Susp_rec (point X) (point X) idmap) 1).
+Defined.
+
+Definition loop_susp_counit_natural {X Y : pType} (f : X ->* Y)
+: f o* loop_susp_counit X
+  ==* loop_susp_counit Y o* psusp_functor (loops_functor f).
+Proof.
+  pointed_reduce.
+  refine (Build_pHomotopy _ _); simpl.
+  - refine (Susp_ind _ _ _ _); cbn; try reflexivity; intros p.
+    rewrite transport_paths_FlFr, ap_compose, concat_p1.
+    apply moveR_Vp.
+    refine (ap_compose
+              (Susp_rec North South (fun x0 => merid (1 @ (ap f x0 @ 1))))
+              (Susp_rec (point Y) (point Y) idmap) (merid p) @ _).
+    do 2 rewrite Susp_comp_nd_merid.
+    refine (Susp_comp_nd_merid _ @ _). (** Not sure why [rewrite] fails here *)
+    apply concat_1p.
+  - reflexivity.
+Qed.
+
+(** Now the triangle identities *)
+
+Definition loop_susp_triangle1 (X : pType)
+: loops_functor (loop_susp_counit X) o* loop_susp_unit (loops X)
+  ==* pmap_idmap (loops X).
+Proof.
+  refine (Build_pHomotopy _ _).
+  - intros p; cbn.
+    refine (concat_1p _ @ (concat_p1 _ @ _)).
+    refine (ap_pp (Susp_rec (point X) (point X) idmap)
+                  (merid p) (merid (point (point X = point X)))^ @ _).
+    refine ((1 @@ ap_V _ _) @ _).
+    refine ((Susp_comp_nd_merid p @@ inverse2 (Susp_comp_nd_merid (point (loops X)))) @ _).
+    exact (concat_p1 _).
+  - destruct X as [X x]; cbn; unfold point.
+    apply whiskerR.
+    rewrite (concat_pV_inverse2
+               (ap (Susp_rec x x idmap) (merid 1))
+               1 (Susp_comp_nd_merid 1)).
+    rewrite (ap_pp_concat_pV (Susp_rec x x idmap) (merid 1)).
+    rewrite ap_compose, (ap_compose _ (fun p => p @ 1)).
+    rewrite concat_1p_1; apply ap.
+    apply concat_p1_1.
+Qed.
+
+Definition loop_susp_triangle2 (X : pType)
+: loop_susp_counit (psusp X) o* psusp_functor (loop_susp_unit X)
+  ==* pmap_idmap (psusp X).
+Proof.
+  refine (Build_pHomotopy _ _);
+  [ refine (Susp_ind _ _ _ _) | ]; try reflexivity; cbn.
+  - exact (merid (point X)).
+  - intros x.
+    rewrite transport_paths_FlFr, ap_idmap, ap_compose.
+    rewrite Susp_comp_nd_merid.
+    apply moveR_pM; rewrite concat_p1.
+    refine (inverse2 (Susp_comp_nd_merid _) @ _).
+    rewrite inv_pp, inv_V; reflexivity.
+Qed.
+
+(** Now we can finally construct the adjunction equivalence. *)
+
+Definition loop_susp_adjoint `{Funext} (A B : pType)
+: (psusp A ->* B) <~> (A ->* loops B).
+Proof.
+  refine (equiv_adjointify
+            (fun f => loops_functor f o* loop_susp_unit A)
+            (fun g => loop_susp_counit B o* psusp_functor g) _ _).
+  - intros g. apply path_pmap.
+    refine (pmap_prewhisker _ (loops_functor_compose _ _) @* _).
+    refine (pmap_compose_assoc _ _ _ @* _).
+    refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
+    refine ((pmap_compose_assoc _ _ _)^* @* _).
+    refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
+    apply pmap_postcompose_idmap.
+  - intros f. apply path_pmap.
+    refine (pmap_postwhisker _ (psusp_functor_compose _ _) @* _).
+    refine ((pmap_compose_assoc _ _ _)^* @* _).
+    refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
+    refine (pmap_compose_assoc _ _ _ @* _).
+    refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
+    apply pmap_precompose_idmap.
+Defined.
+
+(** And its naturality is easy. *)
+
+Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType)
+           (f : psusp A ->* B) (g : B ->* B')
+: loop_susp_adjoint A B' (g o* f)
+  ==* loops_functor g o* loop_susp_adjoint A B f.
+Proof.
+  cbn.
+  refine (_ @* pmap_compose_assoc _ _ _).
+  apply pmap_prewhisker.
+  refine (loops_functor_compose g f).
+Defined.
+
+Definition loop_susp_adjoint_nat_l `{Funext} (A A' B : pType)
+           (f : A ->* loops B) (g : A' ->* A)
+: (loop_susp_adjoint A' B)^-1 (f o* g)
+  ==* (loop_susp_adjoint A B)^-1 f o* psusp_functor g.
+Proof.
+  cbn.
+  refine (_ @* (pmap_compose_assoc _ _ _)^*).
+  apply pmap_postwhisker.
+  refine (psusp_functor_compose f g).
+Defined.
+
+
+
+  definition susp_adjoint_loop (A B : Pointed)
+    : map₊ (pointed.mk' (susp A)) B ≃ map₊ A (Ω B) :=
+  begin
+    fapply equiv.MK,
+    { intro f, fapply pointed_map.mk,
+       intro a, refine !respect_pt⁻¹ ⬝ ap f (merid a ⬝ (merid pt)⁻¹) ⬝ !respect_pt,
+       refine ap _ !con.right_inv ⬝ !con.left_inv},
+    { intro g, fapply pointed_map.mk,
+      { esimp, intro a, induction a,
+          exact pt,
+          exact pt,
+          exact g a} ,
+      { reflexivity}},
+    { intro g, fapply pointed_map_eq,
+        intro a, esimp [respect_pt], refine !idp_con ⬝ !ap_con ⬝ ap _ !ap_inv
+           ⬝ ap _ !elim_merid ⬝ ap _ !elim_merid ⬝ ap _ (respect_pt g) ⬝ _, exact idp,
+        -- rewrite [ap_con,ap_inv,+elim_merid,idp_con,respect_pt],
+       esimp, exact sorry},
+    { intro f, fapply pointed_map_eq,
+      { esimp, intro a, induction a; all_goals esimp,
+          exact !respect_pt⁻¹,
+          exact !respect_pt⁻¹ ⬝ ap f (merid pt),
+          apply pathover_eq, exact sorry},
+      { esimp, exact !con.left_inv⁻¹}},
+  end
+
+end susp
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
deleted file mode 100644
index 9005d100e5..0000000000
--- a/hott/hit/suspension.hlean
+++ /dev/null
@@ -1,111 +0,0 @@
-/-
-Copyright (c) 2015 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
-
-Declaration of suspension
--/
-
-import .pushout types.pointed
-
-open pushout unit eq equiv equiv.ops pointed
-
-definition suspension (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
-
-namespace suspension
-  variable {A : Type}
-
-  definition north (A : Type) : suspension A :=
-  inl _ _ star
-
-  definition south (A : Type) : suspension A :=
-  inr _ _ star
-
-  definition merid (a : A) : north A = south A :=
-  glue _ _ a
-
-  protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), PN =[merid a] PS) (x : suspension A) : P x :=
-  begin
-    fapply pushout.rec_on _ _ x,
-    { intro u, cases u, exact PN},
-    { intro u, cases u, exact PS},
-    { exact Pm},
-  end
-
-  protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A)
-    (PN : P !north) (PS : P !south) (Pm : Π(a : A), PN =[merid a] PS) : P y :=
-  suspension.rec PN PS Pm y
-
-  theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), PN =[merid a] PS) (a : A)
-      : apdo (suspension.rec PN PS Pm) (merid a) = Pm a :=
-  !rec_glue
-
-  protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
-    (x : suspension A) : P :=
-  suspension.rec PN PS (λa, pathover_of_eq (Pm a)) x
-
-  protected definition elim_on [reducible] {P : Type} (x : suspension A)
-    (PN : P) (PS : P)  (Pm : A → PN = PS) : P :=
-  suspension.elim PN PS Pm x
-
-  theorem elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (a : A)
-    : ap (suspension.elim PN PS Pm) (merid a) = Pm a :=
-  begin
-    apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑suspension.elim,rec_merid],
-  end
-
-  protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
-    (x : suspension A) : Type :=
-  suspension.elim PN PS (λa, ua (Pm a)) x
-
-  protected definition elim_type_on [reducible] (x : suspension A)
-    (PN : Type) (PS : Type)  (Pm : A → PN ≃ PS) : Type :=
-  suspension.elim_type PN PS Pm x
-
-  theorem elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
-    (a : A) : transport (suspension.elim_type PN PS Pm) (merid a) = Pm a :=
-  by rewrite [tr_eq_cast_ap_fn,↑suspension.elim_type,elim_merid];apply cast_ua_fn
-
-end suspension
-
-attribute suspension.north suspension.south [constructor]
-attribute suspension.rec suspension.elim [unfold-c 6] [recursor 6]
-attribute suspension.elim_type [unfold-c 5]
-attribute suspension.rec_on suspension.elim_on [unfold-c 3]
-attribute suspension.elim_type_on [unfold-c 2]
-
-namespace suspension
-
-  definition pointed_suspension [instance] [constructor] (A : Type) : pointed (suspension A) :=
-  pointed.mk !north
-
-  definition suspension_adjoint_loop (A B : Pointed)
-    : map₊ (pointed.mk' (suspension A)) B ≃ map₊ A (Ω B) :=
-  begin
-    fapply equiv.MK,
-    { intro f, fapply pointed_map.mk,
-       intro a, refine !respect_pt⁻¹ ⬝ ap f (merid a ⬝ (merid pt)⁻¹) ⬝ !respect_pt,
-       refine ap _ !con.right_inv ⬝ !con.left_inv},
-    { intro g, fapply pointed_map.mk,
-      { esimp, intro a, induction a,
-          exact pt,
-          exact pt,
-          exact g a} ,
-      { reflexivity}},
-    { intro g, fapply pointed_map_eq,
-        intro a, esimp [respect_pt], refine !idp_con ⬝ !ap_con ⬝ ap _ !ap_inv
-           ⬝ ap _ !elim_merid ⬝ ap _ !elim_merid ⬝ ap _ (respect_pt g) ⬝ _, exact idp,
-        -- rewrite [ap_con,ap_inv,+elim_merid,idp_con,respect_pt],
-       esimp, exact sorry},
-    { intro f, fapply pointed_map_eq,
-      { esimp, intro a, induction a; all_goals esimp,
-          exact !respect_pt⁻¹,
-          exact !respect_pt⁻¹ ⬝ ap f (merid pt),
-          apply pathover_eq, exact sorry},
-      { esimp, exact !con.left_inv⁻¹}},
-  end
-
-end suspension
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 7528acacce..4318ccf078 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -55,10 +55,10 @@ namespace trunc
   λxx, trunc.rec_on xx (λx, tr (f x))
 
   definition trunc_functor_compose (f : X → Y) (g : Y → Z)
-    : trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f :=
+    : trunc_functor n (g ∘ f) ~ trunc_functor n g ∘ trunc_functor n f :=
   λxx, trunc.rec_on xx (λx, idp)
 
-  definition trunc_functor_id : trunc_functor n (@id A) ∼ id :=
+  definition trunc_functor_id : trunc_functor n (@id A) ~ id :=
   λxx, trunc.rec_on xx (λx, idp)
 
   definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) :=
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 10849f07ee..56fdbe300a 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -17,8 +17,8 @@ open eq function lift
 structure is_equiv [class] {A B : Type} (f : A → B) :=
 mk' ::
   (inv : B → A)
-  (right_inv : (f ∘ inv) ∼ id)
-  (left_inv : (inv ∘ f) ∼ id)
+  (right_inv : (f ∘ inv) ~ id)
+  (left_inv : (inv ∘ f) ~ id)
   (adj : Πx, right_inv (f x) = ap f (left_inv x))
 
 attribute is_equiv.inv [quasireducible]
@@ -60,48 +60,15 @@ namespace is_equiv
 
   -- Any function equal to an equivalence is an equivlance as well.
   variable {f}
-  definition is_equiv_eq_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') :=
-     eq.rec_on Heq Hf
-
-  -- Any function pointwise equal to an equivalence is an equivalence as well.
-  definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
-    let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ right_inv f b) in
-    let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ left_inv f a) in
-    let adj' := (λ (a : A),
-      let ff'a := Hty a in
-      let invf := inv f in
-      let secta := left_inv f a in
-      let retrfa := right_inv f (f a) in
-      let retrf'a := right_inv f (f' a) in
-      have eq1 : _ = _,
-        from calc ap f secta ⬝ ff'a
-              = retrfa ⬝ ff'a                 : by rewrite adj
-          ... = ap (f ∘ invf) ff'a ⬝ retrf'a  : by rewrite ap_con_eq_con
-          ... = ap f (ap invf ff'a) ⬝ retrf'a : by rewrite ap_compose,
-      have eq2 : _ = _,
-        from calc retrf'a
-              = (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a)   : eq_inv_con_of_con_eq eq1⁻¹
-          ... = (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_inv invf ff'a
-          ... = (ap f (ap invf ff'a))⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : by rewrite ap_con_eq_con_ap
-          ... = ((ap f (ap invf ff'a))⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : by rewrite con.assoc
-          ... = (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta   : by rewrite ap_inv
-          ... = (Hty (invf (f' a)) ⬝ ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_con_eq_con_ap
-          ... = (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : by rewrite ap_inv
-          ... = Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : by rewrite con.assoc,
-      have eq3 : _ = _,
-        from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
-              = (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : inv_con_eq_of_eq_con eq2
-          ... = (ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_inv
-          ... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta)       : by rewrite ap_con,
-    eq3) in
-  is_equiv.mk f' (inv f) sect' retr' adj'
+  definition is_equiv_eq_closed [Hf : is_equiv f] (Heq : f = f') : is_equiv f' :=
+  eq.rec_on Heq Hf
   end
 
   section
   parameters {A B : Type} (f : A → B) (g : B → A)
-            (ret : f ∘ g ∼ id) (sec : g ∘ f ∼ id)
+            (ret : f ∘ g ~ id) (sec : g ∘ f ~ id)
 
-  private definition adjointify_sect' : g ∘ f ∼ id :=
+  private definition adjointify_sect' : g ∘ f ~ id :=
     (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
 
   private definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) :=
@@ -137,9 +104,23 @@ namespace is_equiv
 
   definition adjointify [constructor] : is_equiv f :=
   is_equiv.mk f g ret adjointify_sect' adjointify_adj'
-
   end
 
+  -- Any function pointwise equal to an equivalence is an equivalence as well.
+  definition homotopy_closed [constructor] {A B : Type} {f f' : A → B} [Hf : is_equiv f]
+    (Hty : f ~ f') : is_equiv f' :=
+  adjointify f'
+             (inv f)
+             (λ b, (Hty (inv f b))⁻¹ ⬝ right_inv f b)
+             (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ left_inv f a)
+
+  definition inv_homotopy_closed [constructor] {A B : Type} {f : A → B} {f' : B → A}
+    [Hf : is_equiv f] (Hty : f⁻¹ ~ f') : is_equiv f :=
+  adjointify f
+             f'
+             (λ b, ap f !Hty⁻¹ ⬝ right_inv f b)
+             (λ a, !Hty⁻¹ ⬝ left_inv f a)
+
   definition is_equiv_up [instance] (A : Type) : is_equiv (up : A → lift A) :=
   adjointify up down (λa, by induction a;reflexivity) (λa, idp)
 
@@ -248,12 +229,12 @@ namespace equiv
   variables {A B C : Type}
 
   protected definition MK [reducible] [constructor] (f : A → B) (g : B → A)
-    (right_inv : f ∘ g ∼ id) (left_inv : g ∘ f ∼ id) : A ≃ B :=
+    (right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B :=
   equiv.mk f (adjointify f g right_inv left_inv)
 
   definition to_inv [reducible] [unfold-c 3] (f : A ≃ B) : B → A := f⁻¹
-  definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f
-  definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f
+  definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f
+  definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f
 
   protected definition refl [refl] [constructor] : A ≃ A :=
   equiv.mk id !is_equiv_id
@@ -269,8 +250,12 @@ namespace equiv
     -- notation for inverse which is not overloaded
   abbreviation erfl [constructor] := @equiv.refl
 
-  definition equiv_of_eq_fn_of_equiv [constructor] (f : A ≃ B) {f' : A → B} (Heq : f = f') : A ≃ B :=
-  equiv.mk f' (is_equiv_eq_closed Heq)
+  definition equiv_change_fun [constructor] (f : A ≃ B) {f' : A → B} (Heq : f ~ f') : A ≃ B :=
+  equiv.mk f' (is_equiv.homotopy_closed Heq)
+
+  definition equiv_change_inv [constructor] (f : A ≃ B) {f' : B → A} (Heq : f⁻¹ ~ f')
+    : A ≃ B :=
+  equiv.mk f (inv_homotopy_closed Heq)
 
   --rename: eq_equiv_fn_eq_of_is_equiv
   definition eq_equiv_fn_eq [constructor] (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index e322b6a339..ac6150f927 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -23,7 +23,7 @@ definition funext.{l k} :=
 
 -- Naive funext is the simple assertion that pointwise equal functions are equal.
 definition naive_funext :=
-  Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
+  Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ~ g) → f = g
 
 -- Weak funext says that a product of contractible types is contractible.
 definition weak_funext :=
@@ -33,7 +33,7 @@ definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
   (λ nf A P (Pc : Πx, is_contr (P x)),
     let c := λx, center (P x) in
     is_contr.mk c (λ f,
-      have eq' : (λx, center (P x)) ∼ f,
+      have eq' : (λx, center (P x)) ~ f,
         from (λx, center_eq (f x)),
       have eq : (λx, center (P x)) = f,
         from nf A P (λx, center (P x)) f eq',
@@ -52,12 +52,12 @@ section
   universe variables l k
   parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
 
-  definition is_contr_sigma_homotopy : is_contr (Σ (g : Π x, B x), f ∼ g) :=
+  definition is_contr_sigma_homotopy : is_contr (Σ (g : Π x, B x), f ~ g) :=
     is_contr.mk (sigma.mk f (homotopy.refl f))
       (λ dp, sigma.rec_on dp
-        (λ (g : Π x, B x) (h : f ∼ g),
+        (λ (g : Π x, B x) (h : f ~ g),
           let r := λ (k : Π x, Σ y, f x = y),
-            @sigma.mk _ (λg, f ∼ g)
+            @sigma.mk _ (λg, f ~ g)
               (λx, pr1 (k x)) (λx, pr2 (k x)) in
           let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
           have t1 : Πx, is_contr (Σ y, f x = y),
@@ -75,9 +75,9 @@ section
       )
   local attribute is_contr_sigma_homotopy [instance]
 
-  parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
+  parameters (Q : Π g (h : f ~ g), Type) (d : Q f (homotopy.refl f))
 
-  definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
+  definition homotopy_ind (g : Πx, B x) (h : f ~ g) : Q g h :=
     @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
       (@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d
 
@@ -100,9 +100,9 @@ theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
       proof homotopy_ind_comp f eq_to_f idp qed,
     assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
       proof ap apd10 t1 qed,
-    have left_inv : apd10 ∘ (sim2path g) ∼ id,
+    have left_inv : apd10 ∘ (sim2path g) ~ id,
       proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed,
-    have right_inv : (sim2path g) ∘ apd10 ∼ id,
+    have right_inv : (sim2path g) ∘ apd10 ~ id,
       from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)),
     is_equiv.adjointify apd10 (sim2path g) left_inv right_inv
 
@@ -181,8 +181,8 @@ section
 
   set_option class.conservative false
   theorem nondep_funext_from_ua {A : Type} {B : Type}
-      : Π {f g : A → B}, f ∼ g → f = g :=
-    (λ (f g : A → B) (p : f ∼ g),
+      : Π {f g : A → B}, f ~ g → f = g :=
+    (λ (f g : A → B) (p : f ~ g),
         let d := λ (x : A), sigma.mk (f x , f x) idp in
         let e := λ (x : A), sigma.mk (f x , g x) (p x) in
         let precomp1 :=  compose (pr₁ ∘ pr1) in
@@ -237,13 +237,13 @@ end funext
 
 open funext
 
-definition eq_equiv_homotopy : (f = g) ≃ (f ∼ g) :=
+definition eq_equiv_homotopy : (f = g) ≃ (f ~ g) :=
 equiv.mk apd10 _
 
-definition eq_of_homotopy [reducible] : f ∼ g → f = g :=
+definition eq_of_homotopy [reducible] : f ~ g → f = g :=
 (@apd10 A P f g)⁻¹
 
-definition apd10_eq_of_homotopy (p : f ∼ g) : apd10 (eq_of_homotopy p) = p :=
+definition apd10_eq_of_homotopy (p : f ~ g) : apd10 (eq_of_homotopy p) = p :=
 right_inv apd10 p
 
 definition eq_of_homotopy_apd10 (p : f = g) : eq_of_homotopy (apd10 p) = p :=
@@ -255,9 +255,9 @@ is_equiv.left_inv apd10 idp
 definition naive_funext_of_ua : naive_funext :=
 λ A P f g h, eq_of_homotopy h
 
-protected definition homotopy.rec_on [recursor] {Q : (f ∼ g) → Type} (p : f ∼ g)
+protected definition homotopy.rec_on [recursor] {Q : (f ~ g) → Type} (p : f ~ g)
   (H : Π(q : f = g), Q (apd10 q)) : Q p :=
 right_inv apd10 p ▸ H (eq_of_homotopy p)
 
-protected definition homotopy.rec_on_idp [recursor] {Q : Π{g}, (f ∼ g) → Type} {g : Π x, P x} (p : f ∼ g) (H : Q (homotopy.refl f)) : Q p :=
+protected definition homotopy.rec_on_idp [recursor] {Q : Π{g}, (f ~ g) → Type} {g : Π x, P x} (p : f ~ g) (H : Q (homotopy.refl f)) : Q p :=
 homotopy.rec_on p (λq, eq.rec_on q H)
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index 4eb56e024b..da1fd0e3b4 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -16,7 +16,7 @@ open is_trunc eq
   We take two higher inductive types (hits) as primitive notions in Lean. We define all other hits
   in terms of these two hits. The hits which are primitive are
     - n-truncation
-    - quotients (non-truncated quotients)
+    - quotients (not truncated)
   For each of the hits we add the following constants:
     - the type formation
     - the term and path constructors
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index c8c65a0141..65f7ead770 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -42,13 +42,13 @@ definition rfl {A : Type} {a : A} := eq.refl a
 namespace eq
   variables {A : Type} {a b c : A}
 
-  definition subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
+  definition subst [unfold-c 5] {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
   eq.rec H₂ H₁
 
-  definition trans (H₁ : a = b) (H₂ : b = c) : a = c :=
+  definition trans [unfold-c 5] (H₁ : a = b) (H₂ : b = c) : a = c :=
   subst H₂ H₁
 
-  definition symm (H : a = b) : b = a :=
+  definition symm [unfold-c 4] (H : a = b) : b = a :=
   subst H (refl a)
 
   namespace ops
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 8d55e08969..7a8005029d 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -206,28 +206,26 @@ namespace eq
   definition homotopy [reducible] (f g : Πx, P x) : Type :=
   Πx : A, f x = g x
 
-  infix  ∼ := homotopy
+  infix ~ := homotopy
 
-  namespace homotopy
-  protected definition refl [refl] [reducible] (f : Πx, P x) : f ∼ f :=
+  protected definition homotopy.refl [refl] [reducible] (f : Πx, P x) : f ~ f :=
   λ x, idp
 
-  protected definition symm [symm] [reducible] {f g : Πx, P x} (H : f ∼ g) : g ∼ f :=
+  protected definition homotopy.symm [symm] [reducible] {f g : Πx, P x} (H : f ~ g) : g ~ f :=
   λ x, (H x)⁻¹
 
-  protected definition trans [trans] [reducible] {f g h : Πx, P x} (H1 : f ∼ g) (H2 : g ∼ h)
-    : f ∼ h :=
+  protected definition homotopy.trans [trans] [reducible] {f g h : Πx, P x} (H1 : f ~ g) (H2 : g ~ h)
+    : f ~ h :=
   λ x, H1 x ⬝ H2 x
-  end homotopy
 
-  definition apd10 [unfold-c 5] {f g : Πx, P x} (H : f = g) : f ∼ g :=
+  definition apd10 [unfold-c 5] {f g : Πx, P x} (H : f = g) : f ~ g :=
   λx, eq.rec_on H idp
 
   --the next theorem is useful if you want to write "apply (apd10' a)"
   definition apd10' [unfold-c 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a :=
   eq.rec_on H idp
 
-  definition ap10 [reducible] [unfold-c 5] {f g : A → B} (H : f = g) : f ∼ g := apd10 H
+  definition ap10 [reducible] [unfold-c 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H
 
   definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
   eq.rec_on H (eq.rec_on p idp)
@@ -286,6 +284,7 @@ namespace eq
   definition ap_id (p : x = y) : ap id p = p :=
   eq.rec_on p idp
 
+  -- TODO: interchange arguments f and g
   definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x = y) :
     ap (g ∘ f) p = ap g (ap f p) :=
   eq.rec_on p idp
@@ -300,33 +299,38 @@ namespace eq
   eq.rec_on p idp
 
   -- Naturality of [ap].
-  definition ap_con_eq_con_ap {f g : A → B} (p : f ∼ g) {x y : A} (q : x = y) :
+  definition ap_con_eq_con_ap {f g : A → B} (p : f ~ g) {x y : A} (q : x = y) :
     ap f q ⬝ p y = p x ⬝ ap g q :=
-  eq.rec_on q (!idp_con ⬝ !con_idp⁻¹)
+  eq.rec_on q !idp_con
 
   -- Naturality of [ap] at identity.
   definition ap_con_eq_con {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) :
     ap f q ⬝ p y = p x ⬝ q :=
-  eq.rec_on q (!idp_con ⬝ !con_idp⁻¹)
+  eq.rec_on q !idp_con
 
   definition con_ap_eq_con {f : A → A} (p : Πx, x = f x) {x y : A} (q : x = y) :
     p x ⬝ ap f q =  q ⬝ p y :=
-  eq.rec_on q (!con_idp ⬝ !idp_con⁻¹)
+  eq.rec_on q !idp_con⁻¹
+
+  -- Naturality of [ap] with constant function
+  definition ap_con_eq {f : A → B} {b : B} (p : Πx, f x = b) {x y : A} (q : x = y) :
+    ap f q ⬝ p y = p x :=
+  eq.rec_on q !idp_con
 
   -- Naturality with other paths hanging around.
 
-  definition con_ap_con_con_eq_con_con_ap_con {f g : A → B} (p : f ∼ g) {x y : A} (q : x = y)
+  definition con_ap_con_con_eq_con_con_ap_con {f g : A → B} (p : f ~ g) {x y : A} (q : x = y)
       {w z : B} (r : w = f x) (s : g y = z) :
     (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (ap g q ⬝ s) :=
   eq.rec_on s (eq.rec_on q idp)
 
-  definition con_ap_con_eq_con_con_ap {f g : A → B} (p : f ∼ g) {x y : A} (q : x = y)
+  definition con_ap_con_eq_con_con_ap {f g : A → B} (p : f ~ g) {x y : A} (q : x = y)
       {w : B} (r : w = f x) :
     (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ ap g q :=
   eq.rec_on q idp
 
   -- TODO: try this using the simplifier, and compare proofs
-  definition ap_con_con_eq_con_ap_con {f g : A → B} (p : f ∼ g) {x y : A} (q : x = y)
+  definition ap_con_con_eq_con_ap_con {f g : A → B} (p : f ~ g) {x y : A} (q : x = y)
       {z : B} (s : g y = z) :
     ap f q ⬝ (p y ⬝ s) = p x ⬝ (ap g q ⬝ s) :=
   eq.rec_on s (eq.rec_on q
@@ -337,32 +341,32 @@ namespace eq
   -- This also works:
   -- eq.rec_on s (eq.rec_on q (!idp_con ▸ idp))
 
-  definition con_ap_con_con_eq_con_con_con {f : A → A} (p : f ∼ id) {x y : A} (q : x = y)
+  definition con_ap_con_con_eq_con_con_con {f : A → A} (p : f ~ id) {x y : A} (q : x = y)
       {w z : A} (r : w = f x) (s : y = z) :
     (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (q ⬝ s) :=
   eq.rec_on s (eq.rec_on q idp)
 
-  definition con_con_ap_con_eq_con_con_con {g : A → A} (p : id ∼ g) {x y : A} (q : x = y)
+  definition con_con_ap_con_eq_con_con_con {g : A → A} (p : id ~ g) {x y : A} (q : x = y)
       {w z : A} (r : w = x) (s : g y = z) :
     (r ⬝ p x) ⬝ (ap g q ⬝ s) = (r ⬝ q) ⬝ (p y ⬝ s) :=
   eq.rec_on s (eq.rec_on q idp)
 
-  definition con_ap_con_eq_con_con {f : A → A} (p : f ∼ id) {x y : A} (q : x = y)
+  definition con_ap_con_eq_con_con {f : A → A} (p : f ~ id) {x y : A} (q : x = y)
       {w : A} (r : w = f x) :
     (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ q :=
   eq.rec_on q idp
 
-  definition ap_con_con_eq_con_con {f : A → A} (p : f ∼ id) {x y : A} (q : x = y)
+  definition ap_con_con_eq_con_con {f : A → A} (p : f ~ id) {x y : A} (q : x = y)
       {z : A} (s : y = z) :
     ap f q ⬝ (p y ⬝ s) = p x ⬝ (q ⬝ s) :=
   eq.rec_on s (eq.rec_on q (!idp_con ▸ idp))
 
-  definition con_con_ap_eq_con_con {g : A → A} (p : id ∼ g) {x y : A} (q : x = y)
+  definition con_con_ap_eq_con_con {g : A → A} (p : id ~ g) {x y : A} (q : x = y)
       {w : A} (r : w = x) :
     (r ⬝ p x) ⬝ ap g q = (r ⬝ q) ⬝ p y :=
   begin cases q, exact idp end
 
-  definition con_ap_con_eq_con_con' {g : A → A} (p : id ∼ g) {x y : A} (q : x = y)
+  definition con_ap_con_eq_con_con' {g : A → A} (p : id ~ g) {x y : A} (q : x = y)
       {z : A} (s : g y = z) :
     p x ⬝ (ap g q ⬝ s) = q ⬝ (p y ⬝ s) :=
   begin
@@ -654,4 +658,10 @@ namespace eq
       ⬝ con.assoc' _ _ _
       ⬝ (whisker_right (tr2_con r1 r2 (f x))⁻¹ (apd f p3)) :=
   eq.rec_on r2 (eq.rec_on r1 (eq.rec_on p1 idp))
+
+  -- Naturality of [ap] with constant function over a loop
+  definition ap_eq_idp {f : A → B} {b : B} (p : Πx, f x = b) {x : A} (q : x = x) :
+    ap f q = idp :=
+  cancel_right (ap_con_eq p q ⬝ !idp_con⁻¹)
+
 end eq
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index c413085f56..c74ba3807a 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -187,6 +187,12 @@ namespace eq
   definition pathover_tr_of_pathover {p : a = a₃} (q : b =[p ⬝ p₂⁻¹] b₂) : b =[p] p₂ ▸ b₂ :=
   by cases p₂;exact q
 
+  definition pathover_tr_of_eq (q : b = b') : b =[p] p ▸ b' :=
+  by cases q;apply pathover_tr
+
+  definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' :=
+  by cases q;apply tr_pathover
+
   definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
       : f a b = f a₂ b₂ :=
   by cases Hb; exact idp
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index edad036d55..dbf2d60f07 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -43,7 +43,7 @@ reserve infix `↔`:20
 reserve infix `=`:50
 reserve infix `≠`:50
 reserve infix `≈`:50
-reserve infix `∼`:50
+reserve infix `~`:50
 reserve infix `≡`:50
 
 reserve infixr `∘`:60                   -- input with \comp
diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean
index caa579f678..576e7d4b3a 100644
--- a/hott/types/arrow.hlean
+++ b/hott/types/arrow.hlean
@@ -47,7 +47,7 @@ namespace pi
   /- Transport -/
 
   definition arrow_transport {B C : A → Type} (p : a = a') (f : B a → C a)
-    : (transport (λa, B a → C a) p f) ∼ (λb, p ▸ f (p⁻¹ ▸ b)) :=
+    : (transport (λa, B a → C a) p f) ~ (λb, p ▸ f (p⁻¹ ▸ b)) :=
   eq.rec_on p (λx, idp)
 
   /- Pathovers -/
diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean
index b1bdbc128c..1d95aec403 100644
--- a/hott/types/cubical/square.hlean
+++ b/hott/types/cubical/square.hlean
@@ -5,7 +5,7 @@ Author: Floris van Doorn
 
 Squares in a type
 -/
-
+import types.eq
 open eq equiv is_equiv
 
 namespace eq
@@ -60,24 +60,18 @@ namespace eq
   definition eq_of_square (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ :=
   by cases s₁₁; apply idp
 
-  definition hdeg_square {p q : a = a'} (r : p = q) : square idp idp p q :=
-  by cases r;apply hrefl
-
-  definition vdeg_square {p q : a = a'} (r : p = q) : square p q idp idp :=
-  by cases r;apply vrefl
-
   definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
-  by cases p₁₂; (esimp [concat] at r); cases r; cases p₂₁; cases p₁₀; exact ids
+  by cases p₁₂; esimp [concat] at r; cases r; cases p₂₁; cases p₁₀; exact ids
 
   definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
     : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) :=
   by cases s₁₁;exact ids
 
-  definition square_of_homotopy {B : Type} {f g : A → B} (H : f ∼ g) (p : a = a')
+  definition square_of_homotopy {B : Type} {f g : A → B} (H : f ~ g) (p : a = a')
     : square (H a) (H a') (ap f p) (ap g p) :=
   by cases p; apply vrefl
 
-  definition square_of_homotopy' {B : Type} {f g : A → B} (H : f ∼ g) (p : a = a')
+  definition square_of_homotopy' {B : Type} {f g : A → B} (H : f ~ g) (p : a = a')
     : square (ap f p) (ap g p) (H a) (H a') :=
   by cases p; apply hrefl
 
@@ -91,7 +85,51 @@ namespace eq
     { intro s, cases s, apply idp},
   end
 
-  definition natural_square [unfold-c 8] {f g : A → B} (p : f ∼ g) (q : a = a') :
+  definition hdeg_square {p q : a = a'} (r : p = q) : square idp idp p q :=
+  by cases r;apply hrefl
+
+  definition vdeg_square {p q : a = a'} (r : p = q) : square p q idp idp :=
+  by cases r;apply vrefl
+
+  definition hdeg_square_equiv' [constructor] (p q : a = a') : square idp idp p q ≃ p = q :=
+  by transitivity _;apply square_equiv_eq;transitivity _;apply eq_equiv_eq_symm;
+     apply equiv_eq_closed_right;apply idp_con
+
+  definition vdeg_square_equiv' [constructor] (p q : a = a') : square p q idp idp ≃ p = q :=
+  by transitivity _;apply square_equiv_eq;apply equiv_eq_closed_right; apply idp_con
+
+  definition eq_of_hdeg_square [reducible] {p q : a = a'} (s : square idp idp p q) : p = q :=
+  to_fun !hdeg_square_equiv' s
+
+  definition eq_of_vdeg_square [reducible] {p q : a = a'} (s : square p q idp idp) : p = q :=
+  to_fun !vdeg_square_equiv' s
+
+  /-
+    the following two equivalences have as underlying inverse function the functions
+    hdeg_square and vdeg_square, respectively
+  -/
+  definition hdeg_square_equiv [constructor] (p q : a = a') : square idp idp p q ≃ p = q :=
+  begin
+    fapply equiv_change_fun,
+    { fapply equiv_change_inv, apply hdeg_square_equiv', exact hdeg_square,
+        intro s, cases s, cases p, reflexivity},
+    { exact eq_of_hdeg_square},
+    { reflexivity}
+  end
+
+  definition vdeg_square_equiv [constructor] (p q : a = a') : square p q idp idp ≃ p = q :=
+  begin
+    fapply equiv_change_fun,
+    { fapply equiv_change_inv, apply vdeg_square_equiv',exact vdeg_square,
+        intro s, cases s, cases p, reflexivity},
+    { exact eq_of_vdeg_square},
+    { reflexivity}
+  end
+
+  -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails
+  example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp
+
+  definition natural_square [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
 
@@ -154,12 +192,41 @@ namespace eq
     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
 
-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
 
+  definition pathover_eq {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
+    (s : square q r (ap f p) (ap g p)) : q =[p] r :=
+  by cases p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s
+
+  definition square_of_pathover {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'}
+    (s : q =[p] r) : square q r (ap f p) (ap g p) :=
+  by cases p;apply vdeg_square;exact eq_of_pathover_idp s
+exit
+  definition pathover_eq_equiv_square {f g : A → B} (p : a = a') (q : f a = g a) (r : f a' = g a')
+    : square q r (ap f p) (ap g p) ≃ q =[p] r :=
+  equiv.MK pathover_eq
+           square_of_pathover
+           (λs, begin cases p, esimp [square_of_pathover,pathover_eq],
+                let H := to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s),
+                esimp at H,
+                rewrite [H] end
+                   )
+           (λs, by cases p;esimp [square_of_pathover,pathover_eq] at *)
+
+
+  -- set_option pp.notation false
+  -- set_option pp.implicit true
+example {f g : A → B} (q : f a = g a) (r : f a = g a) (s : q =[idp] r) :
+  function.compose (to_fun (vdeg_square_equiv q r)) (to_fun (vdeg_square_equiv q r))⁻¹
+    (eq_of_pathover_idp s) = sorry :=
+    begin
+      esimp
+    end
+
+example {f g : A → B} (q : f a = g a) (r : f a = g a) (s : square q r idp idp) :
+  to_fun (vdeg_square_equiv q r) s = eq_of_vdeg_square s :=
+    begin
+
+    end
+
 end eq
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index 9e8148d4a1..0854b974dc 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -7,8 +7,6 @@ Partially ported from Coq HoTT
 Theorems about path types (identity types)
 -/
 
-import .cubical.square
-
 open eq sigma sigma.ops equiv is_equiv equiv.ops
 
 -- TODO: Rename transport_eq_... and pathover_eq_... to eq_transport_... and eq_pathover_...
@@ -112,9 +110,8 @@ namespace eq
 
   -- In the comment we give the fibration of the pathover
 
-  definition pathover_eq {f g : A → B} {p : a1 = a2} {q : f a1 = g a1} {r : f a2 = g a2}
-    (s : square q r (ap f p) (ap g p)) : q =[p] r :=
-  by cases p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s
+  -- we should probably try to do everything just with pathover_eq (defined in cubical.square),
+  -- the following definitions may be removed in future.
 
   definition pathover_eq_l (p : a1 = a2) (q : a1 = a3) : q =[p] p⁻¹ ⬝ q := /-(λx, x = a3)-/
   by cases p; cases q; exact idpo
@@ -232,11 +229,20 @@ namespace eq
   definition eq_equiv_con_eq_con_right (p q : a1 = a2) (r : a2 = a3) : (p = q) ≃ (p ⬝ r = q ⬝ r) :=
   equiv.mk _ !is_equiv_whisker_right
 
+  /-
+    The following proofs can be simplified a bit by concatenating previous equivalences.
+    However, these proofs have the advantage that the inverse is definitionally equal to
+    what we would expect
+  -/
   definition is_equiv_con_eq_of_eq_inv_con (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
     : is_equiv (con_eq_of_eq_inv_con : p = r⁻¹ ⬝ q → r ⬝ p = q) :=
   begin
-   cases r,
-   apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right),
+    fapply adjointify,
+    { apply eq_inv_con_of_con_eq},
+    { intro s, cases r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq],
+        con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]},
+    { intro s, cases r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq],
+        con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
   definition eq_inv_con_equiv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
@@ -246,8 +252,12 @@ namespace eq
   definition is_equiv_con_eq_of_eq_con_inv (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
     : is_equiv (con_eq_of_eq_con_inv : r = q ⬝ p⁻¹ → r ⬝ p = q) :=
   begin
-    cases p,
-    apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right)
+    fapply adjointify,
+    { apply eq_con_inv_of_con_eq},
+    { intro s, cases p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq],
+        con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]},
+    { intro s, cases p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq],
+        con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
   definition eq_con_inv_equiv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
@@ -257,8 +267,12 @@ namespace eq
   definition is_equiv_inv_con_eq_of_eq_con (p : a1 = a3) (q : a2 = a3) (r : a1 = a2)
     : is_equiv (inv_con_eq_of_eq_con : p = r ⬝ q → r⁻¹ ⬝ p = q) :=
   begin
-    cases r,
-    apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right)
+    fapply adjointify,
+    { apply eq_con_of_inv_con_eq},
+    { intro s, cases r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq],
+        con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]},
+    { intro s, cases r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq],
+        con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
   definition eq_con_equiv_inv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a1 = a2)
@@ -268,35 +282,38 @@ namespace eq
   definition is_equiv_con_inv_eq_of_eq_con (p : a3 = a1) (q : a2 = a3) (r : a2 = a1)
     : is_equiv (con_inv_eq_of_eq_con : r = q ⬝ p → r ⬝ p⁻¹ = q) :=
   begin
-    cases p,
-    apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right)
+    fapply adjointify,
+    { apply eq_con_of_con_inv_eq},
+    { intro s, cases p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_eq],
+        con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]},
+    { intro s, cases p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_eq],
+        con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
   definition eq_con_equiv_con_inv_eq (p : a3 = a1) (q : a2 = a3) (r : a2 = a1)
     : (r = q ⬝ p) ≃ (r ⬝ p⁻¹ = q) :=
    equiv.mk _ !is_equiv_con_inv_eq_of_eq_con
 
+  local attribute is_equiv_inv_con_eq_of_eq_con
+                  is_equiv_con_inv_eq_of_eq_con
+                  is_equiv_con_eq_of_eq_con_inv
+                  is_equiv_con_eq_of_eq_inv_con [instance]
+
   definition is_equiv_eq_con_of_inv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
     : is_equiv (eq_con_of_inv_con_eq : r⁻¹ ⬝ q = p → q = r ⬝ p) :=
-  begin
-    cases r,
-    apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right)
-  end
-
-  definition inv_con_eq_equiv_eq_con (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
-    : (r⁻¹ ⬝ q = p) ≃ (q = r ⬝ p) :=
-  equiv.mk _ !is_equiv_eq_con_of_inv_con_eq
+  is_equiv_inv inv_con_eq_of_eq_con
 
   definition is_equiv_eq_con_of_con_inv_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
     : is_equiv (eq_con_of_con_inv_eq : q ⬝ p⁻¹ = r → q = r ⬝ p) :=
-  begin
-    cases p,
-    apply (@is_equiv_compose _ _ _ _ _ !is_equiv_concat_left !is_equiv_concat_right)
-  end
+  is_equiv_inv con_inv_eq_of_eq_con
 
-  definition con_inv_eq_equiv_eq_con (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
-    : (q ⬝ p⁻¹ = r) ≃ (q = r ⬝ p) :=
-  equiv.mk _ !is_equiv_eq_con_of_con_inv_eq
+  definition is_equiv_eq_con_inv_of_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
+    : is_equiv (eq_con_inv_of_con_eq : r ⬝ p = q → r = q ⬝ p⁻¹) :=
+  is_equiv_inv con_eq_of_eq_con_inv
+
+  definition is_equiv_eq_inv_con_of_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1)
+    : is_equiv (eq_inv_con_of_con_eq : r ⬝ p = q → p = r⁻¹ ⬝ q) :=
+  is_equiv_inv con_eq_of_eq_inv_con
 
   /- Pathover Equivalences -/
 
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index a0acd0d45b..18484931f3 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -27,7 +27,7 @@ namespace is_equiv
            ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p       : by rewrite ap_inv
            ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p            : by rewrite ap_con)))
 
-  definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
+  definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) :=
   begin
     fapply is_trunc_equiv_closed,
       {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy},
@@ -37,8 +37,8 @@ namespace is_equiv
     apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))),
   end
 
-  definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ∼ id)
-    : is_contr (Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
+  definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ~ id)
+    : is_contr (Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
   begin
     fapply is_trunc_equiv_closed,
       {apply equiv.symm, apply sigma_pi_equiv_pi_sigma},
@@ -50,7 +50,7 @@ namespace is_equiv
   omit H
 
   protected definition sigma_char : (is_equiv f) ≃
-  (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) :=
+  (Σ(g : B → A) (ε : f ∘ g ~ id) (η : g ∘ f ~ id), Π(a : A), ε (f a) = ap f (η a)) :=
   equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩)
            (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2)
            (λp, begin
@@ -62,13 +62,13 @@ namespace is_equiv
            (λH, is_equiv.rec_on H (λH1 H2 H3 H4, idp))
 
   protected definition sigma_char' : (is_equiv f) ≃
-  (Σ(u : Σ(g : B → A), f ∘ g ∼ id), Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
+  (Σ(u : Σ(g : B → A), f ∘ g ~ id), Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
   calc
     (is_equiv f) ≃
-      (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a))
+      (Σ(g : B → A) (ε : f ∘ g ~ id) (η : g ∘ f ~ id), Π(a : A), ε (f a) = ap f (η a))
           : is_equiv.sigma_char
-    ... ≃ (Σ(u : Σ(g : B → A), f ∘ g ∼ id), Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a))
-          : {sigma_assoc_equiv (λu, Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a))}
+    ... ≃ (Σ(u : Σ(g : B → A), f ∘ g ~ id), Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a))
+          : {sigma_assoc_equiv (λu, Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a))}
 
   local attribute is_contr_right_inverse [instance] [priority 1600]
   local attribute is_contr_right_coherence [instance] [priority 1600]
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index ef5af3e030..2026cd0dda 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -18,13 +18,13 @@ namespace pi
 
   /- Paths -/
 
-  /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g].
+  /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g].
 
   This equivalence, however, is just the combination of [apd10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path:  -/
 
   /- Now we show how these things compute. -/
 
-  definition apd10_eq_of_homotopy (h : f ∼ g) : apd10 (eq_of_homotopy h) ∼ h :=
+  definition apd10_eq_of_homotopy (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h :=
   apd10 (right_inv apd10 h)
 
   definition eq_of_homotopy_eta (p : f = g) : eq_of_homotopy (apd10 p) = p :=
@@ -35,14 +35,14 @@ namespace pi
 
   /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
 
-  definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ∼ g) :=
+  definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ~ g) :=
   equiv.mk _ !is_equiv_apd
 
   definition is_equiv_eq_of_homotopy [instance] (f g : Πx, B x)
       : is_equiv (@eq_of_homotopy _ _ f g) :=
   is_equiv_inv apd10
 
-  definition homotopy_equiv_eq (f g : Πx, B x) : (f ∼ g) ≃ (f = g) :=
+  definition homotopy_equiv_eq (f g : Πx, B x) : (f ~ g) ≃ (f = g) :=
   equiv.mk _ !is_equiv_eq_of_homotopy
 
 
@@ -50,7 +50,7 @@ namespace pi
 
   definition pi_transport (p : a = a') (f : Π(b : B a), C a b)
     : (transport (λa, Π(b : B a), C a b) p f)
-      ∼ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▸ b)))) :=
+      ~ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▸ b)))) :=
   eq.rec_on p (λx, idp)
 
   /- A special case of [transport_pi] where the type [B] does not depend on [A],
@@ -149,7 +149,7 @@ namespace pi
 
   definition pi_functor : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
 
-  definition ap_pi_functor {g g' : Π(a:A), B a} (h : g ∼ g')
+  definition ap_pi_functor {g g' : Π(a:A), B a} (h : g ~ g')
       : ap (pi_functor f0 f1) (eq_of_homotopy h) = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) :=
   begin
   apply (equiv_rect (@apd10 A B g g')), intro p, clear h,
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 3e22dedfb6..fd19ff9a39 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -91,55 +91,83 @@ namespace pointed
 end pointed
 
 open pointed
-structure pointed_map (A B : Pointed) :=
-  (map : A → B) (respect_pt : map (Point A) = Point B)
+structure pmap (A B : Pointed) :=
+  (map : A → B)
+  (resp_pt : map (Point A) = Point B)
 
-open pointed_map
+open pmap
 
 namespace pointed
 
-  abbreviation respect_pt := @pointed_map.respect_pt
+  variables {A B C D : Pointed}
 
-  -- definition transport_to_sigma {A B : Pointed}
-  --   {P : Π(X : Type) (m : X → A → B), (Π(f : X), m f (Point A) = Point B) → (Π(m : A → B), m (Point A) = Point B → X) →  Type}
-  --   (H : P (Σ(f : A → B), f (Point A) = Point B) pr1 pr2 sigma.mk) :
-  --   P (pointed_map A B) map respect_pt pointed_map.mk :=
-  -- sorry
+  abbreviation respect_pt [unfold-c 3] := @pmap.resp_pt
 
-
-  notation `map₊` := pointed_map
-  attribute pointed_map.map [coercion]
-  definition pointed_map_eq {A B : Pointed} {f g : map₊ A B}
+  notation `map₊` := pmap
+  infix `→*`:30 := pmap
+  attribute pmap.map [coercion]
+  definition pmap_eq {f g : map₊ A B}
     (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
   begin
     cases f with f p, cases g with g q,
     esimp at *,
-    fapply apo011 pointed_map.mk,
+    fapply apo011 pmap.mk,
     { exact eq_of_homotopy r},
     { apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con,
-      rewrite [ap_eq_ap10,↑ap10,apd10_eq_of_homotopy,↑respect_pt at *,s]}
+      rewrite [ap_eq_ap10,↑ap10,apd10_eq_of_homotopy,s]}
   end
 
-  definition pointed_map_equiv_left (A : Type) (B : Pointed) : map₊ A₊ B ≃ (A → B) :=
+  definition pid [constructor] (A : Pointed) : A →* A :=
+  pmap.mk function.id idp
+
+  definition pcompose [constructor] (g : B →* C) (f : A →* B) : A →* C :=
+  pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g)
+
+  infixr `∘*`:60 := pcompose
+
+  structure phomotopy (f g : A →* B) :=
+    (homotopy : f ~ g)
+    (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
+
+  infix `~*`:50 := phomotopy
+  abbreviation to_homotopy_pt [unfold-c 5] := @phomotopy.homotopy_pt
+  abbreviation to_homotopy [coercion] [unfold-c 5] {f g : A →* B} (p : f ~* g) : Πa, f a = g a :=
+  phomotopy.homotopy p
+
+  definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) :=
+  begin
+    fapply phomotopy.mk, intro a, reflexivity,
+    cases A, cases B, cases C, cases D, cases f with f pf, cases g with g pg, cases h with h ph,
+    esimp at *,
+    induction pf, induction pg, induction ph, reflexivity
+  end
+
+  definition pmap_equiv_left (A : Type) (B : Pointed) : A₊ →* B ≃ (A → B) :=
   begin
     fapply equiv.MK,
     { intro f a, cases f with f p, exact f (some a)},
-    { intro f, fapply pointed_map.mk,
+    { intro f, fapply pmap.mk,
         intro a, cases a, exact pt, exact f a,
         reflexivity},
     { intro f, reflexivity},
-    { intro f, cases f with f p, esimp, fapply pointed_map_eq,
+    { intro f, cases f with f p, esimp, fapply pmap_eq,
       { intro a, cases a; all_goals (esimp at *), exact p⁻¹},
       { esimp, exact !con.left_inv⁻¹}},
   end
 
+  -- definition Loop_space_functor (f : A →* B) : Ω A →* Ω B :=
+  -- begin
+  --   fapply pmap.mk,
+  --   { intro p, exact ap f p},
+  -- end
+
   -- set_option pp.notation false
-  -- definition pointed_map_equiv_right (A : Pointed) (B : Type)
+  -- definition pmap_equiv_right (A : Pointed) (B : Type)
   --   : (Σ(b : B), map₊ A (pointed.Mk b)) ≃ (A → B) :=
   -- begin
   --   fapply equiv.MK,
   --   { intro u a, cases u with b f, cases f with f p, esimp at f, exact f a},
-  --   { intro f, refine ⟨f pt, _⟩, fapply pointed_map.mk,
+  --   { intro f, refine ⟨f pt, _⟩, fapply pmap.mk,
   --       intro a, esimp, exact f a,
   --       reflexivity},
   --   { intro f, reflexivity},
@@ -148,34 +176,66 @@ namespace pointed
   --     }
   -- end
 
-  definition pointed_map_bool_equiv (B : Pointed) : map₊ Bool B ≃ B :=
+  definition pmap_bool_equiv (B : Pointed) : map₊ Bool B ≃ B :=
   begin
     fapply equiv.MK,
     { intro f, cases f with f p, exact f tt},
-    { intro b, fapply pointed_map.mk,
+    { intro b, fapply pmap.mk,
         intro u, cases u, exact pt, exact b,
         reflexivity},
     { intro b, reflexivity},
-    { intro f, cases f with f p, esimp, fapply pointed_map_eq,
+    { intro f, cases f with f p, esimp, fapply pmap_eq,
       { intro a, cases a; all_goals (esimp at *), exact p⁻¹},
       { esimp, exact !con.left_inv⁻¹}},
   end
-  -- calc
-  --   map₊ (Pointed.mk' bool) B ≃ map₊ unit₊ B : sorry
-  --     ... ≃ (unit → B) : pointed_map_equiv
-  --     ... ≃ B : unit_imp_equiv
 
-  definition apn {A B : Pointed} {n : ℕ} (f : map₊ A B) (p : Ω[n] A) : Ω[n] B :=
+  definition apn [constructor] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B :=
   begin
-  revert A B f p, induction n with n IH,
-  { intros A B f p, exact f p},
-  { intros A B f p, rewrite [↑Iterated_loop_space at p,↓Iterated_loop_space n (Ω A) at p,
+  revert A B f, induction n with n IH,
+  { intros A B f, exact f},
+  { intros A B f, rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Ω A),
       ↑Iterated_loop_space, ↓Iterated_loop_space n (Ω B)],
     apply IH (Ω A),
-    { esimp, fapply pointed_map.mk,
+    { esimp, fapply pmap.mk,
         intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
-        esimp, apply con.left_inv},
-    { exact p}}
+        esimp, apply con.left_inv}}
   end
 
+  definition ap1 [constructor] (f : A →* B) := apn (succ 0) f
+
+  protected definition phomotopy.trans [trans] {f g h : A →* B} (p : f ~* g) (q : g ~* h)
+    : f ~* h :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, exact p a ⬝ q a},
+    { induction f, induction g, induction p with p p', induction q with q q', esimp at *,
+      induction p', induction q', esimp, apply con.assoc}
+  end
+
+  protected definition phomotopy.symm [symm] {f g : A →* B} (p : f ~* g) : g ~* f :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, exact (p a)⁻¹},
+    { induction f, induction p with p p', esimp at *,
+      induction p', esimp, apply inv_con_cancel_left}
+  end
+
+  definition eq_of_phomotopy {f g : A →* B} (p : f ~* g) : f = g :=
+  begin
+    fapply pmap_eq,
+    { intro a, exact p a},
+    { exact !to_homotopy_pt⁻¹}
+  end
+
+  structure pequiv (A B : Pointed) :=
+    (to_pmap : A →* B)
+    (is_equiv_to_pmap : is_equiv to_pmap)
+
+  infix `≃*`:25 := pequiv
+  attribute pequiv.to_pmap [coercion]
+  attribute pequiv.is_equiv_to_pmap [instance]
+
+  definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B :=
+  equiv.mk f _
+
 end pointed
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 021a4cffc4..e621112655 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -150,9 +150,6 @@ namespace is_trunc
     is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) :=
   iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn)
 
---  set_option pp.implicit true
-  -- set_option pp.coercions true
-  -- set_option pp.notation false
   definition is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type)
     : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](Pointed.mk a)) :=
   begin
diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean
index 1154e51a24..190b442744 100644
--- a/library/data/list/perm.lean
+++ b/library/data/list/perm.lean
@@ -17,7 +17,7 @@ inductive perm : list A → list A → Prop :=
 | trans : Π {l₁ l₂ l₃ : list A}, perm l₁ l₂ → perm l₂ l₃ → perm l₁ l₃
 
 namespace perm
-infix ~:50 := perm
+infix ~ := perm
 theorem eq_nil_of_perm_nil {l₁ : list A} (p : [] ~ l₁) : l₁ = [] :=
 have gen : ∀ (l₂ : list A) (p : l₂ ~ l₁), l₂ = [] → l₁ = [], from
   take l₂ p, perm.induction_on p
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 13d723de33..440b52299d 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -22,7 +22,8 @@ notation `ℕ+` := pnat
 
 definition nat_of_pnat (p : pnat) : ℕ :=
   pnat.rec_on p (λ n H, n)
-local postfix `~` : std.prec.max_plus := nat_of_pnat
+reserve postfix `~`:std.prec.max_plus
+local postfix ~ := nat_of_pnat
 
 theorem nat_of_pnat_pos (p : pnat) : p~ > 0 :=
   pnat.rec_on p (λ n H, H)
diff --git a/library/init/quot.lean b/library/init/quot.lean
index 49ec6fde65..1e3b93c6bf 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -123,7 +123,7 @@ namespace quot
         (λ a₁a₂, setoid.trans (setoid.symm a₁b₁) (setoid.trans a₁a₂ a₂b₂))
         (λ b₁b₂, setoid.trans a₁b₁ (setoid.trans b₁b₂ (setoid.symm a₂b₂)))))
 
-  local infix `~`:50 := rel
+  local infix `~` := rel
 
   private lemma rel.refl : ∀ q : quot s, q ~ q :=
   λ q, quot.induction_on q (λ a, setoid.refl a)
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 8a25aa453c..cbe19222ae 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -43,7 +43,7 @@ reserve infix `↔`:20
 reserve infix `=`:50
 reserve infix `≠`:50
 reserve infix `≈`:50
-reserve infix `∼`:50
+reserve infix `~`:50
 reserve infix `≡`:50
 
 reserve infixr `∘`:60                   -- input with \comp