diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index aea28999d..4a93d9f29 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -198,7 +198,7 @@ namespace is_equiv
   end
 
   section
-  variables {A B : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B}
+  variables {A B C : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B} {g : B → C} {h : A → C}
   include Hf
 
   --Rewrite rules
@@ -213,6 +213,20 @@ namespace is_equiv
 
   definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b :=
   (inv_eq_of_eq p⁻¹)⁻¹
+
+  variable (f)
+  definition homotopy_of_homotopy_inv' (p : g ~ h ∘ f⁻¹) : g ∘ f ~ h :=
+  λa, p (f a) ⬝ ap h (left_inv f a)
+
+  definition homotopy_of_inv_homotopy' (p : h ∘ f⁻¹ ~ g) : h ~ g ∘ f :=
+  λa, ap h (left_inv f a)⁻¹ ⬝ p (f a)
+
+  definition inv_homotopy_of_homotopy' (p : h ~ g ∘ f) : h ∘ f⁻¹ ~ g :=
+  λb, p (f⁻¹ b) ⬝ ap g (right_inv f b)
+
+  definition homotopy_inv_of_homotopy' (p : g ∘ f ~ h) : g ~ h ∘ f⁻¹  :=
+  λb, ap g (right_inv f b)⁻¹ ⬝ p (f⁻¹ b)
+
   end
 
   --Transporting is an equivalence
@@ -364,6 +378,23 @@ namespace equiv
 
   end
 
+  section
+  variables {A B C : Type} (f : A ≃ B) {a : A} {b : B} {g : B → C} {h : A → C}
+
+  definition homotopy_of_homotopy_inv (p : g ~ h ∘ f⁻¹) : g ∘ f ~ h :=
+  homotopy_of_homotopy_inv' f p
+
+  definition homotopy_of_inv_homotopy (p : h ∘ f⁻¹ ~ g) : h ~ g ∘ f :=
+  homotopy_of_inv_homotopy' f p
+
+  definition inv_homotopy_of_homotopy (p : h ~ g ∘ f) : h ∘ f⁻¹ ~ g :=
+  inv_homotopy_of_homotopy' f p
+
+  definition homotopy_inv_of_homotopy (p : g ∘ f ~ h) : g ~ h ∘ f⁻¹  :=
+  homotopy_inv_of_homotopy' f p
+
+  end
+
 
   namespace ops
     postfix ⁻¹ := equiv.symm -- overloaded notation for inverse
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 32403370d..2c7143aec 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 -/
 
 import arity .eq .bool .unit .sigma .nat.basic prop_trunc
-open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops
+open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops sigma.ops
 
 structure pointed [class] (A : Type) :=
   (point : A)
@@ -301,20 +301,18 @@ namespace pointed
       { esimp, exact !con.left_inv⁻¹}},
   end
 
-  -- set_option pp.notation false
-  -- definition pmap_equiv_right (A : Type*) (B : Type)
-  --   : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) :=
-  -- begin
-  --   fapply equiv.MK,
-  --   { intro u a, cases u with b f, cases f with f p, esimp at f, exact f a},
-  --   { intro f, refine ⟨f pt, _⟩, fapply pmap.mk,
-  --       intro a, esimp, exact f a,
-  --       reflexivity},
-  --   { intro f, reflexivity},
-  --   { intro u, cases u with b f, cases f with f p, esimp at *, apply sigma_eq p,
-  --     esimp, apply sorry
-  --     }
-  -- end
+  definition pmap_equiv_right (A : Type*) (B : Type)
+    : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) :=
+  begin
+    fapply equiv.MK,
+    { intro u a, exact pmap.to_fun u.2 a},
+    { intro f, refine ⟨f pt, _⟩, fapply pmap.mk,
+        intro a, esimp, exact f a,
+        reflexivity},
+    { intro f, reflexivity},
+    { intro u, cases u with b f, cases f with f p, esimp at *, induction p,
+      reflexivity}
+  end
 
   definition pmap_bool_equiv (B : Type*) : (pbool →* B) ≃ B :=
   begin
@@ -377,6 +375,15 @@ namespace pointed
     { reflexivity}
   end
 
+  definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
+  begin
+    fconstructor,
+    { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
+      refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
+      exact !inv_inv⁻¹},
+    { induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
+  end
+
   /- categorical properties of pointed homotopies -/
 
   protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f :=
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index c9ae95362..6b2d12ffd 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 -/
 
 
-import .equiv
+import .equiv cubical.square
 
 open eq is_equiv equiv equiv.ops pointed is_trunc
 
@@ -19,6 +19,9 @@ structure pequiv (A B : Type*) extends equiv A B, pmap A B
 
 namespace pointed
 
+  attribute pequiv._trans_of_to_pmap pequiv._trans_of_to_equiv pequiv.to_pmap pequiv.to_equiv
+            [unfold 3]
+
   variables {A B C : Type*}
 
   /- pointed equivalences -/
@@ -96,4 +99,92 @@ namespace pointed
   infix ` ⬝e*p `:75 := peconcat_eq
   infix ` ⬝pe* `:75 := eq_peconcat
 
+  local attribute pequiv.symm [constructor]
+  definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A :=
+  phomotopy.mk (left_inv f)
+    abstract begin
+      esimp, rewrite ap_inv, symmetry, apply con_inv_cancel_left
+    end end
+
+  definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B :=
+  phomotopy.mk (right_inv f)
+    abstract begin
+      induction f with f H p, esimp,
+      rewrite [ap_con, +ap_inv, -adj f, -ap_compose],
+      note q := natural_square (right_inv f) p,
+      rewrite [ap_id at q],
+      apply eq_bot_of_square,
+      exact transpose q
+    end end
+
+  definition pcancel_left (f : B ≃* C) {g h : A →* B} (p : f ∘* g ~* f ∘* h) : g ~* h :=
+  begin
+    refine _⁻¹* ⬝* pwhisker_left f⁻¹ᵉ* p ⬝* _:
+    refine !passoc⁻¹* ⬝* _:
+    refine pwhisker_right _ (pleft_inv f) ⬝* _:
+    apply pid_comp
+  end
+
+
+  definition pcancel_right (f : A ≃* B) {g h : B →* C} (p : g ∘* f ~* h ∘* f) : g ~* h :=
+  begin
+    refine _⁻¹* ⬝* pwhisker_right f⁻¹ᵉ* p ⬝* _:
+    refine !passoc ⬝* _:
+    refine pwhisker_left _ (pright_inv f) ⬝* _:
+    apply comp_pid
+  end
+
+  definition phomotopy_pinv_right_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C}
+    (p : g ∘* f ~* h) : g ~* h ∘* f⁻¹ᵉ* :=
+  begin
+    refine _ ⬝* pwhisker_right _ p, symmetry,
+    refine !passoc ⬝* _,
+    refine pwhisker_left _ (pright_inv f) ⬝* _,
+    apply comp_pid
+  end
+
+  definition phomotopy_of_pinv_right_phomotopy {f : B ≃* A} {g : B →* C} {h : A →* C}
+    (p : g ∘* f⁻¹ᵉ* ~* h) : g ~* h ∘* f :=
+  begin
+    refine _ ⬝* pwhisker_right _ p, symmetry,
+    refine !passoc ⬝* _,
+    refine pwhisker_left _ (pleft_inv f) ⬝* _,
+    apply comp_pid
+  end
+
+  definition pinv_right_phomotopy_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C}
+    (p : h ~* g ∘* f) : h ∘* f⁻¹ᵉ* ~* g :=
+  (phomotopy_pinv_right_of_phomotopy p⁻¹*)⁻¹*
+
+  definition phomotopy_of_phomotopy_pinv_right {f : B ≃* A} {g : B →* C} {h : A →* C}
+    (p : h ~* g ∘* f⁻¹ᵉ*) : h ∘* f ~* g :=
+  (phomotopy_of_pinv_right_phomotopy p⁻¹*)⁻¹*
+
+  definition phomotopy_pinv_left_of_phomotopy {f : B ≃* C} {g : A →* B} {h : A →* C}
+    (p : f ∘* g ~* h) : g ~* f⁻¹ᵉ* ∘* h :=
+  begin
+    refine _ ⬝* pwhisker_left _ p, symmetry,
+    refine !passoc⁻¹* ⬝* _,
+    refine pwhisker_right _ (pleft_inv f) ⬝* _,
+    apply pid_comp
+  end
+
+  definition phomotopy_of_pinv_left_phomotopy {f : C ≃* B} {g : A →* B} {h : A →* C}
+    (p : f⁻¹ᵉ* ∘* g ~* h) : g ~* f ∘* h :=
+  begin
+    refine _ ⬝* pwhisker_left _ p, symmetry,
+    refine !passoc⁻¹* ⬝* _,
+    refine pwhisker_right _ (pright_inv f) ⬝* _,
+    apply pid_comp
+  end
+
+  definition pinv_left_phomotopy_of_phomotopy {f : B ≃* C} {g : A →* B} {h : A →* C}
+    (p : h ~* f ∘* g) : f⁻¹ᵉ* ∘* h ~* g :=
+  (phomotopy_pinv_left_of_phomotopy p⁻¹*)⁻¹*
+
+
+  definition phomotopy_of_phomotopy_pinv_left {f : C ≃* B} {g : A →* B} {h : A →* C}
+    (p : h ~* f⁻¹ᵉ* ∘* g) : f ∘* h ~* g :=
+  (phomotopy_of_pinv_left_phomotopy p⁻¹*)⁻¹*
+
 end pointed