Merge branch 'master' of https://github.com/cmu-phil/Spectral

algebra/arrow_group.hlean

@@ -3,7 +3,7 @@
 
 --author: Floris van Doorn
 
-import algebra.group_theory ..pointed ..pointed_pi eq2
+import algebra.group_theory ..pointed ..pointed_pi eq2 homotopy.susp
 open pi pointed algebra group eq equiv is_trunc trunc susp
 namespace group
 
@@ -21,7 +21,7 @@ namespace group
   definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
     Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro p, esimp,
       refine ap1_gen_con_left (respect_pt f) (respect_pt f)
                (respect_pt g) (respect_pt g) p ⬝ _,
@@ -38,7 +38,7 @@ namespace group
   definition pmap_mul_pcompose {A B C : Type*} (g h : B →* Ω C) (f : A →* B) :
     pmap_mul g h ∘* f ~* pmap_mul (g ∘* f) (h ∘* f) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro p, reflexivity },
     { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _,
       refine !ap_eq_ap011⁻¹ }
@@ -47,7 +47,7 @@ namespace group
   definition pcompose_pmap_mul {A B C : Type*} (h : B →* C) (f g : A →* Ω B) :
     Ω→ h ∘* pmap_mul f g ~* pmap_mul (Ω→ h ∘* f) (Ω→ h ∘* g) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro p, exact ap1_con h (f p) (g p) },
     { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _,
       refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _,
@@ -203,20 +203,20 @@ namespace group
   begin
     fapply inf_group.mk,
     { exact ppi_mul },
-    { intro f g h, fapply ppi_eq,
+    { intro f g h, apply ppi_eq, fapply ppi_homotopy.mk,
       { intro a, exact con.assoc (f a) (g a) (h a) },
-      { rexact eq_of_square (con2_assoc (ppi_resp_pt f) (ppi_resp_pt g) (ppi_resp_pt h)) }},
+      { symmetry, rexact eq_of_square (con2_assoc (ppi_resp_pt f) (ppi_resp_pt g) (ppi_resp_pt h)) }},
     { apply ppi_const },
-    { intros f, fapply ppi_eq,
+    { intros f, apply ppi_eq, fapply ppi_homotopy.mk,
       { intro a, exact one_mul (f a) },
-      { esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
+      { symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
-    { intros f, fapply ppi_eq,
+    { intros f, apply ppi_eq, fapply ppi_homotopy.mk,
       { intro a, exact mul_one (f a) },
       { reflexivity }},
     { exact ppi_inv },
-    { intro f, fapply ppi_eq,
+    { intro f, apply ppi_eq, fapply ppi_homotopy.mk,
       { intro a, exact con.left_inv (f a) },
-      { exact !con_left_inv_idp⁻¹ }},
+      { exact !con_left_inv_idp }},
   end
 
   definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
@@ -230,9 +230,9 @@ namespace group
     ab_inf_group (Π*a, Ω (Ω (B a))) :=
   ⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm :=
     begin
-      intro f g, fapply ppi_eq,
+      intro f g, apply ppi_eq, fapply ppi_homotopy.mk,
       { intro a, exact eckmann_hilton (f a) (g a) },
-      { rexact eq_of_square (eckmann_hilton_con2 (ppi_resp_pt f) (ppi_resp_pt g)) }
+      { symmetry, rexact eq_of_square (eckmann_hilton_con2 (ppi_resp_pt f) (ppi_resp_pt g)) }
     end⦄
 
   definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :

homotopy/EM.hlean

@@ -1,10 +1,11 @@
 -- Authors: Floris van Doorn
 
 import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
+       ..move_to_lib
 
 open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
 
-/- TODO: try to fix up this file -/
+/- TODO: try to fix the speed of this file -/
 
 namespace EM
 

homotopy/fwedge.hlean

@@ -107,7 +107,7 @@ namespace fwedge
   definition fwedge_pmap_beta [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) (i : I) :
     fwedge_pmap f ∘* pinl i ~* f i :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { reflexivity },
     { exact !idp_con ⬝ !fwedge.elim_glue⁻¹ }
   end
@@ -115,7 +115,7 @@ namespace fwedge
   definition fwedge_pmap_eta [constructor] {I : Type} {F : I → Type*} {X : Type*} (g : ⋁F →* X) :
     fwedge_pmap (λi, g ∘* pinl i) ~* g :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro x, induction x,
         reflexivity,
         exact (respect_pt g)⁻¹,
@@ -125,7 +125,7 @@ namespace fwedge
 
   definition fwedge_pmap_pinl [constructor] {I : Type} {F : I → Type*} : fwedge_pmap (λi, pinl i) ~* pid (⋁ F) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro x, induction x,
         reflexivity, reflexivity,
         apply eq_pathover, apply hdeg_square, refine !elim_glue ⬝ !ap_id⁻¹ },
@@ -143,14 +143,14 @@ namespace fwedge
   end
 
   definition fwedge_pmap_nat₂ {I : Type}(F : I → Type*){X Y : Type*}
-                              (f : X →* Y) (h : Πi, F i →* X) (w : fwedge F) : 
+                              (f : X →* Y) (h : Πi, F i →* X) (w : fwedge F) :
              (f ∘* (fwedge_pmap h)) w = fwedge_pmap (λi, f ∘* (h i)) w :=
   begin
       induction w, reflexivity,
       refine !respect_pt,
       apply eq_pathover,
       refine ap_compose f (fwedge_pmap h) _ ⬝ph _,
-      refine ap (ap f) !elim_glue ⬝ph _, 
+      refine ap (ap f) !elim_glue ⬝ph _,
       refine _ ⬝hp !elim_glue⁻¹, esimp,
       apply whisker_br,
       apply !hrefl

homotopy/smash.hlean

@@ -185,7 +185,7 @@ namespace smash
   !ap_con ⬝ whisker_left _ !ap_inv ⬝ !functor_gluer2 ◾ !functor_gluer2⁻²
 
   lemma functor_gluel'2_same {C D : Type} (f : A → C) (g : B → D) (a : A) :
-    functor_gluel'2 f (pmap_of_map g pt) a a =
+    functor_gluel'2 f g a a =
     ap02 (pmap_of_map f pt ∧→ pmap_of_map g pt) (con.right_inv (gluel a)) ⬝
     (con.right_inv (gluel (f a)))⁻¹ :=
   begin
@@ -557,11 +557,14 @@ namespace smash
       exact smash_functor_pcompose_pconst_homotopy a₀ b₀ d₀ f' f g x, },
     { refine _ ⬝ !idp_con⁻¹,
       refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl_hconcat_eq) ⬝ _,
-      refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, esimp,
+      refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con,
-      refine whisker_right _ !functor_gluel'2_same ⬝ _,
+      refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluel'2_same f' g (f a₀),
       refine !inv_con_cancel_right ⬝ _,
-      refine _ ⬝ idp ◾ ap (whisker_left _) (!idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con)⁻¹,
+      exact sorry, -- TODO: FIX, the proof below should work
-      symmetry, apply whisker_left_idp }
+      -- refine _ ⬝ whisker_left _ _,
+      -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con,
+      -- symmetry, apply whisker_left_idp
+      }
   end
 
   /- a version where the left maps are identities -/

homotopy/smash_adjoint.hlean

@@ -2,7 +2,7 @@
 -- in collaboration with Egbert, Stefano, Robin, Ulrik
 
 /- the adjunction between the smash product and pointed maps -/
-import .smash .susp ..pointed
+import .smash .susp ..pointed ..move_to_lib
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function unit sigma susp sphere
@@ -29,7 +29,7 @@ namespace smash
   definition smash_pmap_unit_pt [constructor] (A B : Type*)
     : pinl A pt ~* pconst A (A ∧ B) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro a, exact gluel' a pt },
     { rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ }
   end
@@ -70,6 +70,7 @@ namespace smash
       rotate 1, rexact (functor_gluel'2_same (pid A) f pt),
       refine whisker_right _ !idp_con ⬝pv _,
       refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl,
+      refine whisker_left _ !to_homotopy_pt_mk ⬝pv _,
       refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _,
       rotate 1, esimp, apply whisker_left_idp_con,
       refine !con.assoc ⬝pv _, apply whisker_tl,
@@ -174,7 +175,7 @@ namespace smash
   definition smash_pmap_unit_counit (A B : Type*) :
     smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro x,
       induction x with a b a b,
       { reflexivity },
@@ -197,7 +198,7 @@ namespace smash
   definition smash_pmap_counit_unit_pt [constructor] (f : A →* B) :
     smash_pmap_counit A B ∘* pinl A f ~* f :=
   begin
-    fconstructor,
+    fapply phomotopy.mk,
     { intro a, reflexivity },
     { refine !idp_con ⬝ !elim_gluer'⁻¹ }
   end

move_to_lib.hlean

@@ -1,6 +1,7 @@
 -- definitions, theorems and attributes which should be moved to files in the HoTT library
 
-import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint
+import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2
+       .homotopy.susp
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
      is_trunc function sphere unit prod bool
@@ -650,6 +651,10 @@ definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop
 pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
 
 namespace pointed
+  definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g)
+    (p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p :=
+  to_right_inv !eq_con_inv_equiv_con_eq p
+
   variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
             {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
             {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}

pointed_pi.hlean

@@ -1,63 +1,77 @@
 /-
 Copyright (c) 2016 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ulrik Buchholtz
+Authors: Ulrik Buchholtz, Floris van Doorn
 -/
 
-import .move_to_lib
+import homotopy.connectedness types.pointed2
 
 open eq pointed equiv sigma is_equiv
 
 /-
-  The goal of this file is to give the truncation level
+  In this file we define dependent pointed maps and properties of them.
+
+  Using this, we give the truncation level
   of the type of pointed maps, giving the connectivity of
   the domain and the truncation level of the codomain.
   This is is_trunc_pmap_of_is_conn at the end.
 
-  First we define the type of dependent pointed maps
+  We also prove other properties about pointed (dependent maps), like the fact that
-  as a tool, because these appear in the more general
+  (Π*a, F a) → (Π*a, X a) → (Π*a, B a)
-  statement is_trunc_ppi (the generality needed for induction).
+  is a fibration sequence if (F a) → (X a) → B a) is.
-
 -/
 
 namespace pointed
 
+  definition pointed_respect_pt [instance] [constructor] {A B : Type*} (f : A →* B) :
+    pointed (f pt = pt) :=
+  pointed.mk (respect_pt f)
+
+  definition ppi_gen_of_phomotopy [constructor] {A B : Type*} {f g : A →* B} (h : f ~* g) :
+    ppi_gen (λx, f x = g x) (respect_pt f ⬝ (respect_pt g)⁻¹) :=
+  h
+
   abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt
 
-  definition ppi_const [constructor] {A : Type*} (P : A → Type*) : Π*(a : A), P a :=
+  definition ppi_const [constructor] {A : Type*} (P : A → Type*) : ppi P :=
   ppi.mk (λa, pt) idp
 
   definition pointed_ppi [instance] [constructor] {A : Type*}
-    (P : A → Type*) : pointed (ppi A P) :=
+    (P : A → Type*) : pointed (ppi P) :=
   pointed.mk (ppi_const P)
 
   definition pppi [constructor] {A : Type*} (P : A → Type*) : Type* :=
-  pointed.mk' (ppi A P)
+  pointed.mk' (ppi P)
 
   notation `Π*` binders `, ` r:(scoped P, pppi P) := r
 
-  structure ppi_homotopy {A : Type*} {P : A → Type*} (f g : Π*(a : A), P a) :=
+  definition ppi_homotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi_gen P x) : Type :=
-    (homotopy : f ~ g)
+  ppi_gen (λa, f a = g a) (ppi_gen.resp_pt f ⬝ (ppi_gen.resp_pt g)⁻¹)
-    (homotopy_pt : homotopy pt ⬝ ppi_resp_pt g = ppi_resp_pt f)
 
-  variables {A : Type*} {P Q R : A → Type*} {f g h : Π*(a : A), P a}
+  variables {A : Type*} {P Q R : A → Type*} {f g h : Π*a, P a}
+                        {B : A → Type} {x₀ : B pt} {k l m : ppi_gen B x₀}
 
   infix ` ~~* `:50 := ppi_homotopy
-  abbreviation ppi_to_homotopy_pt [unfold 5] := @ppi_homotopy.homotopy_pt
-  abbreviation ppi_to_homotopy [coercion] [unfold 5] (p : f ~~* g) : Πa, f a = g a :=
-  ppi_homotopy.homotopy p
 
-  variable (f)
+  definition ppi_homotopy.mk [constructor] [reducible] (h : k ~ l)
-  protected definition ppi_homotopy.refl : f ~~* f :=
+    (p : h pt ⬝ ppi_gen.resp_pt l = ppi_gen.resp_pt k) : k ~~* l :=
+  ppi_gen.mk h (eq_con_inv_of_con_eq p)
+  definition ppi_to_homotopy [coercion] [unfold 6] [reducible] (p : k ~~* l) : Πa, k a = l a := p
+  definition ppi_to_homotopy_pt [unfold 6] [reducible] (p : k ~~* l) :
+    p pt ⬝ ppi_gen.resp_pt l = ppi_gen.resp_pt k :=
+  con_eq_of_eq_con_inv (ppi_gen.resp_pt p)
+
+  variable (k)
+  protected definition ppi_homotopy.refl : k ~~* k :=
   sorry
-  variable {f}
+  variable {k}
-  protected definition ppi_homotopy.rfl [refl] : f ~~* f :=
+  protected definition ppi_homotopy.rfl [refl] : k ~~* k :=
-  ppi_homotopy.refl f
+  ppi_homotopy.refl k
 
-  protected definition ppi_homotopy.symm [symm] (p : f ~~* g) : g ~~* f :=
+  protected definition ppi_homotopy.symm [symm] (p : k ~~* l) : l ~~* k :=
   sorry
 
-  protected definition ppi_homotopy.trans [trans] (p : f ~~* g) (q : g ~~* h) : f ~~* h :=
+  protected definition ppi_homotopy.trans [trans] (p : k ~~* l) (q : l ~~* m) : k ~~* m :=
   sorry
 
   infix ` ⬝*' `:75 := ppi_homotopy.trans
@@ -66,90 +80,118 @@ namespace pointed
   definition ppi_equiv_pmap (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) :=
   begin
     fapply equiv.MK,
-    { intro f, induction f with f p, exact pmap.mk f p },
+    { intro k, induction k with k p, exact pmap.mk k p },
-    { intro f, induction f with f p, exact ppi.mk f p },
+    { intro k, induction k with k p, exact ppi.mk k p },
-    { intro f, induction f with f p, reflexivity },
+    { intro k, induction k with k p, reflexivity },
-    { intro f, induction f with f p, reflexivity }
+    { intro k, induction k with k p, reflexivity }
   end
 
-  definition ppi.sigma_char [constructor] {A : Type*} (P : A → Type*)
+  definition pppi_pequiv_ppmap (A B : Type*) : (Π*(a : A), B) ≃* ppmap A B :=
-    : (Π*(a : A), P a) ≃ Σ(f : (Π (a : A), P a)), f pt = pt :=
+  pequiv_of_equiv (ppi_equiv_pmap A B) idp
+
+  definition ppi.sigma_char [constructor] {A : Type*} (B : A → Type*)
+    : (Π*(a : A), B a) ≃ Σ(k : (Π (a : A), B a)), k pt = pt :=
   begin
-    fapply equiv.MK : intros f,
+    fapply equiv.MK : intros k,
-    { exact ⟨ f , ppi_resp_pt f ⟩ },
+    { exact ⟨ k , ppi_resp_pt k ⟩ },
-    all_goals cases f with f p,
+    all_goals cases k with k p,
-    { exact ppi.mk f p },
+    { exact ppi.mk k p },
     all_goals reflexivity
   end
 
-  -- the same as pmap_eq
+  protected definition ppi_gen.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) :
-  definition ppi_eq (h : f ~ g) : ppi_resp_pt f = h pt ⬝ ppi_resp_pt g → f = g :=
+    ppi_gen B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ :=
   begin
-    cases f with f p, cases g with g q, intro r,
+    fapply equiv.MK: intro x,
-    esimp at *,
+    { constructor, exact ppi_gen.resp_pt x },
-    fapply apd011 ppi.mk,
+    { induction x, constructor, assumption },
-    { apply eq_of_homotopy h },
+    { induction x, reflexivity },
-    { esimp, apply concato_eq, apply eq_pathover_Fl, apply inv_con_eq_of_eq_con,
+    { induction x, reflexivity }
-      rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r }
   end
 
-  variables (f g)
+  variables (k l)
+
+  definition ppi_homotopy.rec' [recursor] (B : k ~~* l → Type)
+    (H : Π(h : k ~ l) (p : h pt ⬝ ppi_gen.resp_pt l = ppi_gen.resp_pt k), B (ppi_homotopy.mk h p))
+    (h : k ~~* l) : B h :=
+  begin
+    induction h with h p,
+    refine transport (λp, B (ppi_gen.mk h p)) _ (H h (con_eq_of_eq_con_inv p)),
+    apply to_left_inv !eq_con_inv_equiv_con_eq p
+  end
 
   definition ppi_homotopy.sigma_char [constructor]
-    : (f ~~* g) ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f :=
+    : (k ~~* l) ≃ Σ(p : k ~ l), p pt ⬝ ppi_gen.resp_pt l = ppi_gen.resp_pt k :=
   begin
     fapply equiv.MK : intros h,
     { exact ⟨h , ppi_to_homotopy_pt h⟩ },
-    all_goals cases h with h p,
+    { cases h with h p, exact ppi_homotopy.mk h p },
-    { exact ppi_homotopy.mk h p },
+    { cases h with h p, exact ap (dpair h) (to_right_inv !eq_con_inv_equiv_con_eq p) },
-    all_goals reflexivity
+    { induction h using ppi_homotopy.rec' with h p,
+      exact ap (ppi_homotopy.mk h) (to_right_inv !eq_con_inv_equiv_con_eq p) }
   end
 
   -- the same as pmap_eq_equiv
-  definition ppi_eq_equiv : (f = g) ≃ (f ~~* g) :=
+  definition ppi_eq_equiv : (k = l) ≃ (k ~~* l) :=
-    calc (f = g) ≃ ppi.sigma_char P f = ppi.sigma_char P g
+    calc (k = l) ≃ ppi_gen.sigma_char B x₀ k = ppi_gen.sigma_char B x₀ l
-                   : eq_equiv_fn_eq (ppi.sigma_char P) f g
+                   : eq_equiv_fn_eq (ppi_gen.sigma_char B x₀) k l
-            ...  ≃ Σ(p : f = g),
+            ...  ≃ Σ(p : k = l),
-                     pathover (λh, h pt = pt) (ppi_resp_pt f) p (ppi_resp_pt g)
+                     pathover (λh, h pt = x₀) (ppi_gen.resp_pt k) p (ppi_gen.resp_pt l)
                    : sigma_eq_equiv _ _
-            ...  ≃ Σ(p : f = g),
+            ...  ≃ Σ(p : k = l),
-                     ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g
+                     ppi_gen.resp_pt k = ap (λh, h pt) p ⬝ ppi_gen.resp_pt l
                    : sigma_equiv_sigma_right
-                       (λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g))
+                       (λp, eq_pathover_equiv_Fl p (ppi_gen.resp_pt k) (ppi_gen.resp_pt l))
-            ...  ≃ Σ(p : f = g),
+            ...  ≃ Σ(p : k = l),
-                     ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g
+                     ppi_gen.resp_pt k = apd10 p pt ⬝ ppi_gen.resp_pt l
                    : sigma_equiv_sigma_right
                        (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
-            ...  ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g
+            ...  ≃ Σ(p : k ~ l), ppi_gen.resp_pt k = p pt ⬝ ppi_gen.resp_pt l
                    : sigma_equiv_sigma_left' eq_equiv_homotopy
-            ...  ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f
+            ...  ≃ Σ(p : k ~ l), p pt ⬝ ppi_gen.resp_pt l = ppi_gen.resp_pt k
                    : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
-            ...  ≃ (f ~~* g) : ppi_homotopy.sigma_char f g
+            ...  ≃ (k ~~* l) : ppi_homotopy.sigma_char k l
 
-  definition ppi_loop_equiv_lemma (p : f ~ f)
+
-    : (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f) ≃ (p pt = idp) :=
+  variables
-    calc (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f)
+  -- the same as pmap_eq
-      ≃ (p pt ⬝ ppi_resp_pt f = idp ⬝ ppi_resp_pt f)
+  variables {k l}
-        : equiv_eq_closed_right (p pt ⬝ ppi_resp_pt f) (inverse (idp_con (ppi_resp_pt f)))
+  definition ppi_eq (h : k ~~* l) : k = l :=
+  (ppi_eq_equiv k l)⁻¹ᵉ h
+
+  definition eq_of_ppi_homotopy (h : k ~~* l) : k = l := ppi_eq h
+
+  definition ppi_homotopy_of_eq (p : k = l) : k ~~* l := ppi_eq_equiv k l p
+
+  definition ppi_homotopy_of_eq_of_ppi_homotopy (h : k ~~* l) :
+    ppi_homotopy_of_eq (eq_of_ppi_homotopy h) = h :=
+  to_right_inv (ppi_eq_equiv k l) h
+
+  definition ppi_loop_equiv_lemma (p : k ~ k)
+    : (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k) ≃ (p pt = idp) :=
+    calc (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k)
+      ≃ (p pt ⬝ ppi_gen.resp_pt k = idp ⬝ ppi_gen.resp_pt k)
+        : equiv_eq_closed_right (p pt ⬝ ppi_gen.resp_pt k) (inverse (idp_con (ppi_gen.resp_pt k)))
   ... ≃ (p pt = idp)
         : eq_equiv_con_eq_con_right
 
-  definition ppi_loop_equiv : (f = f) ≃ Π*(a : A), Ω (pType.mk (P a) (f a)) :=
+  variables (k l)
-    calc (f = f) ≃ (f ~~* f)
+  definition ppi_loop_equiv : (k = k) ≃ Π*(a : A), Ω (pType.mk (B a) (k a)) :=
+    calc (k = k) ≃ (k ~~* k)
                    : ppi_eq_equiv
-             ... ≃ Σ(p : f ~ f), p pt ⬝ ppi_resp_pt f = ppi_resp_pt f
+             ... ≃ Σ(p : k ~ k), p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k
-                   : ppi_homotopy.sigma_char f f
+                   : ppi_homotopy.sigma_char k k
-             ... ≃ Σ(p : f ~ f), p pt = idp
+             ... ≃ Σ(p : k ~ k), p pt = idp
                    : sigma_equiv_sigma_right
-                       (λ p, ppi_loop_equiv_lemma f p)
+                       (λ p, ppi_loop_equiv_lemma p)
-             ... ≃ Π*(a : A), pType.mk (f a = f a) idp
+             ... ≃ Π*(a : A), pType.mk (k a = k a) idp
                    : ppi.sigma_char
-             ... ≃ Π*(a : A), Ω (pType.mk (P a) (f a))
+             ... ≃ Π*(a : A), Ω (pType.mk (B a) (k a))
                    : erfl
 
-  variables {f g}
+  variables {k l}
-  definition eq_of_ppi_homotopy (h : f ~~* g) : f = g :=
+  -- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l :=
-  (ppi_eq_equiv f g)⁻¹ᵉ h
+  -- (ppi_eq_equiv k l)⁻¹ᵉ h
 
   definition ppi_loop_pequiv : Ω (Π*(a : A), P a) ≃* Π*(a : A), Ω (P a) :=
   pequiv_of_equiv (ppi_loop_equiv pt) idp
@@ -168,7 +210,7 @@ namespace pointed
 
   definition ppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
     (Π*(a : A), P a) →* Π*(a : A), Q a :=
-  pmap.mk (pmap_compose_ppi g) (eq_of_ppi_homotopy (pmap_compose_ppi_const_right g))
+  pmap.mk (pmap_compose_ppi g) (ppi_eq (pmap_compose_ppi_const_right g))
 
   definition pmap_compose_ppi_phomotopy_left [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
     (f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~~* pmap_compose_ppi g' f :=
@@ -188,20 +230,187 @@ namespace pointed
   begin
     apply pequiv_of_pmap (ppi_compose_left g),
     apply adjointify _ (ppi_compose_left (λa, (g a)⁻¹ᵉ*)),
-    { intro f, apply eq_of_ppi_homotopy,
+    { intro f, apply ppi_eq,
       refine !pmap_compose_pmap_compose_ppi ⬝*' _,
       refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _,
       apply pmap_compose_ppi_pid_left },
-    { intro f, apply eq_of_ppi_homotopy,
+    { intro f, apply ppi_eq,
       refine !pmap_compose_pmap_compose_ppi ⬝*' _,
       refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _,
       apply pmap_compose_ppi_pid_left }
   end
 
+  definition psigma_gen [constructor] {A : Type*} (P : A → Type) (x : P pt) : Type* :=
+  pointed.MK (Σa, P a) ⟨pt, x⟩
+
+end pointed
+open fiber function
+namespace pointed
+
+  variables {A B C : Type*}
+
+  -- TODO: replace in types.fiber
+  definition pfiber.sigma_char' (f : A →* B) :
+    pfiber f ≃* psigma_gen (λa, f a = pt) (respect_pt f) :=
+  pequiv_of_equiv (fiber.sigma_char f pt) idp
+
+  /- the pointed type of unpointed (nondependent) maps -/
+  definition parrow [constructor] (A : Type) (B : Type*) : Type* :=
+  pointed.MK (A → B) (const A pt)
+
+  /- the pointed type of unpointed dependent maps -/
+  definition p_pi [constructor] {A : Type} (B : A → Type*) : Type* :=
+  pointed.MK (Πa, B a) (λa, pt)
+
+  definition ppmap.sigma_char (A B : Type*) :
+    ppmap A B ≃* @psigma_gen (parrow A B) (λf, f pt = pt) idp :=
+  pequiv_of_equiv pmap.sigma_char idp
+
+  definition pppi.sigma_char {A : Type*} {B : A → Type*} :
+    (Π*(a : A), B a) ≃* @psigma_gen (p_pi B) (λf, f pt = pt) idp :=
+  proof pequiv_of_equiv !ppi.sigma_char idp qed
+
+  definition psigma_gen_pequiv_psigma_gen_right {A : Type*} {B B' : A → Type}
+    {b : B pt} {b' : B' pt} (f : Πa, B a ≃ B' a) (p : f pt b = b') :
+    psigma_gen B b ≃* psigma_gen B' b' :=
+  pequiv_of_equiv (sigma_equiv_sigma_right f) (ap (dpair pt) p)
+
+  definition psigma_gen_pequiv_psigma_gen_basepoint {A : Type*} {B : A → Type} {b b' : B pt}
+    (p : b = b') : psigma_gen B b ≃* psigma_gen B b' :=
+  psigma_gen_pequiv_psigma_gen_right (λa, erfl) p
+
+  definition ppi_gen_functor_right [constructor] {A : Type*} {B B' : A → Type}
+    {b : B pt} {b' : B' pt} (f : Πa, B a → B' a) (p : f pt b = b') (g : ppi_gen B b)
+    : ppi_gen B' b' :=
+  ppi_gen.mk (λa, f a (g a)) (ap (f pt) (ppi_gen.resp_pt g) ⬝ p)
+
+  definition ppi_gen_functor_right_compose [constructor] {A : Type*} {B₁ B₂ B₃ : A → Type}
+    {b₁ : B₁ pt} {b₂ : B₂ pt} {b₃ : B₃ pt} (f₂ : Πa, B₂ a → B₃ a) (p₂ : f₂ pt b₂ = b₃)
+    (f₁ : Πa, B₁ a → B₂ a) (p₁ : f₁ pt b₁ = b₂)
+    (g : ppi_gen B₁ b₁) : ppi_gen_functor_right (λa, f₂ a ∘ f₁ a) (ap (f₂ pt) p₁ ⬝ p₂) g ~~*
+    ppi_gen_functor_right f₂ p₂ (ppi_gen_functor_right f₁ p₁ g) :=
+  begin
+    fapply ppi_homotopy.mk,
+    { reflexivity },
+    { induction p₁, induction p₂, exact !idp_con ⬝ !ap_compose⁻¹ }
+  end
+
+  definition ppi_gen_functor_right_id [constructor] {A : Type*} {B : A → Type}
+    {b : B pt} (g : ppi_gen B b) : ppi_gen_functor_right (λa, id) idp g ~~* g :=
+  begin
+    fapply ppi_homotopy.mk,
+    { reflexivity },
+    { reflexivity }
+  end
+
+  definition ppi_gen_functor_right_homotopy [constructor] {A : Type*} {B B' : A → Type}
+    {b : B pt} {b' : B' pt} {f f' : Πa, B a → B' a} {p : f pt b = b'} {p' : f' pt b = b'}
+    (h : f ~2 f') (q : h pt b ⬝ p' = p) (g : ppi_gen B b) :
+    ppi_gen_functor_right f p g ~~* ppi_gen_functor_right f' p' g :=
+  begin
+    fapply ppi_homotopy.mk,
+    { exact λa, h a (g a) },
+    { induction g with g r, induction r, induction q,
+      exact whisker_left _ !idp_con ⬝ !idp_con⁻¹ }
+  end
+
+  definition ppi_gen_equiv_ppi_gen_right [constructor] {A : Type*} {B B' : A → Type}
+    {b : B pt} {b' : B' pt} (f : Πa, B a ≃ B' a) (p : f pt b = b') :
+    ppi_gen B b ≃ ppi_gen B' b' :=
+  equiv.MK (ppi_gen_functor_right f p) (ppi_gen_functor_right (λa, (f a)⁻¹ᵉ) (inv_eq_of_eq p⁻¹))
+    abstract begin
+      intro g, apply ppi_eq,
+      refine !ppi_gen_functor_right_compose⁻¹*' ⬝*' _,
+      refine ppi_gen_functor_right_homotopy (λa, to_right_inv (f a)) _ g ⬝*'
+            !ppi_gen_functor_right_id, induction p, exact adj (f pt) b ⬝ ap02 (f pt) !idp_con⁻¹
+
+    end end
+    abstract begin
+      intro g, apply ppi_eq,
+      refine !ppi_gen_functor_right_compose⁻¹*' ⬝*' _,
+      refine ppi_gen_functor_right_homotopy (λa, to_left_inv (f a)) _ g ⬝*'
+            !ppi_gen_functor_right_id, induction p, exact (!idp_con ⬝ !idp_con)⁻¹,
+    end end
+
+  definition ppi_gen_equiv_ppi_gen_basepoint [constructor] {A : Type*} {B : A → Type} {b b' : B pt}
+    (p : b = b') : ppi_gen B b ≃ ppi_gen B b' :=
+  ppi_gen_equiv_ppi_gen_right (λa, erfl) p
+
+  definition ppi_psigma {A : Type*} {B : A → Type*} (C : Πa, B a → Type) (c : Πa, C a pt) :
+    (Π*(a : A), (psigma_gen (C a) (c a))) ≃*
+    psigma_gen (λ(f : Π*(a : A), B a), ppi_gen (λa, C a (f a))
+                                               (transport (C pt) (ppi.resp_pt f)⁻¹ (c pt)))
+               (ppi_const _) :=
+  calc (Π*(a : A), psigma_gen (C a) (c a))
+          ≃* @psigma_gen (p_pi (λa, psigma_gen (C a) (c a))) (λf, f pt = pt) idp : pppi.sigma_char
+      ... ≃* psigma_gen (λ(f : Π*(a : A), B a), ppi_gen (λa, C a (f a))
+                                                        (transport (C pt) (ppi.resp_pt f)⁻¹ (c pt)))
+                        (ppi_const _) : sorry
+
+  definition pmap_psigma {A B : Type*} (C : B → Type) (c : C pt) :
+    ppmap A (psigma_gen C c) ≃*
+    psigma_gen (λ(f : ppmap A B), ppi_gen (C ∘ f) (transport C (respect_pt f)⁻¹ c))
+                (ppi_const _) :=
+  !pppi_pequiv_ppmap⁻¹ᵉ* ⬝e* !ppi_psigma ⬝e* sorry
+
+
+  definition pfiber_ppcompose_left (f : B →* C) :
+    pfiber (@ppcompose_left A B C f) ≃* ppmap A (pfiber f) :=
+  calc
+    pfiber (@ppcompose_left A B C f) ≃*
+             psigma_gen (λ(g : ppmap A B), f ∘* g = pconst A C)
+             proof (eq_of_phomotopy (pcompose_pconst f)) qed :
+             by exact !pfiber.sigma_char'
+      ... ≃* psigma_gen (λ(g : ppmap A B), f ∘* g ~* pconst A C) proof (pcompose_pconst f) qed :
+             by exact psigma_gen_pequiv_psigma_gen_right (λa, !pmap_eq_equiv)
+                        !phomotopy_of_eq_of_phomotopy
+      ... ≃* psigma_gen (λ(g : ppmap A B), ppi_gen (λa, f (g a) = pt)
+               (transport (λb, f b = pt) (respect_pt g)⁻¹ (respect_pt f)))
+               (ppi_const _) :
+             begin
+               refine psigma_gen_pequiv_psigma_gen_right
+                        (λg, ppi_gen_equiv_ppi_gen_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
+               intro g, refine !con_idp ⬝ _, apply whisker_right,
+               exact ap02 f !inv_inv⁻¹ ⬝ !ap_inv,
+               apply ppi_eq, fapply ppi_homotopy.mk,
+                 intro x, reflexivity,
+                 refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
+             end
+      ... ≃* ppmap A (psigma_gen (λb, f b = pt) (respect_pt f)) :
+             by exact (pmap_psigma _ _)⁻¹ᵉ*
+      ... ≃* ppmap A (pfiber f) : by exact pequiv_ppcompose_left !pfiber.sigma_char'⁻¹ᵉ*
+
+
+  definition pfiber_ppcompose_left_dep {B C : A → Type*} (f : Πa, B a →* C a) :
+    pfiber (ppi_compose_left f) ≃* Π*(a : A), pfiber (f a) :=
+  calc
+    pfiber (ppi_compose_left f) ≃*
+             psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g = ppi_const C)
+               proof (ppi_eq (pmap_compose_ppi_const_right f)) qed : by exact !pfiber.sigma_char'
+      ... ≃* psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g ~~* ppi_const C)
+               proof (pmap_compose_ppi_const_right f) qed :
+             by exact psigma_gen_pequiv_psigma_gen_right (λa, !ppi_eq_equiv)
+                        !ppi_homotopy_of_eq_of_ppi_homotopy
+      ... ≃* psigma_gen (λ(g : Π*(a : A), B a), ppi_gen (λa, f a (g a) = pt)
+               (transport (λb, f pt b = pt) (ppi.resp_pt g)⁻¹ (respect_pt (f pt))))
+               (ppi_const _) :
+             begin
+               refine psigma_gen_pequiv_psigma_gen_right
+                        (λg, ppi_gen_equiv_ppi_gen_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
+               intro g, refine !con_idp ⬝ _, apply whisker_right,
+               exact ap02 (f pt) !inv_inv⁻¹ ⬝ !ap_inv,
+               apply ppi_eq, fapply ppi_homotopy.mk,
+                 intro x, reflexivity,
+                 refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
+             end
+      ... ≃* Π*(a : A), (psigma_gen (λb, f a b = pt) (respect_pt (f a))) :
+             by exact (ppi_psigma _ _)⁻¹ᵉ*
+      ... ≃* Π*(a : A), pfiber (f a) : by exact ppi_pequiv_right (λa, !pfiber.sigma_char'⁻¹ᵉ*)
+
 end pointed open pointed
 
 open is_trunc is_conn
-section
+namespace is_conn
   variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A]
   include H
 
@@ -210,9 +419,9 @@ section
   begin
     apply is_contr.mk pt,
     intro f, induction f with f p,
-    fapply ppi_eq,
+    apply ppi_eq, fapply ppi_homotopy.mk,
-    { apply is_conn.elim n, esimp, exact p⁻¹ },
+    { apply is_conn.elim n, exact p⁻¹ },
-    { krewrite (is_conn.elim_β n), apply inverse, apply con.left_inv }
+    { krewrite (is_conn.elim_β n), apply con.left_inv }
   end
 
   definition is_trunc_ppi (k : ℕ₋₂) (P : A → (n.+1+2+k)-Type*)
@@ -237,4 +446,4 @@ section
   @is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B)
     (is_trunc_ppi A n k (λ a, B))
 
-end
+end is_conn