style(hott): rename instances of pType using pfoo instead of Foo

For example, the pointed suspension operation was called Susp before this commit, but now is called psusp
2016-02-15 18:23:28 -05:00 · 2016-02-15 18:23:28 -05:00 · 087c44d614
commit 087c44d614
parent c64e5a114c
14 changed files with 91 additions and 84 deletions
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@ -73,7 +73,7 @@ namespace eq
  begin
    revert A, induction m with m IH: intro A,
    { reflexivity},
-    { esimp [Iterated_loop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
+    { esimp [iterated_ploop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
      exact ap (Group_homotopy_group n) !loop_space_succ_eq_in⁻¹}
  end

--- a/hott/hit/pointed_pushout.hlean
+++ b/hott/hit/pointed_pushout.hlean
@ -3,7 +3,7 @@ Copyright (c) 2016 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer, Floris van Doorn

-pType Pushouts
+Pointed Pushouts
 -/
 import .pushout types.pointed2

@ -23,20 +23,20 @@ namespace pushout
  section
  parameters {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR)

-  definition Pushout [constructor] : Type* :=
+  definition ppushout [constructor] : Type* :=
  pointed.mk' (pushout f g)

  parameters {f g}
-  definition pinl [constructor] : BL →* Pushout :=
+  definition pinl [constructor] : BL →* ppushout :=
  pmap.mk inl idp

-  definition pinr [constructor] : TR →* Pushout :=
+  definition pinr [constructor] : TR →* ppushout :=
  pmap.mk inr ((ap inr (respect_pt g))⁻¹ ⬝ !glue⁻¹ ⬝ (ap inl (respect_pt f)))

  definition pglue (x : TL) : pinl (f x) = pinr (g x) := -- TODO do we need this?
  !glue

-  definition prec {P : Pushout → Type} (Pinl : Π x, P (pinl x)) (Pinr : Π x, P (pinr x))
+  definition prec {P : ppushout → Type} (Pinl : Π x, P (pinl x)) (Pinr : Π x, P (pinr x))
    (H : Π x, Pinl (f x) =[pglue x] Pinr (g x)) : (Π y, P y) :=
  pushout.rec Pinl Pinr H
  end
@ -44,7 +44,7 @@ namespace pushout
  section
  variables {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR)

-  protected definition psymm [constructor] : Pushout f g ≃* Pushout g f :=
+  protected definition psymm [constructor] : ppushout f g ≃* ppushout g f :=
  begin
    fapply pequiv_of_equiv,
    { apply pushout.symm},
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@ -14,9 +14,9 @@ See also .set_quotient
  * eq_of_rel : Π{a a' : A}, R a a' → class_of a = class_of a' (R explicit)
 -/

-import arity cubical.squareover types.arrow cubical.pathover2
+import arity cubical.squareover types.arrow cubical.pathover2 types.pointed

-open eq equiv sigma sigma.ops equiv.ops pi is_trunc
+open eq equiv sigma sigma.ops equiv.ops pi is_trunc pointed

 namespace quotient

@ -100,6 +100,9 @@ namespace quotient
    end
  end

+  definition pquotient [constructor] {A : Type*} (R : A → A → Type) : Type* :=
+  pType.mk (quotient R) (class_of R pt)
+
  /- the flattening lemma -/

  namespace flattening
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@ -158,11 +158,11 @@ attribute circle.rec_on circle.elim_on [unfold 2]
 attribute circle.elim_type_on [unfold 1]

 namespace circle
-  definition pointed_circle [instance] [constructor] : pointed circle :=
+  definition pointed_circle [instance] [constructor] : pointed S¹ :=
  pointed.mk base

-  definition Circle [constructor] : Type* := pointed.mk' circle
-  notation `S¹.` := Circle
+  definition pcircle [constructor] : Type* := pointed.mk' S¹
+  notation `S¹.` := pcircle

  definition loop_neq_idp : loop ≠ idp :=
  assume H : loop = idp,
--- a/hott/homotopy/cofiber.hlean
+++ b/hott/homotopy/cofiber.hlean
@ -48,28 +48,28 @@ namespace cofiber
  end
 end cofiber

-- pType version
+-- pointed version

-definition Cofiber {A B : Type*} (f : A →* B) : Type* := Pushout (pconst A Unit) f
+definition pcofiber {A B : Type*} (f : A →* B) : Type* := ppushout (pconst A punit) f

 namespace cofiber

-  protected definition prec {A B : Type*} {f : A →* B} {P : Cofiber f → Type}
+  protected definition prec {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
    (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
    (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) :
-    (Π (y : Cofiber f), P y) :=
+    (Π (y : pcofiber f), P y) :=
  begin
    intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
  end

-  protected definition prec_on {A B : Type*} {f : A →* B} {P : Cofiber f → Type}
-    (y : Cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
+  protected definition prec_on {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
+    (y : pcofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
    (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : P y :=
  begin
    induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
  end

-  protected definition pelim_on {A B C : Type*} {f : A →* B} (y : Cofiber f)
+  protected definition pelim_on {A B C : Type*} {f : A →* B} (y : pcofiber f)
    (c : C) (g : B → C) (p : Π x, c = g (f x)) : C :=
  begin
    fapply pushout.elim_on y, exact (λ x, c), exact g, exact p
@ -79,7 +79,7 @@ namespace cofiber

  variables (A : Type*)

-  definition cofiber_unit : Cofiber (pconst A Unit) ≃* Susp A :=
+  definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A :=
  begin
    fapply pequiv_of_pmap,
    { fconstructor, intro x, induction x, exact north, exact south, exact merid x,
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@ -155,10 +155,10 @@ namespace homotopy

  -- as special case we get elimination principles for pointed connected types
  namespace is_conn
-    open pointed pType unit
+    open pointed unit
    section
      parameters {n : trunc_index} {A : Type*}
-                 [H : is_conn n .+1 A] (P : A → n -Type)
+                 [H : is_conn n .+1 A] (P : A → n-Type)

      include H
      protected definition rec : is_equiv (λs : Πa : A, P a, s (Point A)) :=
--- a/hott/homotopy/smash.hlean
+++ b/hott/homotopy/smash.hlean
@ -10,20 +10,20 @@ import hit.pushout .wedge .cofiber .susp .sphere

 open eq pushout prod pointed pType is_trunc

-definition product_of_wedge [constructor] (A B : Type*) : Wedge A B →* A ×* B :=
+definition product_of_wedge [constructor] (A B : Type*) : pwedge A B →* A ×* B :=
 begin
  fconstructor,
  intro x, induction x with [a, b], exact (a, point B), exact (point A, b),
  do 2 reflexivity
 end

-definition Smash (A B : Type*) := Cofiber (product_of_wedge A B)
+definition psmash (A B : Type*) := pcofiber (product_of_wedge A B)

 open sphere susp unit

 namespace smash

-  protected definition prec {X Y : Type*} {P : Smash X Y → Type}
+  protected definition prec {X Y : Type*} {P : psmash X Y → Type}
    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
@ -37,7 +37,7 @@ namespace smash
    induction u, exact pg,
  end

-  protected definition prec_on {X Y : Type*} {P : Smash X Y → Type} (s : Smash X Y)
+  protected definition prec_on {X Y : Type*} {P : psmash X Y → Type} (s : psmash X Y)
    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
@ -46,7 +46,7 @@ namespace smash
          (px (Point X)) (glue ⋆) (py (Point Y))) : P s :=
  smash.prec pxy ps px py pg s

-/-  definition smash_bool (X : Type*) : Smash X Bool ≃* X :=
+/-  definition smash_bool (X : Type*) : psmash X pbool ≃* X :=
  begin
    fconstructor,
    { fconstructor,
@ -74,7 +74,7 @@ namespace smash
          apply inverse, apply concat, apply ap (ap _),
           } } }

-  definition susp_equiv_circle_smash (X : Type*) : Susp X ≃* Smash (Sphere 1) X :=
+  definition susp_equiv_circle_smash (X : Type*) : psusp X ≃* psmash (psphere 1) X :=
  begin
    fconstructor,
    { fconstructor, intro x, induction x, },
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@ -92,11 +92,11 @@ namespace sphere
  definition base {n : ℕ} : sphere n := north
  definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) :=
  pointed.mk base
-  definition Sphere [constructor] (n : ℕ) : pType := pointed.mk' (sphere n)
+  definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n)

  namespace ops
    abbreviation S := sphere
-    notation `S.`:max := Sphere
+    notation `S.` := psphere
  end ops
  open sphere.ops

@ -106,7 +106,7 @@ namespace sphere
  definition surf {n : ℕ} : Ω[n] S. n :=
  nat.rec_on n (proof base qed)
               (begin intro m s, refine cast _ (apn m (equator m) s),
-                      exact ap pType.carrier !loop_space_succ_eq_in⁻¹ end)
+                      exact ap carrier !loop_space_succ_eq_in⁻¹ end)


  definition bool_of_sphere : S 0 → bool :=
@ -125,11 +125,11 @@ namespace sphere
  definition sphere_eq_bool : S 0 = bool :=
  ua sphere_equiv_bool

-  definition sphere_eq_bool_pointed : S. 0 = Bool :=
+  definition sphere_eq_bool_pointed : S. 0 = pbool :=
  pType_eq sphere_equiv_bool idp

  -- TODO: the commented-out part makes the forward function below "apn _ surf"
-  definition pmap_sphere (A : pType) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
+  definition pmap_sphere (A : Type*) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
  begin
    -- fapply equiv_change_fun,
    -- {
@ -143,10 +143,10 @@ namespace sphere
    --   { exact sorry}}
  end

-  protected definition elim {n : ℕ} {P : pType} (p : Ω[n] P) : map₊ (S. n) P :=
+  protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : map₊ (S. n) P :=
  to_inv !pmap_sphere p

-  -- definition elim_surf {n : ℕ} {P : pType} (p : Ω[n] P) : apn n (sphere.elim p) surf = 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},
@ -157,10 +157,6 @@ end sphere

 open sphere sphere.ops

-structure weakly_constant [class] {A B : Type} (f : A → B) := --move
-  (is_weakly_constant : Πa a', f a = f a')
-abbreviation wconst := @weakly_constant.is_weakly_constant
-
 namespace is_trunc
  open trunc_index
  variables {n : ℕ} {A : Type}
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@ -85,10 +85,10 @@ namespace susp
  definition pointed_susp [instance] [constructor] (X : Type) : pointed (susp X) :=
  pointed.mk north

-  definition Susp [constructor] (X : Type) : pType :=
+  definition psusp [constructor] (X : Type) : pType :=
  pointed.mk' (susp X)

-  definition Susp_functor (f : X →* Y) : Susp X →* Susp Y :=
+  definition psusp_functor (f : X →* Y) : psusp X →* psusp Y :=
  begin
    fconstructor,
    { intro x, induction x,
@ -98,21 +98,21 @@ namespace susp
    { reflexivity}
  end

-  definition Susp_functor_compose (g : Y →* Z) (f : X →* Y)
-    : Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f :=
+  definition psusp_functor_compose (g : Y →* Z) (f : X →* Y)
+    : psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f :=
  begin
    fconstructor,
    { intro a, induction a,
      { reflexivity},
      { reflexivity},
      { apply eq_pathover, apply hdeg_square,
-        rewrite [▸*,ap_compose' _ (Susp_functor f),↑Susp_functor,+elim_merid]}},
+        rewrite [▸*,ap_compose' _ (psusp_functor f),↑psusp_functor,+elim_merid]}},
    { reflexivity}
  end

  -- adjunction from Coq-HoTT

-  definition loop_susp_unit [constructor] (X : pType) : X →* Ω(Susp X) :=
+  definition loop_susp_unit [constructor] (X : pType) : X →* Ω(psusp X) :=
  begin
    fconstructor,
    { intro x, exact merid x ⬝ (merid pt)⁻¹},
@ -120,11 +120,11 @@ namespace susp
  end

  definition loop_susp_unit_natural (f : X →* Y)
-    : loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X :=
+    : loop_susp_unit Y ∘* f ~* ap1 (psusp_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,
    fconstructor,
-    { intro x', esimp [Susp_functor], symmetry,
+    { intro x', esimp [psusp_functor], symmetry,
      exact
        !idp_con ⬝
        (!ap_con ⬝
@ -137,11 +137,11 @@ namespace susp
      rewrite inverse2_right_inv,
      refine _ ⬝ !con.assoc',
      rewrite [ap_con_right_inv],
-      unfold Susp_functor,
+      unfold psusp_functor,
      xrewrite [idp_con_idp, -ap_compose (concat idp)]},
  end

-  definition loop_susp_counit [constructor] (X : pType) : Susp (Ω X) →* X :=
+  definition loop_susp_counit [constructor] (X : pType) : psusp (Ω X) →* X :=
  begin
    fconstructor,
    { intro x, induction x, exact pt, exact pt, exact a},
@ -149,7 +149,7 @@ namespace susp
  end

  definition loop_susp_counit_natural (f : X →* Y)
-    : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (Susp_functor (ap1 f)) :=
+    : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (psusp_functor (ap1 f)) :=
  begin
    induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
    fconstructor,
@ -177,7 +177,7 @@ namespace susp
  end

  definition loop_susp_unit_counit (X : pType)
-    : loop_susp_counit (Susp X) ∘* Susp_functor (loop_susp_unit X) ~* pid (Susp X) :=
+    : loop_susp_counit (psusp X) ∘* psusp_functor (loop_susp_unit X) ~* pid (psusp X) :=
  begin
    induction X with X x, fconstructor,
    { intro x', induction x',
@ -193,7 +193,7 @@ namespace susp
  begin
    fapply equiv.MK,
    { intro f, exact ap1 f ∘* loop_susp_unit X},
-    { intro g, exact loop_susp_counit Y ∘* Susp_functor g},
+    { intro g, exact loop_susp_counit Y ∘* psusp_functor g},
    { intro g, apply eq_of_phomotopy, esimp,
      refine !pwhisker_right !ap1_compose ⬝* _,
      refine !passoc ⬝* _,
@ -202,7 +202,7 @@ namespace susp
      refine !pwhisker_right !loop_susp_counit_unit ⬝* _,
      apply pid_comp},
    { intro f, apply eq_of_phomotopy, esimp,
-      refine !pwhisker_left !Susp_functor_compose ⬝* _,
+      refine !pwhisker_left !psusp_functor_compose ⬝* _,
      refine !passoc⁻¹* ⬝* _,
      refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _,
      refine !passoc ⬝* _,
@ -210,7 +210,7 @@ namespace susp
      apply comp_pid},
  end

-  definition susp_adjoint_loop_nat_right (f : Susp X →* Y) (g : Y →* Z)
+  definition susp_adjoint_loop_nat_right (f : psusp X →* Y) (g : Y →* Z)
    : susp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* susp_adjoint_loop X Y f :=
  begin
    esimp [susp_adjoint_loop],
@ -220,12 +220,12 @@ namespace susp
  end

  definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y)
-    : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* Susp_functor g :=
+    : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* psusp_functor g :=
  begin
    esimp [susp_adjoint_loop],
    refine _ ⬝* !passoc⁻¹*,
    apply pwhisker_left,
-    apply Susp_functor_compose
+    apply psusp_functor_compose
  end

 end susp
--- a/hott/homotopy/wedge.hlean
+++ b/hott/homotopy/wedge.hlean
@ -9,12 +9,12 @@ import hit.pointed_pushout .connectedness

 open eq pushout pointed pType unit

-definition Wedge (A B : Type*) : Type* := Pushout (pconst Unit A) (pconst Unit B)
+definition pwedge (A B : Type*) : Type* := ppushout (pconst punit A) (pconst punit B)

 namespace wedge

  -- TODO maybe find a cleaner proof
-  protected definition unit (A : Type*) : A ≃* Wedge Unit A :=
+  protected definition unit (A : Type*) : A ≃* pwedge punit A :=
  begin
    fapply pequiv_of_pmap,
    { fapply pmap.mk, intro a, apply pinr a, apply respect_pt },
--- a/hott/types/lift.hlean
+++ b/hott/types/lift.hlean
@ -7,7 +7,7 @@ Theorems about lift
 -/

 import ..function
-open eq equiv equiv.ops is_equiv is_trunc
+open eq equiv equiv.ops is_equiv is_trunc pointed

 namespace lift

@ -138,6 +138,12 @@ namespace lift
      apply ua_refl}
  end

+  definition plift [constructor] (A : pType.{u}) : pType.{max u v} :=
+  pType.mk (lift A) (up pt)
+
+  definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B :=
+  pmap.mk (lift_functor f) (ap up (respect_pt f))
+
  -- is_trunc_lift is defined in init.trunc


--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@ -6,9 +6,9 @@ Author: Floris van Doorn
 Theorems about the natural numbers specific to HoTT
 -/

-import .order
+import .order types.pointed

-open is_trunc unit empty eq equiv algebra
+open is_trunc unit empty eq equiv algebra pointed

 namespace nat
  definition is_prop_le [instance] (n m : ℕ) : is_prop (n ≤ m) :=
@ -114,4 +114,7 @@ namespace nat
               rewrite [↑nat.decode,↑nat.refl,v_0]
           end

+  definition pointed_nat [instance] [constructor] : pointed ℕ :=
+  pointed.mk 0
+
 end nat
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@ -16,8 +16,6 @@ structure pType :=
  (carrier : Type)
  (Point   : carrier)

-open pType
-
 notation `Type*` := pType

 namespace pointed
@ -25,6 +23,8 @@ namespace pointed
  variables {A B : Type}

  definition pt [unfold 2] [H : pointed A] := point A
+  definition Point [unfold 1] (A : Type*) := pType.Point A
+  definition carrier [unfold 1] (A : Type*) := pType.carrier A
  protected definition Mk [constructor] {A : Type} (a : A) := pType.mk A a
  protected definition MK [constructor] (A : Type) (a : A) := pType.mk A a
  protected definition mk' [constructor] (A : Type) [H : pointed A] : Type* :=
@ -57,29 +57,29 @@ namespace pointed
  definition pointed_bool [instance] [constructor] : pointed bool :=
  pointed.mk ff

-  definition Prod [constructor] (A B : Type*) : Type* :=
+  definition pprod [constructor] (A B : Type*) : Type* :=
  pointed.mk' (A × B)

-  infixr ` ×* `:35 := Prod
+  infixr ` ×* `:35 := pprod

-  definition Bool [constructor] : Type* :=
+  definition pbool [constructor] : Type* :=
  pointed.mk' bool

-  definition Unit [constructor] : Type* :=
+  definition punit [constructor] : Type* :=
  pointed.Mk unit.star

  definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B :=
  pointed.mk (f pt)

-  definition Loop_space [reducible] [constructor] (A : Type*) : Type* :=
+  definition ploop_space [reducible] [constructor] (A : Type*) : Type* :=
  pointed.mk' (point A = point A)

-  definition Iterated_loop_space [unfold 1] [reducible] : ℕ → Type* → Type*
-  | Iterated_loop_space  0    X := X
-  | Iterated_loop_space (n+1) X := Loop_space (Iterated_loop_space n X)
+  definition iterated_ploop_space [unfold 1] [reducible] : ℕ → Type* → Type*
+  | iterated_ploop_space  0    X := X
+  | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X)

-  prefix `Ω`:(max+5) := Loop_space
-  notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A
+  prefix `Ω`:(max+5) := ploop_space
+  notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A

  definition rfln  [constructor] [reducible] {A : Type*} {n : ℕ} : Ω[n] A := pt
  definition refln [constructor] [reducible] (A : Type*) (n : ℕ) : Ω[n] A := pt
@ -106,7 +106,6 @@ namespace pointed
    { intro x, induction x with X x, reflexivity},
  end

-
  definition add_point [constructor] (A : Type) : Type* :=
  pointed.Mk (none : option A)
  postfix `₊`:(max+1) := add_point
@ -121,14 +120,14 @@ namespace pointed
  begin
    induction n with n IH,
    { reflexivity},
-    { exact ap Loop_space IH}
+    { exact ap ploop_space IH}
  end

  definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) :=
  begin
    induction n with n IH,
    { reflexivity},
-    { exact ap Loop_space IH}
+    { exact ap ploop_space IH}
  end

  definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A)  :=
@ -138,9 +137,9 @@ namespace pointed

  /- the equality [loop_space_succ_eq_in] preserves concatenation -/
  theorem loop_space_succ_eq_in_concat {n : ℕ} (p q : Ω[succ (succ n)] A) :
-           transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) (p ⬝ q)
-         = transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) p
-         ⬝ transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) q :=
+           transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) (p ⬝ q)
+         = transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) p
+         ⬝ transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) q :=
  begin
    rewrite [-+tr_compose, ↑function.compose],
    rewrite [+@transport_eq_FlFr_D _ _ _ _ Point Point, +con.assoc], apply whisker_left,
@ -263,7 +262,7 @@ namespace pointed
  --     }
  -- end

-  definition pmap_bool_equiv (B : Type*) : map₊ Bool B ≃ B :=
+  definition pmap_bool_equiv (B : Type*) : map₊ pbool B ≃ B :=
  begin
    fapply equiv.MK,
    { intro f, cases f with f p, exact f tt},
@ -293,7 +292,7 @@ namespace pointed
  begin
  induction n with n IH,
  { exact f},
-  { esimp [Iterated_loop_space], exact ap1 IH}
+  { esimp [iterated_ploop_space], exact ap1 IH}
  end

  definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@ -150,10 +150,10 @@ 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_loop_space], transitivity _,
+    { intro A, esimp [iterated_ploop_space], 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_loop_space],
+    { intro A, esimp [iterated_ploop_space],
      transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor,
      apply pi_iff_pi, intro a, transitivity _, apply IH,
      transitivity _, apply pi_iff_pi, intro p,
@ -165,7 +165,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_loop_space], apply iff.intro,
+    { esimp [sub_two,iterated_ploop_space], 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},