diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean
index 7bfc731..6a8b5e6 100644
--- a/algebra/arrow_group.hlean
+++ b/algebra/arrow_group.hlean
@@ -61,6 +61,12 @@ namespace group
     exact to_is_equiv (pequiv_ppcompose_right f),
   end
 
+  definition Group_trunc_pmap_isomorphism_refl (A B : Type*) (x : Group_trunc_pmap A B) :
+    Group_trunc_pmap_isomorphism (pequiv.refl A) x = x :=
+  begin
+    induction x, apply ap tr, apply eq_of_phomotopy, apply pcompose_pid
+  end
+
   definition Group_trunc_pmap_pid [constructor] {A B : Type*} (f : Group_trunc_pmap A B) :
     Group_trunc_pmap_homomorphism (pid A) f = f :=
   begin
@@ -83,7 +89,16 @@ namespace group
   definition Group_trunc_pmap_phomotopy [constructor] {A A' B : Type*} {f f' : A' →* A} (p : f ~* f') :
     @Group_trunc_pmap_homomorphism _ _ B f ~ Group_trunc_pmap_homomorphism f' :=
   begin
-    intro f, induction f, exact ap tr (eq_of_phomotopy (pwhisker_left a p))
+    intro g, induction g, exact ap tr (eq_of_phomotopy (pwhisker_left a p))
+  end
+
+  definition Group_trunc_pmap_phomotopy_refl {A A' B : Type*} (f : A' →* A)
+    (x : Group_trunc_pmap A B) : Group_trunc_pmap_phomotopy (phomotopy.refl f) x = idp :=
+  begin
+    induction x,
+    refine ap02 tr _,
+    refine ap eq_of_phomotopy _ ⬝ !eq_of_phomotopy_refl,
+    apply pwhisker_left_refl
   end
 
   definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : ab_inf_group (A →* Ω (Ω B)) :=
diff --git a/choice.hlean b/choice.hlean
index 9f210dc..b873345 100644
--- a/choice.hlean
+++ b/choice.hlean
@@ -1,6 +1,6 @@
-import types.trunc types.sum
+import types.trunc types.sum types.lift types.unit
 
-open pi prod sum unit bool trunc is_trunc is_equiv eq equiv
+open pi prod sum unit bool trunc is_trunc is_equiv eq equiv lift pointed
 
 namespace choice
 
@@ -8,10 +8,10 @@ namespace choice
 definition unchoose [unfold 4] (n : ℕ₋₂) {X : Type} (A : X → Type) : trunc n (Πx, A x) → Πx, trunc n (A x) :=
 trunc.elim (λf x, tr (f x))
 
-definition has_choice.{u} (n : ℕ₋₂) (X : Type.{u}) : Type.{u+1} :=
+definition has_choice.{u} [class] (n : ℕ₋₂) (X : Type.{u}) : Type.{u+1} :=
 Π(A : X → Type.{u}), is_equiv (unchoose n A)
 
-definition choice_equiv.{u} [constructor] {n : ℕ₋₂} {X : Type.{u}} (H : has_choice n X) (A : X → Type.{u})
+definition choice_equiv.{u} [constructor] {n : ℕ₋₂} {X : Type.{u}} [H : has_choice n X] (A : X → Type.{u})
   : trunc n (Πx, A x) ≃ (Πx, trunc n (A x)) :=
 equiv.mk _ (H A)
 
@@ -22,7 +22,7 @@ begin
   { exact H n }
 end
 
-definition has_choice_empty (n : ℕ₋₂) : has_choice n empty :=
+definition has_choice_empty [instance] (n : ℕ₋₂) : has_choice n empty :=
 begin
   intro A, fapply adjointify,
   { intro f, apply tr, intro x, induction x },
@@ -30,16 +30,7 @@ begin
   { intro g, induction g with g, apply ap tr, apply eq_of_homotopy, intro x, induction x }
 end
 
-definition is_trunc_is_contr_fiber [instance] [priority 900] (n : ℕ₋₂) {A B : Type} (f : A → B)
-  (b : B) [is_trunc n A] [is_trunc n B] : is_trunc n (is_contr (fiber f b)) :=
-begin
-  cases n,
-  { apply is_contr_of_inhabited_prop, apply is_contr_fun_of_is_equiv,
-    apply is_equiv_of_is_contr },
-  { apply is_trunc_succ_of_is_prop }
-end
-
-definition has_choice_unit : Πn, has_choice n unit :=
+definition has_choice_unit [instance] : Πn, has_choice n unit :=
 begin
   intro n A, fapply adjointify,
   { intro f, induction f ⋆ with a, apply tr, intro u, induction u, exact a },
@@ -49,8 +40,8 @@ begin
     intro u, induction u, reflexivity }
 end
 
-definition has_choice_sum.{u} (n : ℕ₋₂) {A B : Type.{u}} (hA : has_choice n A) (hB : has_choice n B)
-  : has_choice n (A ⊎ B) :=
+definition has_choice_sum.{u} [instance] (n : ℕ₋₂) (A B : Type.{u})
+  [has_choice n A] [has_choice n B] : has_choice n (A ⊎ B) :=
 begin
   intro P, fapply is_equiv_of_equiv_of_homotopy,
   { exact calc
@@ -58,7 +49,7 @@ begin
        : trunc_equiv_trunc n !equiv_sum_rec⁻¹ᵉ
      ... ≃ trunc n (Πa, P (inl a)) × trunc n (Πb, P (inr b)) : trunc_prod_equiv
      ... ≃ (Πa, trunc n (P (inl a))) × Πb, trunc n (P (inr b))
-       : by exact prod_equiv_prod (choice_equiv hA _) (choice_equiv hB _)
+       : by exact prod_equiv_prod (choice_equiv _) (choice_equiv _)
      ... ≃ Πx, trunc n (P x) : equiv_sum_rec },
   { intro f, induction f, apply eq_of_homotopy, intro x, esimp, induction x with a b: reflexivity }
 end
@@ -70,8 +61,18 @@ begin
   induction f using rec_on_ua_idp, assumption
 end
 
-definition has_choice_bool (n : ℕ₋₂) : has_choice n bool :=
-has_choice_equiv_closed n bool_equiv_unit_sum_unit
-  (has_choice_sum n (has_choice_unit n) (has_choice_unit n))
+definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice n bool :=
+has_choice_equiv_closed n bool_equiv_unit_sum_unit _
+
+definition has_choice_lift [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] :
+  has_choice n (lift A) :=
+has_choice_equiv_closed n !equiv_lift⁻¹ᵉ _
+
+definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice n punit := has_choice_unit n
+definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice n pbool := has_choice_bool n
+definition has_choice_plift [instance] (n : ℕ₋₂) (A : Type*) [has_choice n A]
+  : has_choice n (plift A) := has_choice_lift n A
+definition has_choice_psum [instance] (n : ℕ₋₂) (A B : Type*) [has_choice n A] [has_choice n B]
+  : has_choice n (psum A B) := has_choice_sum n A B
 
 end choice
diff --git a/homotopy/cofiber_sequence.hlean b/homotopy/cofiber_sequence.hlean
new file mode 100644
index 0000000..9dfe53d
--- /dev/null
+++ b/homotopy/cofiber_sequence.hlean
@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2017 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Cofiber sequence of a pointed map
+-/
+
+import .cohomology .pushout
+
+open pointed eq cohomology sigma sigma.ops fiber cofiber chain_complex nat succ_str algebra prod group pushout int
+
+namespace cohomology
+
+  definition pred_fun {A : ℕ → Type*} (f : Πn, A n →* A (n+1)) (n : ℕ) : A (pred n) →* A n :=
+  begin cases n with n, exact pconst (A 0) (A 0), exact f n end
+
+  definition type_chain_complex_snat' [constructor] (A : ℕ → Type*) (f : Πn, A n →* A (n+1))
+    (p : Πn (x : A n), f (n+1) (f n x) = pt) : type_chain_complex -ℕ :=
+  type_chain_complex.mk A (pred_fun f)
+    begin
+      intro n, cases n with n, intro x, reflexivity, cases n with n,
+      intro x, exact respect_pt (f 0), exact p n
+    end
+
+  definition chain_complex_snat' [constructor] (A : ℕ → Set*) (f : Πn, A n →* A (n+1))
+    (p : Πn (x : A n), f (n+1) (f n x) = pt) : chain_complex -ℕ :=
+  chain_complex.mk A (pred_fun f)
+    begin
+      intro n, cases n with n, intro x, reflexivity, cases n with n,
+      intro x, exact respect_pt (f 0), exact p n
+    end
+
+  definition is_exact_at_t_snat' [constructor] {A : ℕ → Type*} (f : Πn, A n →* A (n+1))
+    (p : Πn (x : A n), f (n+1) (f n x) = pt) (q : Πn x, f (n+1) x = pt → fiber (f n) x) (n : ℕ)
+    : is_exact_at_t (type_chain_complex_snat' A f p) (n+2) :=
+  q n
+
+  definition cofiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y)
+    : Σ(Y Z : Type*), Y →* Z :=
+  ⟨v.2.1, pcofiber v.2.2, pcod v.2.2⟩
+
+  definition cofiber_sequence_helpern (v : Σ(X Y : Type*), X →* Y) (n : ℕ)
+    : Σ(Z X : Type*), Z →* X :=
+  iterate cofiber_sequence_helper n v
+
+  section
+  universe variable u
+  parameters {X Y : pType.{u}} (f : X →* Y)
+  include f
+
+  definition cofiber_sequence_carrier (n : ℕ) : Type* :=
+  (cofiber_sequence_helpern ⟨X, Y, f⟩ n).1
+
+  definition cofiber_sequence_fun (n : ℕ)
+    : cofiber_sequence_carrier n →* cofiber_sequence_carrier (n+1) :=
+  (cofiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
+
+  definition cofiber_sequence : type_chain_complex.{0 u} -ℕ :=
+  begin
+    fapply type_chain_complex_snat',
+    { exact cofiber_sequence_carrier },
+    { exact cofiber_sequence_fun },
+    { intro n x, exact pcod_pcompose (cofiber_sequence_fun n) x }
+  end
+
+  end
+
+  section
+  universe variable u
+  parameters {X Y : pType.{u}} (f : X →* Y) (H : cohomology_theory.{u})
+  include f
+
+  definition cohomology_groups [reducible] : -3ℤ → AbGroup
+  | (n, fin.mk 0 p) := H n X
+  | (n, fin.mk 1 p) := H n Y
+  | (n, fin.mk k p) := H n (pcofiber f)
+
+--   definition cohomology_groups_pequiv_loop_spaces2 [reducible]
+--     : Π(n : -3ℤ), ptrunc 0 (loop_spaces2 n) ≃* cohomology_groups n
+--   | (n, fin.mk 0 p) := by reflexivity
+--   | (n, fin.mk 1 p) := by reflexivity
+--   | (n, fin.mk 2 p) := by reflexivity
+--   | (n, fin.mk (k+3) p) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition coboundary (n : ℤ) : H (pred n) X →g H n (pcofiber f) :=
+  H ^→ n (pcofiber_pcod f ∘* pcod (pcod f)) ∘g (Hsusp_neg H n X)⁻¹ᵍ
+
+  definition cohomology_groups_fun : Π(n : -3ℤ), cohomology_groups (S n) →g cohomology_groups n
+  | (n, fin.mk 0 p) := proof H ^→ n f qed
+  | (n, fin.mk 1 p) := proof H ^→ n (pcod f) qed
+  | (n, fin.mk 2 p) := proof coboundary n qed
+  | (n, fin.mk (k+3) p) := begin exfalso, apply lt_le_antisymm p, apply le_add_left end
+
+  -- definition cohomology_groups_fun_pcohomology_loop_spaces_fun2 [reducible]
+  --   : Π(n : -3ℤ), cohomology_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~*
+  --     cohomology_groups_fun n ∘* cohomology_groups_pequiv_loop_spaces2 (S n)
+  -- | (n, fin.mk 0 p) := by reflexivity
+  -- | (n, fin.mk 1 p) := by reflexivity
+  -- | (n, fin.mk 2 p) :=
+  --   begin
+  --     refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹*,
+  --     refine !ptrunc_functor_pcompose
+  --   end
+  -- | (n, fin.mk (k+3) p) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  open cohomology_theory
+
+  definition cohomology_groups_chain_0 (n : ℤ) (x : H n (pcofiber f)) : H ^→ n f (H ^→ n (pcod f) x) = 1 :=
+  begin
+    refine (Hcompose H n (pcod f) f x)⁻¹ ⬝ _,
+    refine Hhomotopy H n (pcod_pcompose f) x ⬝ _,
+    exact Hconst H n x
+  end
+
+  definition cohomology_groups_chain_1 (n : ℤ) (x : H (pred n) X) : H ^→ n (pcod f) (coboundary n x) = 1 :=
+  begin
+    refine (Hcompose H n (pcofiber_pcod f ∘* pcod (pcod f)) (pcod f) ((Hsusp_neg H n X)⁻¹ᵍ x))⁻¹ ⬝ _,
+    refine Hhomotopy H n (!passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst) _ ⬝ _,
+    exact Hconst H n _
+  end
+
+  definition cohomology_groups_chain_2 (n : ℤ) (x : H (pred n) Y) : coboundary n (H ^→ (pred n) f x) = 1 :=
+  begin
+    exact sorry
+    -- refine ap (H ^→ n (pcofiber_pcod f ∘* pcod (pcod f))) _ ⬝ _,
+--Hsusp_neg_inv_natural H n (pcofiber_pcod f ∘* pcod (pcod f)) _
+  end
+
+  definition cohomology_groups_chain : Π(n : -3ℤ) (x : cohomology_groups (S (S n))),
+    cohomology_groups_fun n (cohomology_groups_fun (S n) x) = 1
+  | (n, fin.mk 0 p) := cohomology_groups_chain_0 n
+  | (n, fin.mk 1 p) := cohomology_groups_chain_1 n
+  | (n, fin.mk 2 p) := cohomology_groups_chain_2 n
+  | (n, fin.mk (k+3) p) := begin exfalso, apply lt_le_antisymm p, apply le_add_left end
+
+  definition LES_of_cohomology_groups [constructor] : chain_complex -3ℤ :=
+  chain_complex.mk (λn, cohomology_groups n) (λn, pmap_of_homomorphism (cohomology_groups_fun n)) cohomology_groups_chain
+
+  definition is_exact_LES_of_cohomology_groups : is_exact LES_of_cohomology_groups :=
+  begin
+    intro n,
+    exact sorry
+  end
+
+  end
+
+end cohomology
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index b8068d2..94d5691 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -3,13 +3,13 @@ Copyright (c) 2016 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
-Reduced cohomology
+Reduced cohomology of spectra and cohomology theories
 -/
 
 import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib
 
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra
+     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit
 
 -- TODO: move
 structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
@@ -133,6 +133,10 @@ definition cohomology_functor_phomotopy {X X' : Type*} {f g : X' →* X} (p : f
   (Y : spectrum) (n : ℤ) : cohomology_functor f Y n ~ cohomology_functor g Y n :=
 Group_trunc_pmap_phomotopy p
 
+definition cohomology_functor_phomotopy_refl {X X' : Type*} (f : X' →* X) (Y : spectrum) (n : ℤ)
+  (x : H^n[X, Y]) : cohomology_functor_phomotopy (phomotopy.refl f) Y n x = idp :=
+Group_trunc_pmap_phomotopy_refl f x
+
 definition cohomology_functor_pconst {X X' : Type*} (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
   cohomology_functor (pconst X' X) Y n f = 1 :=
 !Group_trunc_pmap_pconst
@@ -141,6 +145,10 @@ definition cohomology_isomorphism {X X' : Type*} (f : X' ≃* X) (Y : spectrum)
   H^n[X, Y] ≃g H^n[X', Y] :=
 Group_trunc_pmap_isomorphism f
 
+definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : H^n[X,Y]) :
+  cohomology_isomorphism (pequiv.refl X) Y n x = x :=
+!Group_trunc_pmap_isomorphism_refl
+
 /- suspension axiom -/
 
 definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
@@ -232,25 +240,69 @@ theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
 /- cohomology theory -/
 
 structure cohomology_theory.{u} : Type.{u+1} :=
-  (H : ℤ → pType.{u} → AbGroup.{u})
-  (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), H n Y →g H n X)
-  (Hh_id : Π(n : ℤ) {X : Type*} (x : H n X), Hh n (pid X) x = x)
-  (Hh_compose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (z : H n Z),
+  (HH : ℤ → pType.{u} → AbGroup.{u})
+  (Hiso : Π(n : ℤ) {X Y : Type*} (f : X ≃* Y), HH n Y ≃g HH n X)
+  (Hiso_refl : Π(n : ℤ) (X : Type*) (x : HH n X), Hiso n pequiv.rfl x = x)
+  (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n Y →g HH n X)
+  (Hhomotopy : Π(n : ℤ) {X Y : Type*} {f g : X →* Y} (p : f ~* g), Hh n f ~ Hh n g)
+  (Hhomotopy_refl : Π(n : ℤ) {X Y : Type*} (f : X →* Y) (x : HH n Y),
+    Hhomotopy n (phomotopy.refl f) x = idp)
+  (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
+  (Hcompose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (z : HH n Z),
     Hh n (g ∘* f) z = Hh n f (Hh n g z))
-  (Hsusp : Π(n : ℤ) (X : Type*), H (succ n) (psusp X) ≃g H n X)
+  (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
   (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
     Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y)
   (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
   (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
-    is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : H n (⋁ X) → Πᵍ i, H n (X i)))
+    is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
 structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
- (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (H n (plift pbool)))
+ (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))
+
+attribute cohomology_theory.HH [coercion]
+postfix `^→`:90 := cohomology_theory.Hh
+open cohomology_theory
+
+definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X :=
+isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X
+
+definition Hsusp_neg_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
+  Hsusp_neg H n X ∘ H ^→ n (psusp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y :=
+sorry
+
+definition Hsusp_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
+  H ^→ (succ n) (psusp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f :=
+sorry
+
+definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
+  H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f :=
+sorry
+
+definition Hadditive0 (H : cohomology_theory) (n : ℤ) :
+  is_contr (H n (plift punit)) :=
+let P : lift empty → Type* := lift.rec empty.elim in
+let x := Hadditive H n P _ in
+begin
+  note z := equiv.mk _ x,
+  refine @(is_trunc_equiv_closed_rev -2 (_ ⬝e z ⬝e _)) !is_contr_unit,
+  repeat exact sorry
+--  refine equiv_of_isomorphism (Hiso H n (_ ⬝e* _)),
+end
+
+definition Hconst (H : cohomology_theory) (n : ℤ) {X Y : Type*} (y : H n Y) : H ^→ n (pconst X Y) y = 1 :=
+begin
+  refine !one_mul⁻¹ ⬝ _, exact sorry
+end
 
 definition cohomology_theory_spectrum [constructor] (Y : spectrum) : cohomology_theory :=
 cohomology_theory.mk
   (λn A, H^n[A, Y])
+  (λn A B f, cohomology_isomorphism f Y n)
+  (λn A, cohomology_isomorphism_refl A Y n)
   (λn A B f, cohomology_functor f Y n)
+  (λn A B f g p, cohomology_functor_phomotopy p Y n)
+  (λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
   (λn A x, cohomology_functor_pid A Y n x)
   (λn A B C g f x, cohomology_functor_pcompose g f Y n x)
   (λn A, cohomology_psusp A Y n)
@@ -258,7 +310,7 @@ cohomology_theory.mk
   (λn A B f, cohomology_exact f Y n)
   (λn I A H, spectrum_additive H A Y n)
 
-definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
+definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
 ⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
 
 end cohomology
diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean
index 86a7e58..54864a5 100644
--- a/homotopy/fwedge.hlean
+++ b/homotopy/fwedge.hlean
@@ -7,7 +7,7 @@ The Wedge Sum of a family of Pointed Types
 -/
 import homotopy.wedge ..move_to_lib ..choice
 
-open eq pushout pointed unit trunc_index sigma bool equiv trunc choice
+open eq pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc
 
 definition fwedge' {I : Type} (F : I → Type*) : Type := pushout (λi, ⟨i, Point (F i)⟩) (λi, ⋆)
 definition pt' [constructor] {I : Type} {F : I → Type*} : fwedge' F := inr ⋆
@@ -86,6 +86,11 @@ namespace fwedge
     { exact glue ff }
   end
 
+  definition is_contr_fwedge_empty : is_contr (⋁(empty.rec _)) :=
+  begin
+    apply is_contr.mk pt, intro x, induction x, contradiction, reflexivity, contradiction
+  end
+
   definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
   begin
     fconstructor,
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index 9bbc3df..af83bc4 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -499,4 +499,24 @@ namespace pushout
       exact fiber.mk (pcofiber.elim g q) (eq_of_phomotopy (pcofiber.elim_pcod q)) }
   end
 
+  /- cofiber of pcod is suspension -/
+
+  definition pcofiber_pcod {A B : Type*} (f : A →* B) : pcofiber (pcod f) ≃* psusp A :=
+  begin
+    fapply pequiv_of_equiv,
+    { refine !pushout.symm ⬝e _,
+      exact pushout_vcompose_equiv f equiv.rfl homotopy.rfl homotopy.rfl },
+    reflexivity
+  end
+
+  -- definition pushout_vcompose [constructor] {A B C D : Type} (f : A → B) (g : A → C) (h : B → D) :
+  --   pushout h (@inl _ _ _ f g) ≃ pushout (h ∘ f) g :=
+  -- definition pushout_hcompose {A B C D : Type} (f : A → B) (g : A → C) (h : C → D) :
+  --   pushout (@inr _ _ _ f g) h ≃ pushout f (h ∘ g) :=
+
+  -- definition pushout_vcompose_equiv {A B C D E : Type} (f : A → B) {g : A → C} {h : B → D}
+  --   {hf : A → D} {k : B → E} (e : E ≃ pushout f g) (p : k ~ e⁻¹ᵉ ∘ inl) (q : h ∘ f ~ hf) :
+  --   pushout h k ≃ pushout hf g :=
+
+
 end pushout
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 6e3c374..11fe09c 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -19,6 +19,9 @@ definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m
 namespace algebra
   definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) :=
   by induction H; exact _
+
+  definition one_unique {A : Type} [group A] {a : A} (H : Πb, a * b = b) : a = 1 :=
+  !mul_one⁻¹ ⬝ H 1
 end algebra
 
 namespace eq
@@ -675,6 +678,23 @@ namespace is_trunc
 
   definition center' {A : Type} (H : is_contr A) : A := center A
 
+  definition pequiv_punit_of_is_contr [constructor] (A : Type*) (H : is_contr A) : A ≃* punit :=
+  pequiv_of_equiv (equiv_unit_of_is_contr A) (@is_prop.elim unit _ _ _)
+
+  definition pequiv_punit_of_is_contr' [constructor] (A : Type) (H : is_contr A)
+    : pointed.MK A (center A) ≃* punit :=
+  pequiv_punit_of_is_contr (pointed.MK A (center A)) H
+
+
+definition is_trunc_is_contr_fiber [instance] [priority 900] (n : ℕ₋₂) {A B : Type} (f : A → B)
+  (b : B) [is_trunc n A] [is_trunc n B] : is_trunc n (is_contr (fiber f b)) :=
+begin
+  cases n,
+  { apply is_contr_of_inhabited_prop, apply is_contr_fun_of_is_equiv,
+    apply is_equiv_of_is_contr },
+  { apply is_trunc_succ_of_is_prop }
+end
+
 end is_trunc
 
 namespace is_conn