feat(pointed): rename pequiv.MK2 to pequiv.MK, it is the more natural constructor

also move some definitions from pointed or equiv to pointed2 and define transitivity so that it computes

hott/algebra/group_theory.hlean

@@ -179,16 +179,6 @@ namespace group
   isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ))
     begin intros, induction φ, reflexivity end
 
-  definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
-    pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
-  begin
-    induction p,
-    apply pequiv_eq,
-    fapply phomotopy.mk,
-    { intro g, reflexivity },
-    { apply is_prop.elim }
-  end
-
   definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ :=
   homomorphism.mk φ⁻¹
     abstract begin

hott/homotopy/susp.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Ulrik Buchholtz
 Declaration of suspension
 -/
 
-import hit.pushout types.pointed cubical.square .connectedness
+import hit.pushout types.pointed2 cubical.square .connectedness
 
 open pushout unit eq equiv
 

hott/types/equiv.hlean

@@ -306,51 +306,3 @@ namespace equiv
   end
 
 end equiv
-
-namespace pointed
-  open equiv is_equiv pointed prod
-  definition pequiv.sigma_char {A B : Type*} :
-    (A ≃* B) ≃ Σ(f : A →* B), (Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A) :=
-  begin
-    fapply equiv.MK,
-    { intro f, exact ⟨f, (⟨pequiv.to_pinv1 f, pequiv.pright_inv f⟩,
-                          ⟨pequiv.to_pinv2 f, pequiv.pleft_inv f⟩)⟩, },
-    { intro f, exact pequiv.mk' f.1 (pr1 f.2).1 (pr2 f.2).1 (pr1 f.2).2 (pr2 f.2).2 },
-    { intro f, induction f with f v, induction v with hl hr, induction hl, induction hr,
-      reflexivity },
-    { intro f, induction f, reflexivity }
-  end
-
-  variables {A B : Type*}
-  definition is_contr_pright_inv (f : A ≃* B) : is_contr (Σ(g : B →* A), f ∘* g ~* pid B) :=
-  begin
-    fapply is_trunc_equiv_closed,
-      { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
-    fapply is_contr_fiber_of_is_equiv,
-    exact pequiv.to_is_equiv (pequiv_ppcompose_left f)
-  end
-
-  definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) :=
-  begin
-    fapply is_trunc_equiv_closed,
-      { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
-    fapply is_contr_fiber_of_is_equiv,
-    exact pequiv.to_is_equiv (pequiv_ppcompose_right f)
-  end
-
-  definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g :=
-  have Π(f : A →* B), is_prop ((Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A)),
-  begin
-    intro f, apply is_prop_of_imp_is_contr, intro v,
-    let f' := pequiv.sigma_char⁻¹ᵉ ⟨f, v⟩,
-    apply is_trunc_prod, exact is_contr_pright_inv f', exact is_contr_pleft_inv f'
-  end,
-  calc (f = g) ≃ (pequiv.sigma_char f = pequiv.sigma_char g)
-                 : eq_equiv_fn_eq pequiv.sigma_char f g
-          ...  ≃ (f = g :> (A →* B)) : subtype_eq_equiv
-          ...  ≃ (f ~* g) : pmap_eq_equiv f g
-
-  definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g :=
-  (pequiv_eq_equiv f g)⁻¹ᵉ H
-
-end pointed

hott/types/pointed.hlean

@@ -726,7 +726,7 @@ namespace pointed
     is_equiv (pequiv._trans_of_to_pmap f) :=
   pequiv.to_is_equiv f
 
-  protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A)
+  protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A)
     (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B :=
   pequiv.mk' f g g fg gf
 
@@ -752,11 +752,11 @@ namespace pointed
   definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B :=
   pequiv.mk f _ H
 
-  protected definition pequiv.MK [constructor] (f : A →* B) (g : B → A)
+  protected definition pequiv.MK' [constructor] (f : A →* B) (g : B → A)
     (gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B :=
   pequiv.mk f (adjointify f g fg gf) (respect_pt f)
 
-  /- categorical properties of pointed equivalences -/
+  /- reflexivity and symmetry (transitivity is below) -/
 
   protected definition pequiv.refl [refl] [constructor] (A : Type*) : A ≃* A :=
   pequiv.mk' (pid A) (pid A) (pid A) !pid_pcompose !pcompose_pid
@@ -765,36 +765,26 @@ namespace pointed
   pequiv.refl A
 
   protected definition pequiv.symm [symm] [constructor] (f : A ≃* B) : B ≃* A :=
-  pequiv.mk' (pequiv.to_pinv1 f) f f (pleft_inv' f) (pequiv.pright_inv f)
+  pequiv.MK (to_pinv f) f (pequiv.pright_inv f) (pleft_inv' f)
-
-  protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C :=
-  pequiv_of_pmap (g ∘* f) !is_equiv_compose
-
-  definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C :=
-  pequiv_of_pmap (g ∘* f) (is_equiv_compose g f)
 
   postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm
-  infix ` ⬝e* `:75 := pequiv.trans
+
-  infixr ` ∘*ᵉ `:60 := pequiv_compose
+  definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A :=
+  pleft_inv' f
+
+  definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B :=
+  pequiv.pright_inv f
 
   definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f)
     : pequiv.to_pmap (pequiv_of_pmap f H) = f :=
   by reflexivity
 
-  /-
+  definition to_pmap_pequiv_MK [constructor] (f : A →* B) (g : B →* A)
-     A version of pequiv.MK with stronger conditions.
+    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK f g gf fg ~* f :=
-     The advantage of defining a pointed equivalence with this definition is that there is a
-     pointed homotopy between the inverse of the resulting equivalence and the given pointed map g.
-     This is not the case when using `pequiv.MK` (if g is a pointed map),
-     that will only give an ordinary homotopy.
-  -/
-
-  definition to_pmap_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
-    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK2 f g gf fg ~* f :=
   by reflexivity
 
-  definition to_pinv_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
+  definition to_pinv_pequiv_MK [constructor] (f : A →* B) (g : B →* A)
-    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK2 f g gf fg) ~* g :=
+    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK f g gf fg) ~* g :=
   by reflexivity
 
   /- more on pointed equivalences -/
@@ -803,19 +793,12 @@ namespace pointed
     : B a ≃* B a' :=
   pequiv_of_pmap (ptransport B p) !is_equiv_tr
 
-  definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C)
-    : pequiv.to_pmap (f ⬝e* g) = g ∘* f :=
-  by reflexivity
-
-  definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
-  λx, idp
-
   definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B :=
   pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq)
 
   definition pequiv_change_inv [constructor] (f : A ≃* B) (f' : B →* A) (Heq : to_pinv f ~ f')
     : A ≃* B :=
-  pequiv.MK f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq))
+  pequiv.MK' f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq))
 
   definition pequiv_rect' (f : A ≃* B) (P : A → B → Type)
     (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) :=
@@ -827,21 +810,12 @@ namespace pointed
   definition pequiv_of_eq [constructor] {A B : Type*} (p : A = B) : A ≃* B :=
   pequiv_of_pmap (pcast p) !is_equiv_tr
 
-  definition peconcat_eq {A B C : Type*} (p : A ≃* B) (q : B = C) : A ≃* C :=
-  p ⬝e* pequiv_of_eq q
-
-  definition eq_peconcat {A B C : Type*} (p : A = B) (q : B ≃* C) : A ≃* C :=
-  pequiv_of_eq p ⬝e* q
-
   definition eq_of_pequiv {A B : Type*} (p : A ≃* B) : A = B :=
   pType_eq (equiv_of_pequiv p) !respect_pt
 
   definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B :=
   pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end
 
-  infix ` ⬝e*p `:75 := peconcat_eq
-  infix ` ⬝pe* `:75 := eq_peconcat
-
   -- rename pequiv_of_eq_natural
   definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
     {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
@@ -856,12 +830,6 @@ namespace pointed
   -/
 
   /- computation rules of pointed homotopies, possibly combined with pointed equivalences -/
-  definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A :=
-  pleft_inv' f
-
-  definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B :=
-  pequiv.pright_inv f
-
   definition pcancel_left (f : B ≃* C) {g h : A →* B} (p : f ∘* g ~* f ∘* h) : g ~* h :=
   begin
     refine _⁻¹* ⬝* pwhisker_left f⁻¹ᵉ* p ⬝* _:
@@ -952,35 +920,6 @@ namespace pointed
     (p : pid B ~* f ∘* g) : g⁻¹ᵉ* ~* f :=
   (phomotopy_pinv_of_phomotopy_pid' p⁻¹*)⁻¹*
 
-  definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f :=
-  (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹*
-
-  definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* :=
-  phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*)
-
-  postfix [parsing_only] `⁻²*`:(max+10) := pinv2
-
-  definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) :
-    (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* :=
-  begin
-    refine (phomotopy_pinv_of_phomotopy_pid _)⁻¹*,
-    refine !passoc ⬝* _,
-    refine pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose) ⬝* _,
-    apply pright_inv
-  end
-
-  definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) :
-    (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* :=
-  !trans_pinv ⬝* pwhisker_right _ !pinv_pinv
-
-  definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) :
-    (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g :=
-  !trans_pinv ⬝* pwhisker_left _ !pinv_pinv
-
-  definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) :
-    (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g :=
-  !trans_pinv ⬝* !pinv_pinv ◾* !pinv_pinv
-
   definition pinv_pcompose_cancel_left {A B C : Type*} (g : B ≃* C) (f : A →* B) :
     g⁻¹ᵉ* ∘* (g ∘* f) ~* f :=
   !passoc⁻¹* ⬝* pwhisker_right f !pleft_inv ⬝* !pid_pcompose
@@ -997,11 +936,64 @@ namespace pointed
     (g ∘* f) ∘* f⁻¹ᵉ* ~* g :=
   !passoc ⬝* pwhisker_left g !pright_inv ⬝* !pcompose_pid
 
+  definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f :=
+  (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹*
+
+  definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* :=
+  phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*)
+
+  postfix [parsing_only] `⁻²*`:(max+10) := pinv2
+
+  protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C :=
+  pequiv.MK (g ∘* f) (f⁻¹ᵉ* ∘* g⁻¹ᵉ*)
+    abstract !passoc ⬝* pwhisker_left _ (pinv_pcompose_cancel_left g f) ⬝* pleft_inv f end
+    abstract !passoc ⬝* pwhisker_left _ (pcompose_pinv_cancel_left f g⁻¹ᵉ*) ⬝* pright_inv g end
+
+  definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C :=
+  pequiv.trans f g
+
+  infix ` ⬝e* `:75 := pequiv.trans
+  infixr ` ∘*ᵉ `:60 := pequiv_compose
+
+  definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C)
+    : pequiv.to_pmap (f ⬝e* g) = g ∘* f :=
+  by reflexivity
+
+  definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
+  λx, idp
+
+  definition peconcat_eq {A B C : Type*} (p : A ≃* B) (q : B = C) : A ≃* C :=
+  p ⬝e* pequiv_of_eq q
+
+  definition eq_peconcat {A B C : Type*} (p : A = B) (q : B ≃* C) : A ≃* C :=
+  pequiv_of_eq p ⬝e* q
+
+
+  infix ` ⬝e*p `:75 := peconcat_eq
+  infix ` ⬝pe* `:75 := eq_peconcat
+
+
+  definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) :
+    (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* :=
+  by reflexivity
+
+  definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) :
+    (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* :=
+  by reflexivity
+
+  definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) :
+    (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g :=
+  by reflexivity
+
+  definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) :
+    (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g :=
+  by reflexivity
+
   /- pointed equivalences between particular pointed types -/
 
   -- TODO: remove is_equiv_apn, which is proven again here
   definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
-  pequiv.MK2 (apn n f) (apn n f⁻¹ᵉ*)
+  pequiv.MK (apn n f) (apn n f⁻¹ᵉ*)
   abstract begin
     induction n with n IH,
     { apply pleft_inv},
@@ -1153,79 +1145,4 @@ namespace pointed
     apply apn_succ_phomotopy_in
   end
 
-  /- properties of ppmap, the pointed type of pointed maps -/
-  definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
-  phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
-
-  definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
-  phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
-
-  definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
-  pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst 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,
-    { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) },
-    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_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_pcompose f }
-  end
-
-  definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
-  pequiv_of_pmap (ppcompose_left g) _
-
-  definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
-  pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f))
-
-  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 ⬝* !pcompose_pid, },
-    { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _,
-      refine pwhisker_left g !pleft_inv ⬝* !pcompose_pid, },
-  end
-
-  definition loop_ppmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) :=
-    pequiv_of_equiv
-      (calc Ω(ppmap A B) ≃ (pconst A B ~* pconst A B)                       : pmap_eq_equiv _ _
-                     ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char
-                     ... ≃ (A →* Ω B)                                       : pmap.sigma_char)
-      (by reflexivity)
-
-  definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
-  pmap.mk (λ(f : A →* B), f a) idp
-
-  definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
-  pmap.mk (λ(f : A →* B), f a) idp
-
-  definition ppmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B :=
-  begin
-    fapply pequiv.MK,
-    { exact papply B tt },
-    { exact pbool_pmap },
-    { intro f, fapply pmap_eq,
-      { intro b, cases b, exact !respect_pt⁻¹, reflexivity },
-      { exact !con.left_inv⁻¹ }},
-    { intro b, reflexivity },
-  end
-
-  definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) :=
-  pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst)
-
-  definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) :
-    ppmap A B →* Ω[n] B :=
-  papply _ p ∘* papn_pt n A B
-
-
 end pointed

hott/types/pointed2.hlean

@@ -15,10 +15,10 @@ Contains
 
 import algebra.homotopy_group eq2
 
-open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function
+open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool
 
 namespace pointed
-
+  variables {A B C : Type*}
 
   section psquare
   /-
@@ -30,7 +30,7 @@ namespace pointed
     Then the following are operations on squares
   -/
 
-  variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
+  variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
             {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
             {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
             {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
@@ -362,7 +362,7 @@ namespace pointed
     Squares of pointed homotopies
   -/
 
-  variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
+  variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
             {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀}
             {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂}
             {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂}
@@ -549,6 +549,76 @@ namespace pointed
     refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
   end
 
+  /- properties of ppmap, the pointed type of pointed maps -/
+  definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
+  phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
+
+  definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
+  phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
+
+  definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
+  pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst g))
+
+  definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
+  pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f))
+
+  /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/
+  definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
+  pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*)
+    begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end
+    begin intro f, apply eq_of_phomotopy, apply pcompose_pinv_cancel_left end
+  -- pequiv.MK (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*)
+  --   abstract begin
+  --     apply phomotopy_mk_ppmap (pinv_pcompose_cancel_left g), esimp,
+  --     refine !trans_refl ⬝ _,
+  --     refine _ ⬝ (!phomotopy_of_eq_con ⬝ (!phomotopy_of_eq_pcompose_left ⬝
+  --       ap (pwhisker_left _) !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
+
+  --   end end
+  --   abstract begin
+  --     exact sorry
+  --   end end
+
+  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, apply pcompose_pinv_cancel_right },
+    { intro g, apply eq_of_phomotopy, apply pinv_pcompose_cancel_right },
+  end
+
+  definition loop_ppmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) :=
+    pequiv_of_equiv
+      (calc Ω(ppmap A B) ≃ (pconst A B ~* pconst A B)                       : pmap_eq_equiv _ _
+                     ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char
+                     ... ≃ (A →* Ω B)                                       : pmap.sigma_char)
+      (by reflexivity)
+
+  definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
+  pmap.mk (λ(f : A →* B), f a) idp
+
+  definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
+  pmap.mk (λ(f : A →* B), f a) idp
+
+  definition ppmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B :=
+  begin
+    fapply pequiv.MK',
+    { exact papply B tt },
+    { exact pbool_pmap },
+    { intro f, fapply pmap_eq,
+      { intro b, cases b, exact !respect_pt⁻¹, reflexivity },
+      { exact !con.left_inv⁻¹ }},
+    { intro b, reflexivity },
+  end
+
+  definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) :=
+  pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst)
+
+  definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) :
+    ppmap A B →* Ω[n] B :=
+  papply _ p ∘* papn_pt n A B
+
   definition pconst_pcompose_pconst (A B C : Type*) :
     pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) :=
   idp
@@ -688,7 +758,7 @@ namespace pointed
 
   section psquare
 
-  variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
+  variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
             {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
             {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
             {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
@@ -844,4 +914,59 @@ namespace pointed
       apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ }
   end
 
+  open sigma.ops prod
+  definition pequiv.sigma_char {A B : Type*} :
+    (A ≃* B) ≃ Σ(f : A →* B), (Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A) :=
+  begin
+    fapply equiv.MK,
+    { intro f, exact ⟨f, (⟨pequiv.to_pinv1 f, pequiv.pright_inv f⟩,
+                          ⟨pequiv.to_pinv2 f, pequiv.pleft_inv f⟩)⟩, },
+    { intro f, exact pequiv.mk' f.1 (pr1 f.2).1 (pr2 f.2).1 (pr1 f.2).2 (pr2 f.2).2 },
+    { intro f, induction f with f v, induction v with hl hr, induction hl, induction hr,
+      reflexivity },
+    { intro f, induction f, reflexivity }
+  end
+
+  definition is_contr_pright_inv (f : A ≃* B) : is_contr (Σ(g : B →* A), f ∘* g ~* pid B) :=
+  begin
+    fapply is_trunc_equiv_closed,
+      { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
+    fapply is_contr_fiber_of_is_equiv,
+    exact pequiv.to_is_equiv (pequiv_ppcompose_left f)
+  end
+
+  definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) :=
+  begin
+    fapply is_trunc_equiv_closed,
+      { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
+    fapply is_contr_fiber_of_is_equiv,
+    exact pequiv.to_is_equiv (pequiv_ppcompose_right f)
+  end
+
+  definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g :=
+  have Π(f : A →* B), is_prop ((Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A)),
+  begin
+    intro f, apply is_prop_of_imp_is_contr, intro v,
+    let f' := pequiv.sigma_char⁻¹ᵉ ⟨f, v⟩,
+    apply is_trunc_prod, exact is_contr_pright_inv f', exact is_contr_pleft_inv f'
+  end,
+  calc (f = g) ≃ (pequiv.sigma_char f = pequiv.sigma_char g)
+                 : eq_equiv_fn_eq pequiv.sigma_char f g
+          ...  ≃ (f = g :> (A →* B)) : subtype_eq_equiv
+          ...  ≃ (f ~* g) : pmap_eq_equiv f g
+
+  definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g :=
+  (pequiv_eq_equiv f g)⁻¹ᵉ H
+
+  open algebra
+  definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
+    pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
+  begin
+    induction p,
+    apply pequiv_eq,
+    fapply phomotopy.mk,
+    { intro g, reflexivity },
+    { apply is_prop.elim }
+  end
+
 end pointed