work on translation from reduced cohomology to unreduced cohomology

homotopy/EM.hlean

@@ -1,7 +1,7 @@
 -- Authors: Floris van Doorn
 
 import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
-       ..move_to_lib
+       ..move_to_lib .susp
 
 open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
 
@@ -518,33 +518,6 @@ namespace EM
   equivalence.mk (EM_cfunctor (n+2)) (is_equivalence_EM_cfunctor n)
   end category
 
-  /- move -/
-
-  open trunc_index
-  definition is_trunc_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
-    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
-  begin
-    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
-    refine is_conn.elim -1 _ _, exact H
-  end
-
-  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
-    (H2 : is_conn m A) : is_trunc (m + n) A :=
-  begin
-    revert A H H2; induction m with m IH: intro A H H2,
-    { rewrite [nat.zero_add], exact H },
-    rewrite [succ_add],
-    apply is_trunc_succ_of_is_trunc_loop,
-    { apply IH,
-      { apply is_trunc_equiv_closed _ !loopn_succ_in },
-      apply is_conn_loop },
-    exact is_conn_of_le _ (zero_le_of_nat (succ m))
-  end
-
-  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
-    (H2 : is_conn m A) : is_trunc m A :=
-  is_trunc_of_is_trunc_loopn m 0 A H H2
-
   definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[n] X ≃* EM1 G)
     [H1 : is_conn n X] : X ≃* EMadd1 G n :=
   begin
@@ -563,6 +536,25 @@ namespace EM
     abstract (EM1_functor_gcompose φ φ⁻¹ᵍ)⁻¹* ⬝* EM1_functor_phomotopy proof right_inv φ qed ⬝*
              EM1_functor_gid H end
 
+  definition is_contr_EM1 {G : Group} (H : is_contr G) : is_contr (EM1 G) :=
+  is_contr_of_is_conn_of_is_trunc
+    (is_trunc_succ_succ_of_is_trunc_loop _ _ (is_trunc_equiv_closed _ !loop_EM1) _) !is_conn_EM1
+
+  definition is_contr_EMadd1 (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (EMadd1 G n) :=
+  begin
+    induction n with n IH,
+    { exact is_contr_EM1 H },
+    { have is_contr (ptrunc (n+2) (psusp (EMadd1 G n))), from _,
+      exact this }
+  end
+
+  definition is_contr_EM (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (K G n) :=
+  begin
+    cases n with n,
+    { exact H },
+    { exact is_contr_EMadd1 n H }
+  end
+
   definition EMadd1_pequiv_EMadd1 (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : EMadd1 G n ≃* EMadd1 H n :=
   pequiv.MK (EMadd1_functor φ n) (EMadd1_functor φ⁻¹ᵍ n)
     abstract (EMadd1_functor_gcompose φ⁻¹ᵍ φ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof left_inv φ qed n ⬝*
@@ -577,4 +569,12 @@ namespace EM
     { exact EMadd1_pequiv_EMadd1 n φ }
   end
 
+  definition ppi_EMadd1 {X : Type*} (Y : X → Type*) (n : ℕ) :
+    (Π*(x : X), EMadd1 (πag[n+2] (Y x)) (n+1)) ≃* EMadd1 (πag[n+2] (Π*(x : X), Y x)) (n+1) :=
+  begin
+    exact sorry
+  end
+--EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k
+
+
 end EM

homotopy/cohomology.hlean

@@ -43,7 +43,7 @@ definition ordinary_parametrized_cohomology [reducible] {X : Type*} (G : X → A
 parametrized_cohomology (λx, EM_spectrum (G x)) n
 
 definition unreduced_parametrized_cohomology {X : Type} (Y : X → spectrum) (n : ℤ) : AbGroup :=
-@parametrized_cohomology X₊ (λx, option.cases_on x sunit Y) n
+@parametrized_cohomology X₊ (add_point_spectrum Y) n
 
 definition unreduced_ordinary_parametrized_cohomology [reducible] {X : Type} (G : X → AbGroup)
   (n : ℤ) : AbGroup :=
@@ -78,7 +78,6 @@ definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
 sorry
 
-
 /- functoriality -/
 
 definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
@@ -118,7 +117,7 @@ definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn,
    : H^n[X, Y] ≃g H^n[X, Y'] :=
 sorry
 
-definition parametrized_cohomology_isomorphism_right (X : Type*) {Y Y' : X → spectrum}
+definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum}
   (e : Πx n, Y x n ≃* Y' x n) (n : ℤ)
    : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
 sorry
@@ -127,9 +126,19 @@ definition ordinary_cohomology_isomorphism_right (X : Type*) {G G' : AbGroup} (e
   (n : ℤ) : oH^n[X, G] ≃g oH^n[X, G'] :=
 cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
 
-definition ordinary_parametrized_cohomology_isomorphism_right (X : Type*) {G G' : X → AbGroup}
+definition ordinary_parametrized_cohomology_isomorphism_right {X : Type*} {G G' : X → AbGroup}
   (e : Πx, G x ≃g G' x) (n : ℤ) : opH^n[(x : X), G x] ≃g opH^n[(x : X), G' x] :=
-parametrized_cohomology_isomorphism_right X (λx, EM_spectrum_pequiv (e x)) n
+parametrized_cohomology_isomorphism_right (λx, EM_spectrum_pequiv (e x)) n
+
+definition uopH_isomorphism_opH {X : Type} (G : X → AbGroup) (n : ℤ) :
+  uopH^n[(x : X), G x] ≃g opH^n[(x : X₊), add_point_AbGroup G x] :=
+parametrized_cohomology_isomorphism_right
+  begin
+    intro x n, induction x with x,
+    { symmetry, apply EM_spectrum_trivial, },
+    { reflexivity }
+  end
+  n
 
 /- suspension axiom -/
 

homotopy/serre.hlean

@@ -1,7 +1,7 @@
 import ..algebra.module_exact_couple .strunc .cohomology
 
 open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
-     cohomology group sigma unit
+     cohomology group sigma unit is_conn
 set_option pp.binder_types true
 
 /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
@@ -19,7 +19,7 @@ begin
 end
 
 section
-open nat is_conn group
+open nat group
 definition pfiber_postnikov_map (A : Type*) (n : ℕ) :
   pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
 begin
@@ -76,10 +76,30 @@ definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) :
   strunc k X →ₛ strunc (k - 1) X :=
 strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
 
+/-
+  we could try to prove that postnikov_smap is homotopic to postnikov_map, although the types
+  are different enough, that even stating it will be quite annoying
+-/
+
 definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) :
-  pfiber (postnikov_smap A n k) ≃* EM_spectrum (πₛ[n] A) k :=
+  sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) k :=
 begin
   exact sorry
+/-  symmetry, apply spectrum_pequiv_of_nat_succ_succ, clear k, intro k,
+  apply EMadd1_pequiv k,
+  { exact sorry
+    -- refine _ ⬝g shomotopy_group_strunc n A,
+    -- exact chain_complex.LES_isomorphism_of_trivial_cod _ _
+    --   (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
+    --   (trivial_homotopy_group_of_is_trunc _ (le_succ _))
+},
+  { exact sorry --apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr
+    },
+  { -- have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
+    -- have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
+    -- apply is_trunc_pfiber
+    exact sorry
+    }-/
 end
 
 section atiyah_hirzebruch
@@ -121,8 +141,8 @@ section atiyah_hirzebruch
     (λn s, πₛ[n] (sfiber (postnikov_smap (spi X Y) s))) ⟹ᵍ (λn, πₛ[n] (strunc s₀ (spi X Y))) :=
   converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
 
-  lemma spi_EM_spectrum (k s : ℤ) :
+  lemma spi_EM_spectrum (k n : ℤ) :
-    EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k :=
+    EM_spectrum (πₛ[n] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
   sorry
 
   definition atiyah_hirzebruch_convergence :
@@ -142,30 +162,23 @@ section atiyah_hirzebruch
       apply ptrunc_pequiv, exact is_strunc_spi s₀ Y H k,
     end
 
---{X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
 end atiyah_hirzebruch
 
 section unreduced_atiyah_hirzebruch
 
-open option
-
 definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ)
   (H : Πx, is_strunc s₀ (Y x)) :
   (λn s, uopH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) :=
 converges_to_g_isomorphism
   (@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H))
   begin
-    intro n s, exact sorry
+    intro n s, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ,
-    -- refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ,
+    apply ordinary_parametrized_cohomology_isomorphism_right,
-    -- apply shomotopy_group_isomorphism_of_pequiv, intro k,
+    intro x,
-    -- refine pfiber_postnikov_smap (spi X Y) s k ⬝e* _,
+    apply shomotopy_group_add_point_spectrum
-    -- apply spi_EM_spectrum
   end
   begin
-    intro n, exact sorry
+    intro n, reflexivity
-    -- refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ,
-    -- apply shomotopy_group_isomorphism_of_pequiv, intro k,
-    -- apply ptrunc_pequiv, exact is_strunc_spi s₀ Y H k,
   end
 end unreduced_atiyah_hirzebruch
 
@@ -178,28 +191,28 @@ section serre
 
   postfix `₊ₒ`:(max+1) := add_point_over
 
-  /- NOTE: we need unreduced cohomology, maybe also define aityah_hirzebruch for unreduced cohomology -/
   include H
-  definition serre_convergence :
+ --  definition serre_convergence :
-    (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) :=
+ --    (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) :=
-  proof
+ --  proof
-  converges_to_g_isomorphism
+ --  converges_to_g_isomorphism
-    (atiyah_hirzebruch_convergence (λx, sp_cotensor (F₊ₒ x) Y) s₀
+ --    (unreduced_atiyah_hirzebruch_convergence
-                                   (λx, is_strunc_sp_cotensor s₀ (F₊ₒ x) H))
+ --      (λx, sp_cotensor (F x) Y) s₀
-    begin
+ --      (λx, is_strunc_sp_cotensor s₀ (F x) H))
-      exact sorry
+ --      begin
-      -- intro n s,
+ --        exact sorry
-      -- apply ordinary_parametrized_cohomology_isomorphism_right,
+ --        -- intro n s,
-      -- intro x,
+ --        -- apply ordinary_parametrized_cohomology_isomorphism_right,
-      -- exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
+ --        -- intro x,
-    end
+ --        -- exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
-    begin
+ --      end
-      intro n, exact sorry
+ --      begin
---      refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _,
+ --        intro n, exact sorry
---      refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
+ --  --      refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _,
---      apply shomotopy_group_isomorphism_of_pequiv, intro k,
+ --  --      refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
-    end
+ --  --      apply shomotopy_group_isomorphism_of_pequiv, intro k,
- qed
+ --      end
+ -- qed
 end serre
 
 /- TODO: πₛ[n] (strunc 0 (spi X Y)) ≃g H^n[X, λx, Y x] -/

homotopy/spectrum.hlean

@@ -253,11 +253,34 @@ namespace spectrum
   -- Equivalences of prespectra
   ------------------------------
 
+  definition spectrum_pequiv_of_pequiv_succ {E F : spectrum} (n : ℤ) (e : E (n + 1) ≃* F (n + 1)) :
+    E n ≃* F n :=
+  equiv_glue E n ⬝e* loop_pequiv_loop e ⬝e* (equiv_glue F n)⁻¹ᵉ*
+
   definition spectrum_pequiv_of_nat {E F : spectrum} (e : Π(n : ℕ), E n ≃* F n) (n : ℤ) :
     E n ≃* F n :=
   begin
-    have Πn, E (n + 1) ≃* F (n + 1) → E n ≃* F n,
+    induction n with n n,
-    from λk f, equiv_glue E k ⬝e* loop_pequiv_loop f ⬝e* (equiv_glue F k)⁻¹ᵉ*,
+      exact e n,
+    induction n with n IH,
+    { exact spectrum_pequiv_of_pequiv_succ -[1+0] (e 0) },
+    { exact spectrum_pequiv_of_pequiv_succ -[1+succ n] IH }
+  end
+
+  -- definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
+  --   (e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
+  -- begin
+  --   apply spectrum_pequiv_of_nat,
+  --   refine nat.rec_down _ m e _,
+  --   intro n f m, cases m with m,
+
+  -- end
+
+  definition is_contr_spectrum_of_nat {E : spectrum} (e : Π(n : ℕ), is_contr (E n)) (n : ℤ) :
+    is_contr (E n)  :=
+  begin
+    have Πn, is_contr (E (n + 1)) → is_contr (E n),
+    from λn H, @(is_trunc_equiv_closed_rev -2 !equiv_glue) (is_contr_loop_of_is_contr H),
     induction n with n n,
       exact e n,
     induction n with n IH,
@@ -338,18 +361,6 @@ namespace spectrum
   definition psp_sphere : gen_prespectrum +ℕ :=
     psp_susp bool.pbool
 
-  ------------------------------
-  -- Contractible spectrum
-  ------------------------------
-
-  definition sunit.{u} [constructor] : spectrum.{u} :=
-  spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
-
-  open option
-  definition add_point_spectrum {X : Type} (Y : X → spectrum) : X₊ → spectrum
-  | (some x) := Y x
-  | none     := sunit
-
   /---------------------
     Homotopy groups
    ---------------------/
@@ -756,6 +767,29 @@ spectrify_fun (smash_prespectrum_fun f g)
 
   /- Cofibers and stability -/
 
+
+  ------------------------------
+  -- Contractible spectrum
+  ------------------------------
+
+  definition sunit.{u} [constructor] : spectrum.{u} :=
+  spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
+
+  definition shomotopy_group_sunit.{u} (n : ℤ) : πₛ[n] sunit.{u} ≃g trivial_ab_group_lift.{u} :=
+  have H : 0 <[ℕ] 2, from !zero_lt_succ,
+  isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H)
+    !is_trunc_lift
+
+  open option
+  definition add_point_spectrum [unfold 3] {X : Type} (Y : X → spectrum) : X₊ → spectrum
+  | (some x) := Y x
+  | none     := sunit
+
+  definition shomotopy_group_add_point_spectrum {X : Type} (Y : X → spectrum) (n : ℤ) :
+    Π(x : X₊), πₛ[n] (add_point_spectrum Y x) ≃g add_point_AbGroup (λ (x : X), πₛ[n] (Y x)) x
+  | (some x) := by reflexivity
+  | none     := shomotopy_group_sunit n
+
   /- The Eilenberg-MacLane spectrum -/
 
   definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
@@ -765,6 +799,12 @@ spectrify_fun (smash_prespectrum_fun f g)
     EM_spectrum G n ≃* EM_spectrum H n :=
   spectrum_pequiv_of_nat (λk, EM_pequiv_EM k e) n
 
+  definition EM_spectrum_trivial.{u} (n : ℤ) :
+    EM_spectrum trivial_ab_group_lift.{u} n ≃* trivial_ab_group_lift.{u} :=
+  pequiv_of_is_contr _ _
+    (is_contr_spectrum_of_nat (λk, is_contr_EM k !is_trunc_lift) n)
+    !is_trunc_lift
+
   /- Wedge of prespectra -/
 
 open fwedge

homotopy/susp.hlean

@@ -1,6 +1,6 @@
-import homotopy.susp types.pointed2
+import homotopy.susp types.pointed2 ..move_to_lib
 
-open susp eq pointed function is_equiv lift equiv
+open susp eq pointed function is_equiv lift equiv is_trunc
 
 namespace susp
   variables {X X' Y Y' Z : Type*}
@@ -90,4 +90,42 @@ namespace susp
                         ... ≃* psusp (plift.{u v} A) : by exact psusp_pequiv (pequiv_plift.{u v} A)
   end
 
+  definition is_contr_susp [instance] (A : Type) [H : is_contr A] : is_contr (susp A) :=
+  begin
+    apply is_contr.mk north,
+    intro x, induction x,
+    reflexivity,
+    exact merid !center,
+    apply eq_pathover_constant_left_id_right, apply square_of_eq,
+    exact whisker_left idp (ap merid !eq_of_is_contr)
+  end
+
+  definition is_contr_psusp [instance] (A : Type) [H : is_contr A] : is_contr (psusp A) :=
+  is_contr_susp A
+
+definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
+pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
+
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
+            {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
+            {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
+
+  -- rename: psusp_functor_psquare
+  definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
+sorry
+
+  definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
+  begin
+    intro p,
+    refine pvconcat _ (ap1_psquare p),
+    exact loop_psusp_unit_natural f₁₀
+  end
+
+  definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
+  begin
+    intro p,
+    refine pvconcat (suspend_psquare p) _,
+    exact psquare_transpose (loop_psusp_counit_natural f₁₂)
+  end
+
 end susp

move_to_lib.hlean

@@ -1,7 +1,6 @@
 -- 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.susp
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
      is_trunc function sphere unit prod bool
@@ -294,9 +293,6 @@ namespace trunc
     { apply idp_con }
   end
 
-  definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
-  transport (λk, is_trunc k A) p H
-
   definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
     (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
   is_trunc_trunc_of_is_trunc A n m
@@ -326,6 +322,38 @@ namespace trunc
 
 end trunc
 
+namespace is_trunc
+
+  open trunc_index is_conn
+
+  definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
+  transport (λk, is_trunc k A) p H
+
+  definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
+    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
+  begin
+    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
+    refine is_conn.elim -1 _ _, exact H
+  end
+
+  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc (m + n) A :=
+  begin
+    revert A H H2; induction m with m IH: intro A H H2,
+    { rewrite [nat.zero_add], exact H },
+    rewrite [succ_add],
+    apply is_trunc_succ_succ_of_is_trunc_loop,
+    { apply IH,
+      { apply is_trunc_equiv_closed _ !loopn_succ_in },
+      apply is_conn_loop },
+    exact is_conn_of_le _ (zero_le_of_nat (succ m))
+  end
+
+  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc m A :=
+  is_trunc_of_is_trunc_loopn m 0 A H H2
+
+end is_trunc
 namespace sigma
 
   -- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type}
@@ -381,6 +409,14 @@ namespace group
     reflexivity
   end
 
+  open option
+  definition add_point_AbGroup [unfold 3] {X : Type} (G : X → AbGroup) : X₊ → AbGroup
+  | (some x) := G x
+  | none     := trivial_ab_group_lift
+
+  definition isomorphism_of_is_contr {G H : Group} (hG : is_contr G) (hH : is_contr H) : G ≃g H :=
+  trivial_group_of_is_contr G ⬝g (trivial_group_of_is_contr H)⁻¹ᵍ
+
 end group open group
 
 namespace function
@@ -419,35 +455,6 @@ namespace is_conn
 
 end is_conn
 
-namespace is_trunc
-
-open trunc_index is_conn
-
-  definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
-    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
-  begin
-    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
-    refine is_conn.elim -1 _ _, exact H
-  end
-  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
-    (H2 : is_conn m A) : is_trunc (m +[ℕ] n) A :=
-  begin
-    revert A H H2; induction m with m IH: intro A H H2,
-    { rewrite [nat.zero_add], exact H },
-    rewrite [succ_add],
-    apply is_trunc_succ_succ_of_is_trunc_loop,
-    { apply IH,
-      { apply is_trunc_equiv_closed _ !loopn_succ_in },
-      apply is_conn_loop },
-    exact is_conn_of_le _ (zero_le_of_nat (succ m))
-  end
-
-  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
-    (H2 : is_conn m A) : is_trunc m A :=
-  is_trunc_of_is_trunc_loopn m 0 A H H2
-
-end is_trunc
-
 namespace misc
   open is_conn
 
@@ -801,34 +808,16 @@ begin
   rewrite trans_refl
 end
 
-definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
-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₂₂}
-
   definition psquare_transpose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹*
 
-  definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
-sorry
-
-  definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
-  begin
-    intro p,
-    refine pvconcat _ (ap1_psquare p),
-    exact loop_psusp_unit_natural f₁₀
-  end
-
-  definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
-  begin
-    intro p,
-    refine pvconcat (suspend_psquare p) _,
-    exact psquare_transpose (loop_psusp_counit_natural f₁₂)
-  end
 end pointed

pointed.hlean

@@ -195,6 +195,9 @@ namespace pointed
   definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) :=
   is_contr.mk idp (λa, !is_prop.elim)
 
+  definition is_contr_loop_of_is_contr {A : Type*} (H : is_contr A) : is_contr (Ω A) :=
+  is_contr_loop A
+
   definition is_contr_punit [instance] : is_contr punit :=
   is_contr_unit