diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index c35485594..b4f2e2b7b 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -13,21 +13,17 @@ open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv
 -- TODO: consistently make n an argument before A
 namespace eq
 
-  definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* :=
+  definition homotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* :=
   ptrunc 0 (Ω[n] A)
 
-  definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type :=
-  phomotopy_group n A
-
-  notation `π*[`:95 n:0 `]`:0 := phomotopy_group n
-  notation `π[`:95  n:0 `]`:0 :=  homotopy_group n
+  notation `π[`:95  n:0 `]`:0 := homotopy_group n
 
   definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*)
     : group (π[succ n] A) :=
   trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv
 
   definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) :
-    group (carrier (ptrunctype.to_pType (π*[k + 1] A))) :=
+    group (carrier (ptrunctype.to_pType (π[k + 1] A))) :=
   group_homotopy_group k A
 
   definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*)
@@ -58,30 +54,30 @@ namespace eq
     : tr p *[π[succ n] A] tr q = tr (p ⬝ q) :=
   idp
 
-  definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
-    : π*[n] A ≃* π*[n] B :=
+  definition homotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
+    : π[n] A ≃* π[n] B :=
   ptrunc_pequiv_ptrunc 0 (loopn_pequiv_loopn n H)
 
-  definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) :
-    π*[k] A ≃* Ω[k] (ptrunc k A) :=
+  definition homotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) :
+    π[k] A ≃* Ω[k] (ptrunc k A) :=
   begin
-    refine !iterated_loop_ptrunc_pequiv⁻¹ᵉ* ⬝e* _,
+    refine !loopn_ptrunc_pequiv⁻¹ᵉ* ⬝e* _,
     exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end)
   end
 
   open trunc_index
-  definition phomotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) :
-    π*[k] (ptrunc n A) ≃* π*[k] A :=
+  definition homotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) :
+    π[k] (ptrunc n A) ≃* π[k] A :=
   calc
-    π*[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A))
-             : phomotopy_group_pequiv_loop_ptrunc k (ptrunc n A)
+    π[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A))
+             : homotopy_group_pequiv_loop_ptrunc k (ptrunc n A)
       ... ≃* Ω[k] (ptrunc k A)
              : loopn_pequiv_loopn k (ptrunc_ptrunc_pequiv_left A (of_nat_le_of_nat H))
-      ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+      ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
 
-  definition phomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
-    π*[k] (ptrunc k A) ≃* π*[k] A :=
-  phomotopy_group_ptrunc_of_le (le.refl k) A
+  definition homotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
+    π[k] (ptrunc k A) ≃* π[k] A :=
+  homotopy_group_ptrunc_of_le (le.refl k) A
 
   theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 :=
   begin
@@ -91,67 +87,63 @@ namespace eq
     apply is_trunc_succ_succ_of_is_set
   end
 
-  definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp
+  definition homotopy_group_succ_out (A : Type*) (n : ℕ) : π[n + 1] A = π₁ (Ω[n] A) := idp
 
-  definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A ≃* π*[n] (Ω A) :=
-  ptrunc_pequiv_ptrunc 0 (loop_space_succ_in A n)
+  definition homotopy_group_succ_in (A : Type*) (n : ℕ) : π[n + 1] A ≃* π[n] (Ω A) :=
+  ptrunc_pequiv_ptrunc 0 (loopn_succ_in A n)
 
-  definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp
+  definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ (Ω[n] A) := idp
 
-  definition phomotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) :
-    phomotopy_group_succ_in A (succ n) (g * h) =
-    phomotopy_group_succ_in A (succ n) g * phomotopy_group_succ_in A (succ n) h :=
+  definition homotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) :
+    homotopy_group_succ_in A (succ n) (g * h) =
+    homotopy_group_succ_in A (succ n) g * homotopy_group_succ_in A (succ n) h :=
   begin
     induction g with p, induction h with q, esimp,
-    apply ap tr, apply loop_space_succ_in_con
+    apply ap tr, apply loopn_succ_in_con
   end
 
   definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] (Ω A) :=
   begin
     fapply isomorphism_of_equiv,
-    { exact phomotopy_group_succ_in A (succ n)},
-    { exact phomotopy_group_succ_in_con},
+    { exact homotopy_group_succ_in A (succ n)},
+    { exact homotopy_group_succ_in_con},
   end
 
-  definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
-    : π*[n] A →* π*[n] B :=
+  definition homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    : π[n] A →* π[n] B :=
   ptrunc_functor 0 (apn n f)
 
-  definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B :=
-  phomotopy_group_functor n f
+  notation `π→[`:95  n:0 `]`:0 := homotopy_group_functor n
 
-  notation `π→*[`:95 n:0 `]`:0 := phomotopy_group_functor n
-  notation `π→[`:95  n:0 `]`:0 :=  homotopy_group_functor n
-
-  definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B}
-    (p : f ~* g) : π→*[n] f ~* π→*[n] g :=
+  definition homotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B}
+    (p : f ~* g) : π→[n] f ~* π→[n] g :=
   ptrunc_functor_phomotopy 0 (apn_phomotopy n p)
 
-  definition phomotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
-    (f : A →* B) : π→*[n] (g ∘* f) ~* π→*[n] g ∘* π→*[n] f :=
-  ptrunc_functor_phomotopy 0 !apn_compose ⬝* !ptrunc_functor_pcompose
+  definition homotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
+    (f : A →* B) : π→[n] (g ∘* f) ~* π→[n] g ∘* π→[n] f :=
+  ptrunc_functor_phomotopy 0 !apn_pcompose ⬝* !ptrunc_functor_pcompose
 
   definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
     [is_equiv f] : is_equiv (π→[n] f) :=
   @(is_equiv_trunc_functor 0 _) !is_equiv_apn
 
-  definition phomotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) :
-    phomotopy_group_succ_in B n ∘* π→*[n + 1] f ~*
-    π→*[n] (Ω→ f) ∘* phomotopy_group_succ_in A n :=
+  definition homotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) :
+    homotopy_group_succ_in B n ∘* π→[n + 1] f ~*
+    π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n :=
   begin
     refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose,
     exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f)
   end
 
-  definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
-    [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) :=
-  have is_equiv (phomotopy_group_succ_in B n ∘* π→*[n + 1] f),
-  from is_equiv_compose _ (π→*[n + 1] f),
-  have is_equiv (π→*[n] (Ω→ f) ∘ phomotopy_group_succ_in A n),
-  from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f),
-  is_equiv.cancel_right (phomotopy_group_succ_in A n) _
+  definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
+    [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) :=
+  have is_equiv (homotopy_group_succ_in B n ∘* π→[n + 1] f),
+  from is_equiv_compose _ (π→[n + 1] f),
+  have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n),
+  from is_equiv.homotopy_closed _ (homotopy_group_functor_succ_phomotopy_in n f),
+  is_equiv.cancel_right (homotopy_group_succ_in A n) _
 
-  definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
+  definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X :=
   ptrunc_functor 0 pinverse
 
   definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) :=
@@ -165,7 +157,7 @@ namespace eq
     { reflexivity}
   end
 
-  definition phomotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B)
+  definition homotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B)
     (p q : πg[n+1] A) :
     (π→[n + 1] g) (p *[πg[n+1] A] q) = (π→[n + 1] g) p *[πg[n+1] B] (π→[n + 1] g) q :=
   begin
@@ -179,8 +171,8 @@ namespace eq
     : πg[n+1] A →g πg[n+1] B :=
   begin
     fconstructor,
-    { exact phomotopy_group_functor (n+1) f},
-    { apply phomotopy_group_functor_mul}
+    { exact homotopy_group_functor (n+1) f},
+    { apply homotopy_group_functor_mul}
   end
 
   definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B)
@@ -190,63 +182,63 @@ namespace eq
     esimp, apply is_equiv_trunc_functor, apply is_equiv_apn,
   end
 
-  definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] Ω[m] A :=
+  definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] (Ω[m] A) :=
   begin
     revert A, induction m with m IH: intro A,
     { reflexivity},
-    { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _,
+    { esimp [loopn, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _,
       apply homotopy_group_isomorphism_of_pequiv,
-      exact !loop_space_succ_in⁻¹ᵉ*}
+      exact !loopn_succ_in⁻¹ᵉ*}
   end
 
-  theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ)
+  theorem trivial_homotopy_add_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ)
     (H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 :=
   !homotopy_group_add ⬝g !trivial_homotopy_of_is_set
 
-  theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
+  theorem trivial_homotopy_le_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
     (H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 :=
   obtain (k : ℕ) (p : n + k = m), from le.elim H1,
   isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g
-  trivial_homotopy_add_of_is_set_loop_space k H2
+  trivial_homotopy_add_of_is_set_loopn k H2
 
-  definition phomotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) :
-    phomotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) =
-    phomotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝
-    phomotopy_group_pequiv_loop_ptrunc (succ k) A q :=
+  definition homotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) :
+    homotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) =
+    homotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝
+    homotopy_group_pequiv_loop_ptrunc (succ k) A q :=
   begin
     refine _ ⬝ !loopn_pequiv_loopn_con,
-    exact ap (loopn_pequiv_loopn _ _) !iterated_loop_ptrunc_pequiv_inv_con
+    exact ap (loopn_pequiv_loopn _ _) !loopn_ptrunc_pequiv_inv_con
   end
 
-  definition phomotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*}
+  definition homotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*}
     (p q : Ω[succ k] (ptrunc (succ k) A)) :
-    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) =
-    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p *
-    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q :=
-  inv_preserve_binary (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat
-    (@phomotopy_group_pequiv_loop_ptrunc_con k A) p q
+    (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) =
+    (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p *
+    (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q :=
+  inv_preserve_binary (homotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat
+    (@homotopy_group_pequiv_loop_ptrunc_con k A) p q
 
   definition ghomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
     πg[k+1] (ptrunc (k+1) A) ≃g πg[k+1] A :=
   begin
     fapply isomorphism_of_equiv,
-    { exact phomotopy_group_ptrunc (k+1) A},
+    { exact homotopy_group_ptrunc (k+1) A},
     { intro g₁ g₂, esimp,
-      refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con,
-      apply ap ((phomotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*),
+      refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con,
+      apply ap ((homotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*),
       refine _ ⬝ !loopn_pequiv_loopn_con ,
       apply ap (loopn_pequiv_loopn (k+1) _),
-      apply phomotopy_group_pequiv_loop_ptrunc_con}
+      apply homotopy_group_pequiv_loop_ptrunc_con}
   end
 
   /- some homomorphisms -/
 
-  -- definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) :
-  --   is_homomorphism (loop_space_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) :=
+  -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) :
+  --   is_homomorphism (loopn_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) :=
   -- begin
   --   intro g h, induction g with g, induction h with h,
   --   xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose,
-  --             loop_space_succ_eq_in_concat, - + tr_compose],
+  --             loopn_succ_eq_in_concat, - + tr_compose],
   -- end
 
   definition is_homomorphism_inverse (A : Type*) (n : ℕ)
diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean
index 638f96f16..d17c0a906 100644
--- a/hott/homotopy/EM.hlean
+++ b/hott/homotopy/EM.hlean
@@ -220,7 +220,7 @@ namespace EM
   end ops
   open ops
 
-  definition phomotopy_group_EM (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G :=
+  definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* pType_of_Group G :=
   begin
     cases n with n,
     { rexact ptrunc_pequiv 0 (pType_of_Group G) _},
@@ -318,7 +318,7 @@ namespace EM
   (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl
 
   open circle int
-  definition EM_pequiv_circle : K agℤ 1 ≃* S¹. :=
+  definition EM_pequiv_circle : K agℤ 1 ≃* S¹* :=
   !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle
 
   /- loops of EM-spaces -/
diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean
index 001855606..ad186b6ac 100644
--- a/hott/homotopy/LES_of_homotopy_groups.hlean
+++ b/hott/homotopy/LES_of_homotopy_groups.hlean
@@ -264,26 +264,26 @@ namespace chain_complex
 
   /- Now we are ready to define the long exact sequence of homotopy groups.
      First we define its carrier -/
-  definition loop_spaces : ℕ → Type*
+  definition loopns : ℕ → Type*
   | 0     := Y
   | 1     := X
   | 2     := pfiber f
-  | (k+3) := Ω (loop_spaces k)
+  | (k+3) := Ω (loopns k)
 
   /- The maps between the homotopy groups -/
-  definition loop_spaces_fun
-    : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n
+  definition loopns_fun
+    : Π(n : ℕ), loopns (n+1) →* loopns n
   | 0     := proof f qed
   | 1     := proof ppoint f qed
   | 2     := proof boundary_map qed
-  | (k+3) := proof ap1 (loop_spaces_fun k) qed
+  | (k+3) := proof ap1 (loopns_fun k) qed
 
-  definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) :
-    loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) :=
+  definition loopns_fun_add3 [unfold_full] (n : ℕ) :
+    loopns_fun (n + 3) = ap1 (loopns_fun n) :=
   proof idp qed
 
-  definition fiber_sequence_pequiv_loop_spaces :
-    Πn, fiber_sequence_carrier n ≃* loop_spaces n
+  definition fiber_sequence_pequiv_loopns :
+    Πn, fiber_sequence_carrier n ≃* loopns n
   | 0     := by reflexivity
   | 1     := by reflexivity
   | 2     := by reflexivity
@@ -291,22 +291,22 @@ namespace chain_complex
     begin
       refine fiber_sequence_carrier_pequiv k ⬝e* _,
       apply loop_pequiv_loop,
-      exact fiber_sequence_pequiv_loop_spaces k
+      exact fiber_sequence_pequiv_loopns k
     end
 
-  definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ)
-    : fiber_sequence_pequiv_loop_spaces (n + 3) =
-      ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n :=
+  definition fiber_sequence_pequiv_loopns_add3 (n : ℕ)
+    : fiber_sequence_pequiv_loopns (n + 3) =
+      ap1 (fiber_sequence_pequiv_loopns n) ∘* fiber_sequence_carrier_pequiv n :=
   by reflexivity
 
-  definition fiber_sequence_pequiv_loop_spaces_3_phomotopy
-    : fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed :=
+  definition fiber_sequence_pequiv_loopns_3_phomotopy
+    : fiber_sequence_pequiv_loopns 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed :=
   begin
-    refine pwhisker_right _ ap1_id ⬝* _,
-    apply pid_comp
+    refine pwhisker_right _ ap1_pid ⬝* _,
+    apply pid_pcompose
   end
 
-  definition pid_or_pinverse : Π(n : ℕ), loop_spaces n ≃* loop_spaces n
+  definition pid_or_pinverse : Π(n : ℕ), loopns n ≃* loopns n
   | 0     := pequiv.rfl
   | 1     := pequiv.rfl
   | 2     := pequiv.rfl
@@ -321,69 +321,69 @@ namespace chain_complex
     pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1))
   | 0     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
                    replace pid_or_pinverse (0 + 1) with pequiv.refl X,
-                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
-                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _,
+                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
   | 1     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
                    replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f),
-                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
-                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _,
+                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
   | 2     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
                    replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y),
-                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
-                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _,
+                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
   | (k+3) :=
     begin
       replace (k + 3 + 1) with (k + 4),
       rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans],
-      refine _ ⬝* pwhisker_left _ !ap1_compose⁻¹*,
+      refine _ ⬝* pwhisker_left _ !ap1_pcompose⁻¹*,
       refine _ ⬝* !passoc,
       apply pconcat2,
       { refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _,
-        refine !ap1_compose ⬝* _, apply pwhisker_right, apply ap1_pinverse},
+        refine !ap1_pcompose ⬝* _, apply pwhisker_right, apply ap1_pinverse},
       { refine !ap1_pinverse⁻¹*}
     end
 
-  theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ),
-    fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~*
-      (loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loop_spaces (n + 1)
-  | 0     := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !comp_pid⁻¹* qed
+  theorem fiber_sequence_phomotopy_loopns : Π(n : ℕ),
+    fiber_sequence_pequiv_loopns n ∘* fiber_sequence_fun n ~*
+      (loopns_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loopns (n + 1)
+  | 0     := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !pcompose_pid⁻¹* qed
   | 1     := by reflexivity
   | 2     :=
     begin
-      refine !pid_comp ⬝* _,
-      replace loop_spaces_fun 2 with boundary_map,
-      refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*,
+      refine !pid_pcompose ⬝* _,
+      replace loopns_fun 2 with boundary_map,
+      refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loopns_3_phomotopy⁻¹*,
       apply phomotopy_of_pinv_right_phomotopy,
-      exact !pid_comp⁻¹*
+      exact !pid_pcompose⁻¹*
     end
   | (k+3) :=
     begin
       replace (k + 3 + 1) with (k + 1 + 3),
-      rewrite [fiber_sequence_pequiv_loop_spaces_add3 k,
-               fiber_sequence_pequiv_loop_spaces_add3 (k+1)],
+      rewrite [fiber_sequence_pequiv_loopns_add3 k,
+               fiber_sequence_pequiv_loopns_add3 (k+1)],
       refine !passoc ⬝* _,
       refine pwhisker_left _ (fiber_sequence_fun_phomotopy k) ⬝* _,
       refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
       apply pwhisker_right,
       replace (k + 1 + 3) with (k + 4),
-      xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans],
+      xrewrite [loopns_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans],
       refine _ ⬝* !passoc⁻¹*,
       refine _ ⬝* pwhisker_left _ !passoc⁻¹*,
-      refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_compose_pinverse),
+      refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_pcompose_pinverse),
       refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc,
       apply pwhisker_right,
-      refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose ⬝* pwhisker_right _ !ap1_compose,
+      refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose ⬝* pwhisker_right _ !ap1_pcompose,
       apply ap1_phomotopy,
-      exact fiber_sequence_phomotopy_loop_spaces k
+      exact fiber_sequence_phomotopy_loopns k
     end
 
-  definition pid_or_pinverse_right : Π(n : ℕ), loop_spaces n →* loop_spaces n
+  definition pid_or_pinverse_right : Π(n : ℕ), loopns n →* loopns n
   | 0     := !pid
   | 1     := !pid
   | 2     := !pid
   | (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse
 
-  definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n
+  definition pid_or_pinverse_left : Π(n : ℕ), loopns n →* loopns n
   | 0     := pequiv.rfl
   | 1     := pequiv.rfl
   | 2     := pequiv.rfl
@@ -400,63 +400,63 @@ namespace chain_complex
   by reflexivity
 
   theorem pid_or_pinverse_commute_right : Π(n : ℕ),
-    loop_spaces_fun n ~* pid_or_pinverse_right n ∘* loop_spaces_fun n ∘* pid_or_pinverse (n + 1)
-  | 0     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
-  | 1     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
-  | 2     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
+    loopns_fun n ~* pid_or_pinverse_right n ∘* loopns_fun n ∘* pid_or_pinverse (n + 1)
+  | 0     := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed
+  | 1     := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed
+  | 2     := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed
   | (k+3) :=
     begin
       replace (k + 3 + 1) with (k + 4),
-      rewrite [pid_or_pinverse_right_add3, loop_spaces_fun_add3],
+      rewrite [pid_or_pinverse_right_add3, loopns_fun_add3],
       refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pid_or_pinverse_add4_rev⁻¹*),
       refine ap1_phomotopy (pid_or_pinverse_commute_right k) ⬝* _,
-      refine !ap1_compose ⬝* _ ⬝* !passoc⁻¹*,
+      refine !ap1_pcompose ⬝* _ ⬝* !passoc⁻¹*,
       apply pwhisker_left,
-      refine !ap1_compose ⬝* _ ⬝* !passoc ⬝* !passoc,
+      refine !ap1_pcompose ⬝* _ ⬝* !passoc ⬝* !passoc,
       apply pwhisker_right,
-      refine _ ⬝* pwhisker_right _ !ap1_compose_pinverse,
+      refine _ ⬝* pwhisker_right _ !ap1_pcompose_pinverse,
       refine _ ⬝* !passoc⁻¹*,
-      refine !comp_pid⁻¹* ⬝* pwhisker_left _ _,
+      refine !pcompose_pid⁻¹* ⬝* pwhisker_left _ _,
       symmetry, apply pinverse_pinverse
     end
 
   theorem pid_or_pinverse_commute_left : Π(n : ℕ),
-    loop_spaces_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loop_spaces_fun n
-  | 0     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
-  | 1     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
-  | 2     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
-  | 3     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
+    loopns_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loopns_fun n
+  | 0     := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed
+  | 1     := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed
+  | 2     := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed
+  | 3     := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed
   | (k+4) :=
     begin
       replace (k + 4 + 1) with (k + 5),
       rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans],
       replace (k + 4) with (k + 1 + 3),
-      rewrite [loop_spaces_fun_add3],
+      rewrite [loopns_fun_add3],
       refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*,
-      refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse,
+      refine _ ⬝* pwhisker_left _ !ap1_pcompose_pinverse,
       refine _ ⬝* !passoc,
       apply pwhisker_right,
-      refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose,
+      refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose,
       exact ap1_phomotopy (pid_or_pinverse_commute_left (k+1))
     end
 
-  definition LES_of_loop_spaces' [constructor] : type_chain_complex +ℕ :=
+  definition LES_of_loopns' [constructor] : type_chain_complex +ℕ :=
   transfer_type_chain_complex
     fiber_sequence
-    (λn, loop_spaces_fun n ∘* pid_or_pinverse (n + 1))
-    fiber_sequence_pequiv_loop_spaces
-    fiber_sequence_phomotopy_loop_spaces
+    (λn, loopns_fun n ∘* pid_or_pinverse (n + 1))
+    fiber_sequence_pequiv_loopns
+    fiber_sequence_phomotopy_loopns
 
-  definition LES_of_loop_spaces [constructor] : type_chain_complex +ℕ :=
+  definition LES_of_loopns [constructor] : type_chain_complex +ℕ :=
   type_chain_complex_cancel_aut
-    LES_of_loop_spaces'
-    loop_spaces_fun
+    LES_of_loopns'
+    loopns_fun
     pid_or_pinverse
     pid_or_pinverse_right
     (λn x, idp)
     pid_or_pinverse_commute_right
 
-  definition is_exact_LES_of_loop_spaces : is_exact_t LES_of_loop_spaces :=
+  definition is_exact_LES_of_loopns : is_exact_t LES_of_loopns :=
   begin
     intro n,
     refine is_exact_at_t_cancel_aut n pid_or_pinverse_left _ _ pid_or_pinverse_commute_left _,
@@ -470,38 +470,38 @@ namespace chain_complex
       PART 3
    --------------/
 
-  definition loop_spaces2 [reducible] : +3ℕ → Type*
+  definition loopns2 [reducible] : +3ℕ → Type*
   | (n, fin.mk 0 H) := Ω[n] Y
   | (n, fin.mk 1 H) := Ω[n] X
   | (n, fin.mk k H) := Ω[n] (pfiber f)
 
-  definition loop_spaces2_add1 (n : ℕ) : Π(x : fin 3),
-    loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x))
+  definition loopns2_add1 (n : ℕ) : Π(x : fin 3),
+    loopns2 (n+1, x) = Ω (loopns2 (n, x))
   | (fin.mk 0 H) := by reflexivity
   | (fin.mk 1 H) := by reflexivity
   | (fin.mk 2 H) := by reflexivity
   | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
-  definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n
+  definition loopns_fun2 : Π(n : +3ℕ), loopns2 (S n) →* loopns2 n
   | (n, fin.mk 0 H) := proof Ω→[n] f qed
   | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed
-  | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loop_space_succ_in Y n qed
+  | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in Y n qed
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
-  definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
-    : loop_spaces_fun2 (n+1, fin.mk 0 H) ~*
-      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 0 H)) :=
+  definition loopns_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
+    : loopns_fun2 (n+1, fin.mk 0 H) ~*
+      cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 0 H)) :=
   by reflexivity
 
-  definition loop_spaces_fun2_add1_1 (n : ℕ) (H : 1 < succ 2)
-    : loop_spaces_fun2 (n+1, fin.mk 1 H) ~*
-      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 1 H)) :=
+  definition loopns_fun2_add1_1 (n : ℕ) (H : 1 < succ 2)
+    : loopns_fun2 (n+1, fin.mk 1 H) ~*
+      cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 1 H)) :=
   by reflexivity
 
-  definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2)
-    : loop_spaces_fun2 (n+1, fin.mk 2 H) ~*
-      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) :=
-  proof !ap1_compose⁻¹* qed
+  definition loopns_fun2_add1_2 (n : ℕ) (H : 2 < succ 2)
+    : loopns_fun2 (n+1, fin.mk 2 H) ~*
+      cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 2 H)) :=
+  proof !ap1_pcompose⁻¹* qed
 
   definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ :=
   λx, succ n * pr1 x + val (pr2 x)
@@ -537,126 +537,126 @@ namespace chain_complex
     note: in the following theorem the (n+1) case is 3 times the same,
     so maybe this can be simplified
   -/
-  definition loop_spaces2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)),
-    loop_spaces (nat_of_str (n, x)) ≃* loop_spaces2 (n, x)
+  definition loopns2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)),
+    loopns (nat_of_str (n, x)) ≃* loopns2 (n, x)
   |  0    (fin.mk 0 H)     := by reflexivity
   |  0    (fin.mk 1 H)     := by reflexivity
   |  0    (fin.mk 2 H)     := by reflexivity
   | (n+1) (fin.mk 0 H)     :=
     begin
       apply loop_pequiv_loop,
-      rexact loop_spaces2_pequiv' n (fin.mk 0 H)
+      rexact loopns2_pequiv' n (fin.mk 0 H)
     end
   | (n+1) (fin.mk 1 H)     :=
     begin
       apply loop_pequiv_loop,
-      rexact loop_spaces2_pequiv' n (fin.mk 1 H)
+      rexact loopns2_pequiv' n (fin.mk 1 H)
     end
   | (n+1) (fin.mk 2 H)     :=
     begin
       apply loop_pequiv_loop,
-      rexact loop_spaces2_pequiv' n (fin.mk 2 H)
+      rexact loopns2_pequiv' n (fin.mk 2 H)
     end
   | n     (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
-  definition loop_spaces2_pequiv : Π(x : +3ℕ),
-    loop_spaces (nat_of_str x) ≃* loop_spaces2 x
-  | (n, x) := loop_spaces2_pequiv' n x
+  definition loopns2_pequiv : Π(x : +3ℕ),
+    loopns (nat_of_str x) ≃* loopns2 x
+  | (n, x) := loopns2_pequiv' n x
 
   local attribute loop_pequiv_loop [reducible]
 
   /- all cases where n>0 are basically the same -/
-  definition loop_spaces_fun2_phomotopy (x : +3ℕ) :
-    loop_spaces2_pequiv x ∘* loop_spaces_fun (nat_of_str x) ~*
-      (loop_spaces_fun2 x ∘* loop_spaces2_pequiv (S x))
-    ∘* pcast (ap (loop_spaces) (nat_of_str_3S x)) :=
+  definition loopns_fun2_phomotopy (x : +3ℕ) :
+    loopns2_pequiv x ∘* loopns_fun (nat_of_str x) ~*
+      (loopns_fun2 x ∘* loopns2_pequiv (S x))
+    ∘* pcast (ap (loopns) (nat_of_str_3S x)) :=
   begin
     cases x with n x, cases x with k H,
     do 3 (cases k with k; rotate 1),
     { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left},
     { /-k=0-/
       induction n with n IH,
-      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+      { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹* ⬝* !pcompose_pid⁻¹*,
         reflexivity},
-      { refine _ ⬝* !comp_pid⁻¹*,
-        refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_0⁻¹*,
-        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
-        exact IH ⬝* !comp_pid}},
+      { refine _ ⬝* !pcompose_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_0⁻¹*,
+        refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy,
+        exact IH ⬝* !pcompose_pid}},
     { /-k=1-/
       induction n with n IH,
-      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+      { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹* ⬝* !pcompose_pid⁻¹*,
         reflexivity},
-      { refine _ ⬝* !comp_pid⁻¹*,
-        refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_1⁻¹*,
-        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
-        exact IH ⬝* !comp_pid}},
+      { refine _ ⬝* !pcompose_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_1⁻¹*,
+        refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy,
+        exact IH ⬝* !pcompose_pid}},
     { /-k=2-/
       induction n with n IH,
-      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
-        refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
-        { exact (comp_pid (chain_complex.boundary_map f))⁻¹*},
+      { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹*,
+        refine !pcompose_pid⁻¹* ⬝* pconcat2 _ _,
+        { exact (pcompose_pid (chain_complex.boundary_map f))⁻¹*},
         { refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}},
-      { refine _ ⬝* !comp_pid⁻¹*,
-        refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_2⁻¹*,
-        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
-        exact IH ⬝* !comp_pid}},
+      { refine _ ⬝* !pcompose_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_2⁻¹*,
+        refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy,
+        exact IH ⬝* !pcompose_pid}},
   end
 
-  definition LES_of_loop_spaces2 [constructor] : type_chain_complex +3ℕ :=
+  definition LES_of_loopns2 [constructor] : type_chain_complex +3ℕ :=
   transfer_type_chain_complex2
-    LES_of_loop_spaces
+    LES_of_loopns
     !fin_prod_nat_equiv_nat
     nat_of_str_3S
-    @loop_spaces_fun2
-    @loop_spaces2_pequiv
+    @loopns_fun2
+    @loopns2_pequiv
     begin
       intro m x,
-      refine loop_spaces_fun2_phomotopy m x ⬝ _,
-      apply ap (loop_spaces_fun2 m), apply ap (loop_spaces2_pequiv (S m)),
+      refine loopns_fun2_phomotopy m x ⬝ _,
+      apply ap (loopns_fun2 m), apply ap (loopns2_pequiv (S m)),
       esimp, exact ap010 cast !ap_compose⁻¹ x
     end
 
-  definition is_exact_LES_of_loop_spaces2 : is_exact_t LES_of_loop_spaces2 :=
+  definition is_exact_LES_of_loopns2 : is_exact_t LES_of_loopns2 :=
   begin
     intro n,
     apply is_exact_at_t_transfer2,
-    apply is_exact_LES_of_loop_spaces
+    apply is_exact_LES_of_loopns
   end
 
   definition LES_of_homotopy_groups' [constructor] : chain_complex +3ℕ :=
-  trunc_chain_complex LES_of_loop_spaces2
+  trunc_chain_complex LES_of_loopns2
 
 /--------------
     PART 4
  --------------/
 
   definition homotopy_groups [reducible] : +3ℕ → Set*
-  | (n, fin.mk 0 H) := π*[n] Y
-  | (n, fin.mk 1 H) := π*[n] X
-  | (n, fin.mk k H) := π*[n] (pfiber f)
+  | (n, fin.mk 0 H) := π[n] Y
+  | (n, fin.mk 1 H) := π[n] X
+  | (n, fin.mk k H) := π[n] (pfiber f)
 
-  definition homotopy_groups_pequiv_loop_spaces2 [reducible]
-    : Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups n
+  definition homotopy_groups_pequiv_loopns2 [reducible]
+    : Π(n : +3ℕ), ptrunc 0 (loopns2 n) ≃* homotopy_groups n
   | (n, fin.mk 0 H) := by reflexivity
   | (n, fin.mk 1 H) := by reflexivity
   | (n, fin.mk 2 H) := by reflexivity
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
   definition homotopy_groups_fun : Π(n : +3ℕ), homotopy_groups (S n) →* homotopy_groups n
-  | (n, fin.mk 0 H) := proof π→*[n] f qed
-  | (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed
+  | (n, fin.mk 0 H) := proof π→[n] f qed
+  | (n, fin.mk 1 H) := proof π→[n] (ppoint f) qed
   | (n, fin.mk 2 H) :=
-    proof π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n qed
+    proof π→[n] boundary_map ∘* homotopy_group_succ_in Y n qed
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
-  definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible]
-    : Π(n : +3ℕ), homotopy_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~*
-      homotopy_groups_fun n ∘* homotopy_groups_pequiv_loop_spaces2 (S n)
+  definition homotopy_groups_fun_phomotopy_loopns_fun2 [reducible]
+    : Π(n : +3ℕ), homotopy_groups_pequiv_loopns2 n ∘* ptrunc_functor 0 (loopns_fun2 n) ~*
+      homotopy_groups_fun n ∘* homotopy_groups_pequiv_loopns2 (S n)
   | (n, fin.mk 0 H) := by reflexivity
   | (n, fin.mk 1 H) := by reflexivity
   | (n, fin.mk 2 H) :=
     begin
-      refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+      refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹*,
       refine !ptrunc_functor_pcompose
     end
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
@@ -665,32 +665,32 @@ namespace chain_complex
   transfer_chain_complex
     LES_of_homotopy_groups'
     homotopy_groups_fun
-    homotopy_groups_pequiv_loop_spaces2
-    homotopy_groups_fun_phomotopy_loop_spaces_fun2
+    homotopy_groups_pequiv_loopns2
+    homotopy_groups_fun_phomotopy_loopns_fun2
 
   definition is_exact_LES_of_homotopy_groups : is_exact LES_of_homotopy_groups :=
   begin
     intro n,
     apply is_exact_at_transfer,
     apply is_exact_at_trunc,
-    apply is_exact_LES_of_loop_spaces2
+    apply is_exact_LES_of_loopns2
   end
 
   variable (n : ℕ)
 
   /- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/
-  example : LES_of_homotopy_groups (str_of_nat 6)  = π*[2] Y          :> Set* := by reflexivity
-  example : LES_of_homotopy_groups (str_of_nat 7)  = π*[2] X          :> Set* := by reflexivity
-  example : LES_of_homotopy_groups (str_of_nat 8)  = π*[2] (pfiber f) :> Set* := by reflexivity
-  example : LES_of_homotopy_groups (str_of_nat 9)  = π*[3] Y          :> Set* := by reflexivity
-  example : LES_of_homotopy_groups (str_of_nat 10) = π*[3] X          :> Set* := by reflexivity
-  example : LES_of_homotopy_groups (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 6)  = π[2] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 7)  = π[2] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 8)  = π[2] (pfiber f) :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 9)  = π[3] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 10) = π[3] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 11) = π[3] (pfiber f) :> Set* := by reflexivity
 
-  definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π*[n] Y :=
+  definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π[n] Y :=
   by reflexivity
-  definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π*[n] X :=
+  definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π[n] X :=
   by reflexivity
-  definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π*[n] (pfiber f) :=
+  definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π[n] (pfiber f) :=
   by reflexivity
 
   /-
@@ -698,13 +698,13 @@ namespace chain_complex
   -/
 
   definition LES_of_homotopy_groups_fun_0 :
-    cc_to_fn LES_of_homotopy_groups (n, 0) = π→*[n] f :=
+    cc_to_fn LES_of_homotopy_groups (n, 0) = π→[n] f :=
   by reflexivity
   definition LES_of_homotopy_groups_fun_1 :
-    cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) :=
+    cc_to_fn LES_of_homotopy_groups (n, 1) = π→[n] (ppoint f) :=
   by reflexivity
   definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) =
-    π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n :=
+    π→[n] boundary_map ∘* homotopy_group_succ_in Y n :=
   by reflexivity
 
   open group
@@ -735,10 +735,10 @@ namespace chain_complex
     Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k
   | (k, fin.mk 0 H) :=
     proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 0))
-                          (phomotopy_group_functor_mul _ _) qed
+                          (homotopy_group_functor_mul _ _) qed
   | (k, fin.mk 1 H) :=
     proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 1))
-                          (phomotopy_group_functor_mul _ _) qed
+                          (homotopy_group_functor_mul _ _) qed
   | (k, fin.mk 2 H) :=
     begin
       apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)),
@@ -773,30 +773,30 @@ namespace chain_complex
     : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n
   | (n, fin.mk 0 H) := proof Ω→[n] f qed
   | (n, fin.mk 1 H) := proof Ω→[n] g qed
-  | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loop_space_succ_in Y n qed
+  | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in Y n qed
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
   definition fibration_sequence_pequiv : Π(x : +3ℕ),
-     loop_spaces2 f x ≃* fibration_sequence_car x
+     loopns2 f x ≃* fibration_sequence_car x
   | (n, fin.mk 0 H) := by reflexivity
   | (n, fin.mk 1 H) := by reflexivity
   | (n, fin.mk 2 H) := loopn_pequiv_loopn n e
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
   definition fibration_sequence_fun_phomotopy : Π(x : +3ℕ),
-    fibration_sequence_pequiv x ∘* loop_spaces_fun2 f x ~*
+    fibration_sequence_pequiv x ∘* loopns_fun2 f x ~*
       (fibration_sequence_fun x ∘* fibration_sequence_pequiv (S x))
   | (n, fin.mk 0 H) := by reflexivity
   | (n, fin.mk 1 H) :=
-    begin refine !pid_comp ⬝* _, refine apn_phomotopy n p ⬝* _,
-      refine !apn_compose ⬝* _, reflexivity end
-  | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !comp_pid⁻¹*, apply pwhisker_right,
-      refine _ ⬝* !apn_compose⁻¹*, reflexivity end
+    begin refine !pid_pcompose ⬝* _, refine apn_phomotopy n p ⬝* _,
+      refine !apn_pcompose ⬝* _, reflexivity end
+  | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !pcompose_pid⁻¹*, apply pwhisker_right,
+      refine _ ⬝* !apn_pcompose⁻¹*, reflexivity end
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
   definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ :=
   transfer_type_chain_complex
-    (LES_of_loop_spaces2 f)
+    (LES_of_loopns2 f)
     fibration_sequence_fun
     fibration_sequence_pequiv
     fibration_sequence_fun_phomotopy
@@ -805,7 +805,7 @@ namespace chain_complex
   begin
     intro n,
     apply is_exact_at_t_transfer,
-    apply is_exact_LES_of_loop_spaces2
+    apply is_exact_LES_of_loopns2
   end
 
   definition fibration_sequence [constructor] : chain_complex +3ℕ :=
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index 86246dd17..e1f3d37b1 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -220,7 +220,7 @@ namespace circle
   pointed.mk base
 
   definition pcircle [constructor] : Type* := pointed.mk' S¹
-  notation `S¹.` := pcircle
+  notation `S¹*` := pcircle
 
   definition loop_neq_idp : loop ≠ idp :=
   assume H : loop = idp,
@@ -295,13 +295,13 @@ namespace circle
   --the carrier of π₁(S¹) is the set-truncation of base = base.
   open algebra trunc group
 
-  definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ :=
+  definition fg_carrier_equiv_int : π[1](S¹*) ≃ ℤ :=
   trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed
 
   definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
   eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
 
-  definition fundamental_group_of_circle : π₁(S¹.) ≃g gℤ :=
+  definition fundamental_group_of_circle : π₁(S¹*) ≃g gℤ :=
   begin
     apply (isomorphism_of_equiv fg_carrier_equiv_int),
     intros g h,
@@ -310,9 +310,9 @@ namespace circle
   end
 
   open nat
-  definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. ≃g G0 :=
+  definition homotopy_group_of_circle (n : ℕ) : πg[n+2] S¹* ≃g G0 :=
   begin
-    refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _,
+    refine @trivial_homotopy_add_of_is_set_loopn S¹* 1 n _,
     apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv
   end
 
@@ -337,8 +337,8 @@ namespace circle
   proposition is_conn_circle [instance] : is_conn 0 S¹ :=
   sphere.is_conn_sphere -1.+2
 
-  definition is_conn_pcircle [instance] : is_conn 0 S¹. := !is_conn_circle
-  definition is_trunc_pcircle [instance] : is_trunc 1 S¹. := !is_trunc_circle
+  definition is_conn_pcircle [instance] : is_conn 0 S¹* := !is_conn_circle
+  definition is_trunc_pcircle [instance] : is_trunc 1 S¹* := !is_trunc_circle
 
   definition circle_mul [reducible] (x y : S¹) : S¹ :=
   circle.elim y (circle_turn y) x
diff --git a/hott/homotopy/complex_hopf.hlean b/hott/homotopy/complex_hopf.hlean
index aff545afa..e89308bf6 100644
--- a/hott/homotopy/complex_hopf.hlean
+++ b/hott/homotopy/complex_hopf.hlean
@@ -36,10 +36,10 @@ namespace hopf
     apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x
   end
 
-  definition complex_phopf [constructor] : S. 3 →* S. 2 :=
+  definition complex_phopf [constructor] : S* 3 →* S* 2 :=
   proof pmap.mk complex_hopf idp qed
 
-  definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 :=
+  definition pfiber_complex_phopf : pfiber complex_phopf ≃* S* 1 :=
   begin
     fapply pequiv_of_equiv,
     { esimp, unfold [complex_hopf],
diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean
index acd26b15d..2f8a79ceb 100644
--- a/hott/homotopy/freudenthal.hlean
+++ b/hott/homotopy/freudenthal.hlean
@@ -178,12 +178,12 @@ definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2
 freudenthal_pequiv A H
 
 definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
-  : π*[k + 1] (psusp A) ≃* π*[k] A  :=
+  : π[k + 1] (psusp A) ≃* π[k] A  :=
 calc
-  π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : phomotopy_group_succ_in (psusp A) k
-    ... ≃* Ω[k] (ptrunc k (Ω (psusp A)))     : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A))
+  π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in (psusp A) k
+    ... ≃* Ω[k] (ptrunc k (Ω (psusp A)))     : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A))
     ... ≃* Ω[k] (ptrunc k A)                 : loopn_pequiv_loopn k (freudenthal_pequiv A H)
-    ... ≃* π*[k] A                           : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+    ... ≃* π[k] A                           : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
 
 definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A]
   (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (psusp A) ≃g πg[k+1] A :=
@@ -191,17 +191,17 @@ begin
   fapply isomorphism_of_equiv,
   { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)},
   { intro g h,
-    refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con,
-    apply ap !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
+    refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con,
+    apply ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
     refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con,
-    refine ap !phomotopy_group_pequiv_loop_ptrunc _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_con,
-    apply phomotopy_group_succ_in_con}
+    refine ap !homotopy_group_pequiv_loop_ptrunc _ ⬝ !homotopy_group_pequiv_loop_ptrunc_con,
+    apply homotopy_group_succ_in_con}
 end
 
 namespace susp
 
   definition iterate_psusp_stability_pequiv (A : Type*) {k n : ℕ} [is_conn 0 A]
-    (H : k ≤ 2 * n) : π*[k + 1] (iterate_psusp (n + 1) A) ≃* π*[k] (iterate_psusp n A) :=
+    (H : k ≤ 2 * n) : π[k + 1] (iterate_psusp (n + 1) A) ≃* π[k] (iterate_psusp n A) :=
   have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _,
   freudenthal_homotopy_group_pequiv (iterate_psusp n A) H
 
@@ -227,8 +227,8 @@ namespace susp
   end
 
   definition iterate_susp_stability_pequiv (A : Type) {k n : ℕ}
-    (H : k + 2 ≤ 2 * n) : π*[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃*
-                          π*[k    ] (pointed.MK (iterate_susp (n + 1) A) !north) :=
+    (H : k + 2 ≤ 2 * n) : π[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃*
+                          π[k    ] (pointed.MK (iterate_susp (n + 1) A) !north) :=
   have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from
     stability_helper2 A H,
   freudenthal_homotopy_group_pequiv (pointed.MK (iterate_susp (n + 1) A) !north)
diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean
index 1331bc036..d6953bfc1 100644
--- a/hott/homotopy/homotopy_group.hlean
+++ b/hott/homotopy/homotopy_group.hlean
@@ -34,13 +34,13 @@ namespace is_trunc
       have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H),
       have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loop_of_is_trunc,
       apply is_trunc_equiv_closed_rev,
-      { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
+      { apply equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)}
   end
 
   -- Corollary 8.3.3
   section
   open sphere sphere.ops sphere_index
-  theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
+  theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S* n)) :=
   begin
     cases n with n,
     { exfalso, apply not_lt_zero, exact H},
@@ -54,12 +54,12 @@ namespace is_trunc
   @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
 
   theorem homotopy_group_trunc_of_le (A : Type*) (n k : ℕ) (H : k ≤ n)
-    : π*[k] (ptrunc n A) ≃* π*[k] A :=
+    : π[k] (ptrunc n A) ≃* π[k] A :=
   begin
-    refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _,
+    refine !homotopy_group_pequiv_loop_ptrunc ⬝e* _,
     refine loopn_pequiv_loopn _ (ptrunc_ptrunc_pequiv_left _ _) ⬝e* _,
     exact of_nat_le_of_nat H,
-    exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
+    exact !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
   end
 
   /- Corollaries of the LES of homotopy groups -/
@@ -96,11 +96,11 @@ namespace is_trunc
   theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B)
     (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) :=
   begin
-    have π→*[k] pdown.{v u} ∘* π→*[k] (plift_functor f) ∘* π→*[k] pup.{u v} ~* π→*[k] f,
+    have π→[k] pdown.{v u} ∘* π→[k] (plift_functor f) ∘* π→[k] pup.{u v} ~* π→[k] f,
     begin
-      refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _,
-      refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
-      apply phomotopy_group_functor_phomotopy, apply plift_functor_phomotopy
+      refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _,
+      refine !homotopy_group_functor_compose⁻¹* ⬝* _,
+      apply homotopy_group_functor_phomotopy, apply plift_functor_phomotopy
     end,
     have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this,
     apply is_equiv.homotopy_closed, rotate 1,
@@ -112,8 +112,8 @@ namespace is_trunc
   end
 
   definition π_equiv_π_of_is_connected {A B : Type*} {n k : ℕ} (f : A →* B)
-     (H2 : k ≤ n) [H : is_conn_fun n f] : π*[k] A ≃* π*[k] B :=
-  pequiv_of_pmap (π→*[k] f) (is_equiv_π_of_is_connected f H2)
+     (H2 : k ≤ n) [H : is_conn_fun n f] : π[k] A ≃* π[k] B :=
+  pequiv_of_pmap (π→[k] f) (is_equiv_π_of_is_connected f H2)
 
   -- TODO: prove this for A and B in different universe levels
   theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B)
@@ -128,7 +128,7 @@ namespace is_trunc
   -/
   definition whitehead_principle (n : ℕ₋₂) {A B : Type}
     [HA : is_trunc n A] [HB : is_trunc n B] (f : A → B) (H' : is_equiv (trunc_functor 0 f))
-    (H : Πa k, is_equiv (π→*[k + 1] (pmap_of_map f a))) : is_equiv f :=
+    (H : Πa k, is_equiv (π→[k + 1] (pmap_of_map f a))) : is_equiv f :=
   begin
     revert A B HA HB f H' H, induction n with n IH: intros,
     { apply is_equiv_of_is_contr},
@@ -138,24 +138,24 @@ namespace is_trunc
       apply IH, do 2 (esimp; exact _),
       { rexact H a 0},
       intro p k,
-      have is_equiv (π→*[k + 1] (Ω→(pmap_of_map f a))),
-        from is_equiv_phomotopy_group_functor_ap1 (k+1) (pmap_of_map f a),
+      have is_equiv (π→[k + 1] (Ω→(pmap_of_map f a))),
+        from is_equiv_homotopy_group_functor_ap1 (k+1) (pmap_of_map f a),
       have Π(b : A) (p : a = b),
-        is_equiv (pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))),
+        is_equiv (pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))),
       begin
         intro b p, induction p, apply is_equiv.homotopy_closed, exact this,
-        refine phomotopy_group_functor_phomotopy _ _,
+        refine homotopy_group_functor_phomotopy _ _,
         apply ap1_pmap_of_map
       end,
-      have is_equiv (phomotopy_group_pequiv _
+      have is_equiv (homotopy_group_pequiv _
                       (pequiv_of_eq_pt (!idp_con⁻¹ : ap f p = Ω→ (pmap_of_map f a) p)) ∘
-           pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))),
+           pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))),
       begin
         apply is_equiv_compose, exact this a p,
       end,
       apply is_equiv.homotopy_closed, exact this,
-      refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
-      apply phomotopy_group_functor_phomotopy,
+      refine !homotopy_group_functor_compose⁻¹* ⬝* _,
+      apply homotopy_group_functor_phomotopy,
       fapply phomotopy.mk,
       { esimp, intro q, refine !idp_con⁻¹},
       { esimp, refine !idp_con⁻¹},
@@ -165,23 +165,23 @@ namespace is_trunc
 
   definition whitehead_principle_pointed (n : ℕ₋₂) {A B : Type*}
     [HA : is_trunc n A] [HB : is_trunc n B] [is_conn 0 A] (f : A →* B)
-    (H : Πk, is_equiv (π→*[k] f)) : is_equiv f :=
+    (H : Πk, is_equiv (π→[k] f)) : is_equiv f :=
   begin
     apply whitehead_principle n, rexact H 0,
     intro a k, revert a, apply is_conn.elim -1,
-    have is_equiv (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
-           ∘* π→*[k + 1] f ∘* π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
+    have is_equiv (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
+           ∘* π→[k + 1] f ∘* π→[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
     begin
       apply is_equiv_compose
-              (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)),
-      apply is_equiv_compose (π→*[k + 1] f),
+              (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)),
+      apply is_equiv_compose (π→[k + 1] f),
       all_goals apply is_equiv_homotopy_group_functor,
     end,
     refine @(is_equiv.homotopy_closed _) _ this _,
     apply to_homotopy,
-    refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _,
-    refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
-    apply phomotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map
+    refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _,
+    refine !homotopy_group_functor_compose⁻¹* ⬝* _,
+    apply homotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map
   end
 
   open pointed.ops
@@ -236,7 +236,7 @@ namespace is_trunc
   have H3 : Πa, is_contr (ptrunc n (pfiber (pmap_of_map f a))),
   begin
     intro a, apply is_contr_of_trivial_homotopy_nat_pointed n,
-    { intro k H, apply is_trunc_equiv_closed_rev, exact phomotopy_group_ptrunc_of_le H _,
+    { intro k H, apply is_trunc_equiv_closed_rev, exact homotopy_group_ptrunc_of_le H _,
       rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ
                (LES_of_homotopy_groups (pmap_of_map f a)) (k, 0)
                (is_exact_LES_of_homotopy_groups _ _)
diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean
index fcc08220d..7c2f6699b 100644
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@@ -255,29 +255,29 @@ namespace sphere
 
   namespace ops
     abbreviation S := sphere
-    notation `S.` := psphere
+    notation `S*` := psphere
   end ops
   open sphere.ops
 
   definition sphere_minus_one : S -1 = empty := idp
   definition sphere_succ [unfold_full] (n : ℕ₋₁) : S n.+1 = susp (S n) := idp
-  definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
+  definition psphere_succ [unfold_full] (n : ℕ) : S* (n + 1) = psusp (S* n) := idp
   definition psphere_eq_iterate_susp (n : ℕ)
-    : S. n = pointed.MK (iterate_susp (succ n) empty) !north :=
+    : S* n = pointed.MK (iterate_susp (succ n) empty) !north :=
   begin
     esimp,
     apply ap (λx, pointed.MK (susp x) (@north x)); apply ap (λx, iterate_susp x empty),
     apply add_one_sub_one
   end
 
-  definition equator [constructor] (n : ℕ) : S. n →* Ω (S. (succ n)) :=
-  loop_susp_unit (S. n)
+  definition equator [constructor] (n : ℕ) : S* n →* Ω (S* (succ n)) :=
+  loop_susp_unit (S* n)
 
-  definition surf {n : ℕ} : Ω[n] S. n :=
+  definition surf {n : ℕ} : Ω[n] (S* n) :=
   begin
     induction n with n s,
     { exact @base 0},
-    { exact (loop_space_succ_in (S. (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), }
+    { exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), }
   end
 
   definition bool_of_sphere [unfold 1] : S 0 → bool :=
@@ -293,24 +293,24 @@ namespace sphere
            (λb, match b with | tt := idp | ff := idp end)
            (λx, proof susp.rec_on x idp idp (empty.rec _) qed)
 
-  definition psphere_pequiv_pbool : S. 0 ≃* pbool :=
+  definition psphere_pequiv_pbool : S* 0 ≃* pbool :=
   pequiv_of_equiv sphere_equiv_bool idp
 
   definition sphere_eq_bool : S 0 = bool :=
   ua sphere_equiv_bool
 
-  definition sphere_eq_pbool : S. 0 = pbool :=
+  definition sphere_eq_pbool : S* 0 = pbool :=
   pType_eq sphere_equiv_bool idp
 
   -- TODO1: the commented-out part makes the forward function below "apn _ surf" (the next def also)
   -- TODO2: we could make this a pointed equivalence
-  definition pmap_sphere (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A :=
+  definition psphere_pmap_equiv (A : Type*) (n : ℕ) : (S* n →* A) ≃ Ω[n] A :=
   begin
     -- fapply equiv_change_fun,
     -- {
       revert A, induction n with n IH: intro A,
-      { refine _ ⬝e !pmap_bool_equiv, exact equiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ*},
-      { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e !loop_space_succ_in⁻¹ᵉ* }
+      { refine _ ⬝e !pmap_bool_equiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ*},
+      { refine susp_adjoint_loop (S* n) A ⬝e !IH ⬝e !loopn_succ_in⁻¹ᵉ* }
     -- },
     -- { intro f, exact apn n f surf},
     -- { revert A, induction n with n IH: intro A f,
@@ -318,25 +318,25 @@ namespace sphere
     --   { exact sorry}}
   end
 
-  -- definition pmap_sphere' (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A :=
+  -- definition psphere_pmap_equiv' (A : Type*) (n : ℕ) : (S* n →* A) ≃ Ω[n] A :=
   -- begin
   --   fapply equiv.MK,
   --   { intro f, exact apn n f surf },
   --   { revert A, induction n with n IH: intro A p,
   --     { exact !pmap_bool_equiv⁻¹ᵉ p ∘* psphere_pequiv_pbool },
-  --     { refine (susp_adjoint_loop (S. n) A)⁻¹ᵉ (IH (Ω A) _),
-  --       exact loop_space_succ_in A n p }},
+  --     { refine (susp_adjoint_loop (S* n) A)⁻¹ᵉ (IH (Ω A) _),
+  --       exact loopn_succ_in A n p }},
   --   { exact sorry},
   --   { exact sorry}
   -- end
 
-  protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S. n →* P :=
-  to_inv !pmap_sphere p
+  protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S* n →* P :=
+  to_inv !psphere_pmap_equiv p
 
   -- definition elim_surf {n : ℕ} {P : Type*} (p : Ω[n] P) : apn n (sphere.elim p) surf = p :=
   -- begin
   --   induction n with n IH,
-  --   { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry},
+  --   { esimp [apn,surf,sphere.elim,psphere_pmap_equiv], apply sorry},
   --   { apply sorry}
   -- end
 
@@ -354,7 +354,7 @@ namespace sphere
       apply is_conn_susp }
   end
 
-  theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S. n) :=
+  theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S* n) :=
   transport (λx, is_conn x (sphere n)) (of_nat_sub_one n) (is_conn_sphere n)
 
 end sphere
@@ -364,12 +364,12 @@ open sphere sphere.ops
 namespace is_trunc
   open trunc_index
   variables {n : ℕ} {A : Type}
-  definition is_trunc_of_pmap_sphere_constant
-    (H : Π(a : A) (f : S. n →* pointed.Mk a) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
+  definition is_trunc_of_psphere_pmap_equiv_constant
+    (H : Π(a : A) (f : 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 pmap_sphere,
+    apply is_trunc_equiv_closed, apply psphere_pmap_equiv,
     fapply is_contr.mk,
     { exact pmap.mk (λx, a) idp},
     { intro f, fapply pmap_eq,
@@ -380,27 +380,27 @@ namespace is_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_pmap_sphere_constant,
+    apply is_trunc_of_psphere_pmap_equiv_constant,
     intros, cases f with f p, esimp at *, apply H
   end
 
-  definition pmap_sphere_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A]
-    (a : A) (f : S. n →* pointed.Mk a) (x : S n) : f x = f base :=
+  definition psphere_pmap_equiv_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A]
+    (a : A) (f : 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,
-    note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H',
+    note H'' := @is_trunc_equiv_closed_rev _ _ _ !psphere_pmap_equiv H',
     have p : (f = pmap.mk (λx, f base) (respect_pt f)),
       by apply is_prop.elim,
     exact ap10 (ap pmap.to_fun p) x
   end
 
-  definition pmap_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
-    (a : A) (f : 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⁻¹
+  definition psphere_pmap_equiv_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+    (a : A) (f : S* n →* pointed.Mk a) (x y : S n) : f x = f y :=
+  let H := psphere_pmap_equiv_constant_of_is_trunc' a f in !H ⬝ !H⁻¹
 
   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
+  psphere_pmap_equiv_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 :=
diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean
index 487f19ac7..3c15db76d 100644
--- a/hott/homotopy/sphere2.hlean
+++ b/hott/homotopy/sphere2.hlean
@@ -20,7 +20,7 @@ namespace sphere
   /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/
   open sphere sphere.ops int circle hopf
 
-  definition π2S2 : πg[1+1] (S. 2) ≃g gℤ :=
+  definition π2S2 : πg[1+1] (S* 2) ≃g gℤ :=
   begin
     refine _ ⬝g fundamental_group_of_circle,
     refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_phopf,
@@ -47,7 +47,7 @@ namespace sphere
   end
 
   open circle
-  definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S. 3) ≃g πg[n+2 +1] (S. 2) :=
+  definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S* 3) ≃g πg[n+2 +1] (S* 2) :=
   begin
     fapply isomorphism_of_equiv,
     { fapply equiv.mk,
@@ -75,15 +75,15 @@ namespace sphere
   end
 
   definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) :
-    π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) :=
+    π[k + 1] (S* (n+1)) ≃* π[k] (S* n) :=
   begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_pequiv empty H end
 
   definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n)
-    : πg[k+1 +1] (S. (n+1)) ≃g πg[k+1] (S. n) :=
+    : πg[k+1 +1] (S* (n+1)) ≃g πg[k+1] (S* n) :=
   begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_isomorphism empty H end
 
   open int circle hopf
-  definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) ≃g gℤ :=
+  definition πnSn (n : ℕ) : πg[n+1] (S* (succ n)) ≃g gℤ :=
   begin
     cases n with n IH,
     { exact fundamental_group_of_circle},
@@ -93,10 +93,10 @@ namespace sphere
         rexact add_mul_le_mul_add n 1 2}}
   end
 
-  theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) :=
+  theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S* (succ n)) :=
   begin
     intro H,
-    note H2 := trivial_ghomotopy_group_of_is_trunc (S. (succ n)) n n !le.refl,
+    note H2 := trivial_ghomotopy_group_of_is_trunc (S* (succ n)) n n !le.refl,
     have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)),
     have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
     apply H4,
@@ -120,7 +120,7 @@ namespace sphere
 
   end
 
-  definition π3S2 : πg[2+1] (S. 2) ≃g gℤ :=
+  definition π3S2 : πg[2+1] (S* 2) ≃g gℤ :=
   (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2
 
 end sphere
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index 8db9fb116..97c0f9c84 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -321,19 +321,19 @@ namespace susp
     { intro f, exact ap1 f ∘* loop_susp_unit X},
     { intro g, exact loop_susp_counit Y ∘* psusp_functor g},
     { intro g, apply eq_of_phomotopy, esimp,
-      refine !pwhisker_right !ap1_compose ⬝* _,
+      refine !pwhisker_right !ap1_pcompose ⬝* _,
       refine !passoc ⬝* _,
       refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _,
       refine !passoc⁻¹* ⬝* _,
       refine !pwhisker_right !loop_susp_counit_unit ⬝* _,
-      apply pid_comp},
+      apply pid_pcompose},
     { intro f, apply eq_of_phomotopy, esimp,
       refine !pwhisker_left !psusp_functor_compose ⬝* _,
       refine !passoc⁻¹* ⬝* _,
       refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _,
       refine !passoc ⬝* _,
       refine !pwhisker_left !loop_susp_unit_counit ⬝* _,
-      apply comp_pid},
+      apply pcompose_pid},
   end
 
   definition susp_adjoint_loop_nat_right (f : psusp X →* Y) (g : Y →* Z)
@@ -342,7 +342,7 @@ namespace susp
     esimp [susp_adjoint_loop],
     refine _ ⬝* !passoc,
     apply pwhisker_right,
-    apply ap1_compose
+    apply ap1_pcompose
   end
 
   definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y)
diff --git a/hott/naming_conventions.md b/hott/naming_conventions.md
new file mode 100644
index 000000000..37ab0c89b
--- /dev/null
+++ b/hott/naming_conventions.md
@@ -0,0 +1,14 @@
+HoTT Naming Conventions
+=======================
+
+
+[generic naming conventions go here]
+
+Pointed Types
+-------------
+
+We use a prefix `p` to specify that an operation/construction is pointed. For example `pequiv` is
+pointed equivalences and `phomotopy` are pointed homotopies. Only if a construction only works for
+pointed types and has no unpointed equivalent we omit the `p` (examples: `loop` `loopn`
+`homotopy_group`). A lemma about pointed constructions repeats the `p` for every name, for example
+`psusp_pequiv_psusp` or `pid_pcompose`. For notation we append `*` for the pointed version, like `Type*` (this is the universe of pointed types, not the universe considered as a pointed type), `S*` or `bool*`. For notations which only make sense pointed we don't add the star, like `Ω[n]` or `π[k]`.
\ No newline at end of file
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 5f6b417a4..985df4f8f 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -19,15 +19,15 @@ namespace pointed
   definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B :=
   pointed.mk (f pt)
 
-  definition ploop_space [reducible] [constructor] (A : Type*) : Type* :=
+  definition loop [reducible] [constructor] (A : Type*) : Type* :=
   pointed.mk' (point A = point A)
 
-  definition iterated_ploop_space [reducible] : ℕ → Type* → Type*
-  | iterated_ploop_space  0    X := X
-  | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X)
+  definition loopn [reducible] : ℕ → Type* → Type*
+  | loopn  0    X := X
+  | loopn (n+1) X := loop (loopn n X)
 
-  notation `Ω` := ploop_space
-  notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A
+  notation `Ω` := loop
+  notation `Ω[`:95 n:0 `]`:0 := loopn n
 
   namespace ops
     -- this is in a separate namespace because it caused type class inference to loop in some places
@@ -40,17 +40,17 @@ namespace pointed
     (n : ℕ₋₂) [H : is_trunc (n.+1) A] : is_trunc n (Ω A) :=
   !is_trunc_eq
 
-  definition iterated_ploop_space_zero [unfold_full] (A : Type*)
+  definition loopn_zero_eq [unfold_full] (A : Type*)
     : Ω[0] A = A := rfl
 
-  definition iterated_ploop_space_succ [unfold_full] (k : ℕ) (A : Type*)
-    : Ω[succ k] A = Ω Ω[k] A := rfl
+  definition loopn_succ_eq [unfold_full] (k : ℕ) (A : Type*)
+    : Ω[succ k] A = Ω (Ω[k] A) := rfl
 
   definition rfln  [constructor] [reducible] {n : ℕ} {A : Type*} : Ω[n] A := pt
   definition refln [constructor] [reducible] (n : ℕ) (A : Type*) : Ω[n] A := pt
   definition refln_eq_refl [unfold_full] (A : Type*) (n : ℕ) : rfln = rfl :> Ω[succ n] A := rfl
 
-  definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
+  definition loopn_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
   Ω[n] (pointed.mk' A)
 
   definition loop_mul {k : ℕ} {A : Type*} (mul : A → A → A) : Ω[k] A → Ω[k] A → Ω[k] A :=
@@ -131,14 +131,14 @@ namespace pointed
     induction pf, induction pg, induction ph, reflexivity
   end
 
-  definition pid_comp [constructor] (f : A →* B) : pid B ∘* f ~* f :=
+  definition pid_pcompose [constructor] (f : A →* B) : pid B ∘* f ~* f :=
   begin
     fconstructor,
     { intro a, reflexivity},
     { reflexivity}
   end
 
-  definition comp_pid [constructor] (f : A →* B) : f ∘* pid A ~* f :=
+  definition pcompose_pid [constructor] (f : A →* B) : f ∘* pid A ~* f :=
   begin
     fconstructor,
     { intro a, reflexivity},
@@ -223,7 +223,7 @@ namespace pointed
   begin
   induction n with n IH,
   { exact f},
-  { esimp [iterated_ploop_space], exact ap1 IH}
+  { esimp [loopn], exact ap1 IH}
   end
 
   prefix `Ω→`:(max+5) := ap1
@@ -279,7 +279,7 @@ namespace pointed
   definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) :=
   !is_equiv_cast
 
-  definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
+  definition ap1_pid [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
   begin
     fapply phomotopy.mk,
     { intro p, esimp, refine !idp_con ⬝ !ap_id},
@@ -293,7 +293,7 @@ namespace pointed
     { reflexivity}
   end
 
-  definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
+  definition ap1_pcompose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
   begin
     induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
     induction pg, induction pf,
@@ -302,7 +302,7 @@ namespace pointed
     { reflexivity}
   end
 
-  definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
+  definition ap1_pcompose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
   begin
     fconstructor,
     { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
@@ -321,12 +321,6 @@ namespace pointed
     rewrite [▸*,ap_inv, +con_inv, inv_inv, +con.assoc], repeat apply whisker_left
   end
 
-  definition pcast_ap_loop_space {A B : Type*} (p : A = B)
-    : pcast (ap ploop_space p) ~* Ω→ (pcast p) :=
-  begin
-    induction p, exact !ap1_id⁻¹*
-  end
-
   definition pinverse_con [constructor] {X : Type*} (p q : Ω X)
     : pinverse (p ⬝ q) = pinverse q ⬝ pinverse p :=
   !con_inv
@@ -411,18 +405,18 @@ namespace pointed
     { exact ap1_phomotopy IH}
   end
 
-  definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
+  definition apn_pcompose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
   begin
     induction n with n IH,
     { reflexivity},
-    { refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
+    { refine ap1_phomotopy IH ⬝* _, apply ap1_pcompose}
   end
 
   definition apn_pid [constructor] {A : Type*} (n : ℕ) : apn n (pid A) ~* pid (Ω[n] A) :=
   begin
     induction n with n IH,
     { reflexivity},
-    { exact ap1_phomotopy IH ⬝* ap1_id}
+    { exact ap1_phomotopy IH ⬝* ap1_pid}
   end
 
   theorem apn_con (n : ℕ) (f : A →* B) (p q : Ω[n+1] A)
@@ -439,7 +433,7 @@ namespace pointed
     { reflexivity}
   end
 
-  definition pcast_loop_space [constructor] {A B : Type*} (p : A = B) :
+  definition pcast_ap_loop [constructor] {A B : Type*} (p : A = B) :
     pcast (ap Ω p) ~* ap1 (pcast p) :=
   begin
     fapply phomotopy.mk,
@@ -589,7 +583,7 @@ namespace pointed
     refine _⁻¹* ⬝* pwhisker_left f⁻¹ᵉ* p ⬝* _:
     refine !passoc⁻¹* ⬝* _:
     refine pwhisker_right _ (pleft_inv f) ⬝* _:
-    apply pid_comp
+    apply pid_pcompose
   end
 
   definition pcancel_right (f : A ≃* B) {g h : B →* C} (p : g ∘* f ~* h ∘* f) : g ~* h :=
@@ -597,7 +591,7 @@ namespace pointed
     refine _⁻¹* ⬝* pwhisker_right f⁻¹ᵉ* p ⬝* _:
     refine !passoc ⬝* _:
     refine pwhisker_left _ (pright_inv f) ⬝* _:
-    apply comp_pid
+    apply pcompose_pid
   end
 
   definition phomotopy_pinv_right_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C}
@@ -606,7 +600,7 @@ namespace pointed
     refine _ ⬝* pwhisker_right _ p, symmetry,
     refine !passoc ⬝* _,
     refine pwhisker_left _ (pright_inv f) ⬝* _,
-    apply comp_pid
+    apply pcompose_pid
   end
 
   definition phomotopy_of_pinv_right_phomotopy {f : B ≃* A} {g : B →* C} {h : A →* C}
@@ -615,7 +609,7 @@ namespace pointed
     refine _ ⬝* pwhisker_right _ p, symmetry,
     refine !passoc ⬝* _,
     refine pwhisker_left _ (pleft_inv f) ⬝* _,
-    apply comp_pid
+    apply pcompose_pid
   end
 
   definition pinv_right_phomotopy_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C}
@@ -632,7 +626,7 @@ namespace pointed
     refine _ ⬝* pwhisker_left _ p, symmetry,
     refine !passoc⁻¹* ⬝* _,
     refine pwhisker_right _ (pleft_inv f) ⬝* _,
-    apply pid_comp
+    apply pid_pcompose
   end
 
   definition phomotopy_of_pinv_left_phomotopy {f : C ≃* B} {g : A →* B} {h : A →* C}
@@ -641,7 +635,7 @@ namespace pointed
     refine _ ⬝* pwhisker_left _ p, symmetry,
     refine !passoc⁻¹* ⬝* _,
     refine pwhisker_right _ (pright_inv f) ⬝* _,
-    apply pid_comp
+    apply pid_pcompose
   end
 
   definition pinv_left_phomotopy_of_phomotopy {f : B ≃* C} {g : A →* B} {h : A →* C}
@@ -661,18 +655,18 @@ namespace pointed
     { apply pleft_inv},
     { replace nat.succ n with n + 1,
       rewrite [+apn_succ],
-      refine !ap1_compose⁻¹* ⬝* _,
+      refine !ap1_pcompose⁻¹* ⬝* _,
       refine ap1_phomotopy IH ⬝* _,
-      apply ap1_id}
+      apply ap1_pid}
   end end
   abstract begin
     induction n with n IH,
     { apply pright_inv},
     { replace nat.succ n with n + 1,
       rewrite [+apn_succ],
-      refine !ap1_compose⁻¹* ⬝* _,
+      refine !ap1_pcompose⁻¹* ⬝* _,
       refine ap1_phomotopy IH ⬝* _,
-      apply ap1_id}
+      apply ap1_pid}
   end end
 
   definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
@@ -753,31 +747,31 @@ namespace pointed
 
   /- properties of iterated loop space -/
   variable (A)
-  definition loop_space_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) :=
+  definition loopn_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) :=
   begin
     induction n with n IH,
     { reflexivity},
     { exact loop_pequiv_loop IH}
   end
 
-  definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) :=
+  definition loopn_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) :=
   begin
     induction n with n IH,
     { reflexivity},
     { exact loop_pequiv_loop IH}
   end
 
-  definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A)  :=
+  definition loopn_succ_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A)  :=
   by reflexivity
 
   variable {A}
 
-  theorem loop_space_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) :
-    loop_space_succ_in A (succ n) (p ⬝ q) =
-    loop_space_succ_in A (succ n) p ⬝ loop_space_succ_in A (succ n) q :=
+  theorem loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) :
+    loopn_succ_in A (succ n) (p ⬝ q) =
+    loopn_succ_in A (succ n) p ⬝ loopn_succ_in A (succ n) q :=
   !loop_pequiv_loop_con
 
-  definition loop_space_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A :=
+  definition loopn_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A :=
   begin
     intros, fapply pType_eq,
     { esimp, transitivity _,
@@ -786,26 +780,26 @@ namespace pointed
     { esimp, apply con.left_inv}
   end
 
-  definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A)
+  definition loopn_space_loop_irrel (n : ℕ) (p : point A = point A)
     : Ω[succ n](pointed.Mk p) = Ω[succ (succ n)] A :> pType :=
   calc
-    Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : eq_of_pequiv !loop_space_succ_in
-      ... = Ω[n] (Ω[2] A)                            : loop_space_loop_irrel
-      ... = Ω[2+n] A                                 : eq_of_pequiv !loop_space_add
+    Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : eq_of_pequiv !loopn_succ_in
+      ... = Ω[n] (Ω[2] A)                            : loopn_loop_irrel
+      ... = Ω[2+n] A                                 : eq_of_pequiv !loopn_add
       ... = Ω[n+2] A                                 : by rewrite [algebra.add.comm]
 
   definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) :
-    loop_space_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loop_space_succ_in A n :=
+    loopn_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n :=
   begin
     induction n with n IH,
     { reflexivity},
-    { exact !ap1_compose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_compose}
+    { exact !ap1_pcompose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_pcompose}
   end
 
   definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
   pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, respect_pt g) (idp_con _)⁻¹))
 
-  definition is_equiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] :
+  definition is_pequiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] :
     is_equiv (@ppcompose_left A B C g) :=
   begin
     fapply is_equiv.adjointify,
@@ -813,13 +807,13 @@ namespace pointed
     all_goals (intros f; esimp; apply eq_of_phomotopy),
     { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc
                                                   ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H))
-                                                  ... ~* f : pid_comp f },
+                                                  ... ~* f : pid_pcompose f },
     { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc
                                                   ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H))
-                                                  ... ~* f : pid_comp f }
+                                                  ... ~* f : pid_pcompose f }
   end
 
-  definition equiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
+  definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
   pequiv_of_pmap (ppcompose_left g) _
 
   definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
@@ -835,15 +829,15 @@ namespace pointed
     { apply eq_of_phomotopy, esimp, apply pconst_pcompose }
   end
 
-  definition equiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C :=
+  definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C :=
   begin
     fapply pequiv.MK,
     { exact ppcompose_right f },
     { exact ppcompose_right f⁻¹ᵉ* },
     { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _,
-      refine pwhisker_left g !pright_inv ⬝* !comp_pid, },
+      refine pwhisker_left g !pright_inv ⬝* !pcompose_pid, },
     { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _,
-      refine pwhisker_left g !pleft_inv ⬝* !comp_pid, },
+      refine pwhisker_left g !pleft_inv ⬝* !pcompose_pid, },
   end
 
 
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 255d5b265..ce877e579 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -420,15 +420,15 @@ namespace is_trunc
     : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](pointed.Mk a)) :=
   begin
     revert A, induction n with n IH,
-    { intro A, esimp [iterated_ploop_space], transitivity _,
+    { intro A, esimp [loopn], transitivity _,
       { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl},
       { apply pi_iff_pi, intro a, esimp, apply is_prop_iff_is_contr, reflexivity}},
-    { intro A, esimp [iterated_ploop_space],
+    { intro A, esimp [loopn],
       transitivity _,
       { apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, apply minus_one_le_succ},
       apply pi_iff_pi, intro a, transitivity _, apply IH,
       transitivity _, apply pi_iff_pi, intro p,
-      rewrite [iterated_loop_space_loop_irrel n p], apply iff.refl, esimp,
+      rewrite [loopn_space_loop_irrel n p], apply iff.refl, esimp,
       apply imp_iff, reflexivity}
   end
 
@@ -437,7 +437,7 @@ namespace is_trunc
     : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) :=
   begin
     induction n with n,
-    { esimp [sub_two,iterated_ploop_space], apply iff.intro,
+    { esimp [sub_two,loopn], apply iff.intro,
         intro H a, exact is_contr_of_inhabited_prop a,
         intro H, apply is_prop_of_imp_is_contr, exact H},
     { apply is_trunc_iff_is_contr_loop_succ},
@@ -718,34 +718,34 @@ namespace trunc
   encode_con p q
 
   -- rename
-  definition iterated_loop_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) :
+  definition loopn_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) :
     Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) :=
   begin
     revert n, induction k with k IH: intro n,
     { reflexivity},
     { refine _ ⬝e* loop_ptrunc_pequiv n (Ω[k] A),
-      rewrite [iterated_ploop_space_succ], apply loop_pequiv_loop,
+      rewrite [loopn_succ_eq], apply loop_pequiv_loop,
       refine _ ⬝e* IH (n.+1),
       rewrite succ_add_nat}
   end
 
-  definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
+  definition loopn_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
     (p q : Ω[succ k] (ptrunc (n+succ k) A)) :
-    iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) =
-    tconcat (iterated_loop_ptrunc_pequiv n (succ k) A p)
-            (iterated_loop_ptrunc_pequiv n (succ k) A q)  :=
+    loopn_ptrunc_pequiv n (succ k) A (p ⬝ q) =
+    tconcat (loopn_ptrunc_pequiv n (succ k) A p)
+            (loopn_ptrunc_pequiv n (succ k) A q)  :=
   begin
     refine _ ⬝ loop_ptrunc_pequiv_con _ _,
     exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con
   end
 
-  definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
+  definition loopn_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
     (p q : ptrunc n (Ω[succ k] A)) :
-    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (tconcat p q) =
-    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝
-    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q :=
-  equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat tconcat
-    (@iterated_loop_ptrunc_pequiv_con n k A) p q
+    (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (tconcat p q) =
+    (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝
+    (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q :=
+  equiv.inv_preserve_binary (loopn_ptrunc_pequiv n (succ k) A) concat tconcat
+    (@loopn_ptrunc_pequiv_con n k A) p q
 
   definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z)
     (f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f :=