fix definition of spectrum cohomology, and prove that spectrum cohomology forms a cohomology theory

algebra/arrow_group.hlean

@@ -1,14 +1,104 @@
 
-import algebra.group_theory ..move_to_lib
-open pi pointed algebra group eq equiv is_trunc
+import algebra.group_theory ..move_to_lib eq2
+open pi pointed algebra group eq equiv is_trunc trunc
 
 namespace group
 
+  -- definition pmap_mul [constructor] {A B : Type*} [inf_pgroup B] (f g : A →* B) : A →* B :=
+  -- pmap.mk (λa, f a * g a) (ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul)
+
+  -- definition pmap_inv [constructor] {A B : Type*} [inf_pgroup B] (f : A →* B) : A →* B :=
+  -- pmap.mk (λa, (f a)⁻¹) (ap inv (respect_pt f) ⬝ !one_inv)
+
+  definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B :=
+  pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con)
+
+  definition pmap_inv [constructor] {A B : Type*} (f : A →* Ω B) : A →* Ω B :=
+  pmap.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻²
+
+  definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) :=
+  begin
+    fapply inf_group.mk,
+    { exact pmap_mul },
+    { intro f g h, fapply pmap_eq,
+      { intro a, exact con.assoc (f a) (g a) (h a) },
+      { rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }},
+    { apply pconst },
+    { intros f, fapply pmap_eq,
+      { intro a, exact one_mul (f a) },
+      { esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
+    { intros f, fapply pmap_eq,
+      { intro a, exact mul_one (f a) },
+      { reflexivity }},
+    { exact pmap_inv },
+    { intro f, fapply pmap_eq,
+      { intro a, exact con.left_inv (f a) },
+      { exact !con_left_inv_idp⁻¹ }},
+  end
+
+  definition group_trunc_pmap [constructor] [instance] (A B : Type*) : group (trunc 0 (A →* Ω B)) :=
+  !trunc_group
+
+  definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group :=
+  Group.mk (trunc 0 (A →* Ω (Ω B))) _
+
+  definition Group_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) :
+    Group_trunc_pmap A B →g Group_trunc_pmap A' B :=
+  begin
+    fapply homomorphism.mk,
+    { apply trunc_functor, intro g, exact g ∘* f},
+    { intro g h, induction g with g, induction h with h, apply ap tr,
+      fapply pmap_eq,
+      { intro a, reflexivity },
+      { refine _ ⬝ !idp_con⁻¹,
+        refine whisker_right _ !ap_con_fn ⬝ _, apply con2_con_con2 }}
+  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
+    induction f with f, apply ap tr, apply eq_of_phomotopy, apply pcompose_pid
+  end
+
+  definition Group_trunc_pmap_pconst [constructor] {A A' B : Type*} (f : Group_trunc_pmap A B) :
+    Group_trunc_pmap_homomorphism (pconst A' A) f = 1 :=
+  begin
+    induction f with f, apply ap tr, apply eq_of_phomotopy, apply pcompose_pconst
+  end
+
+  definition Group_trunc_pmap_pcompose [constructor] {A A' A'' B : Type*} (f : A' →* A) (f' : A'' →* A')
+    (g : Group_trunc_pmap A B) : Group_trunc_pmap_homomorphism (f ∘* f') g =
+    Group_trunc_pmap_homomorphism f' (Group_trunc_pmap_homomorphism f g) :=
+  begin
+    induction g with g, apply ap tr, apply eq_of_phomotopy, exact !passoc⁻¹*
+  end
+
+  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))
+  end
+
+  definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : ab_inf_group (A →* Ω (Ω B)) :=
+  ⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm :=
+    begin
+      intro f g, fapply pmap_eq,
+      { intro a, exact eckmann_hilton (f a) (g a) },
+      { rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
+    end⦄
+
+  definition ab_group_trunc_pmap [constructor] [instance] (A B : Type*) :
+    ab_group (trunc 0 (A →* Ω (Ω B))) :=
+  !trunc_ab_group
+
+  definition AbGroup_trunc_pmap [reducible] [constructor] (A B : Type*) : AbGroup :=
+  AbGroup.mk (trunc 0 (A →* Ω (Ω B))) _
+
   /- Group of functions whose codomain is a group -/
-  definition group_arrow [instance] (A B : Type) [group B] : group (A → B) :=
+  definition group_pi [instance] [constructor] {A : Type} (P : A → Type) [Πa, group (P a)] : group (Πa, P a) :=
   begin
     fapply group.mk,
-    { apply is_trunc_arrow },
+    { apply is_trunc_pi },
     { intro f g a, exact f a * g a },
     { intros, apply eq_of_homotopy, intro a, apply mul.assoc },
     { intro a, exact 1 },
@@ -18,43 +108,78 @@ namespace group
     { intros, apply eq_of_homotopy, intro a, apply mul.left_inv }
   end
 
-  definition Group_arrow (A : Type) (G : Group) : Group :=
-  Group.mk (A → G) _
+  definition Group_pi [constructor] {A : Type} (P : A → Group) : Group :=
+  Group.mk (Πa, P a) _
 
-  definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) :=
-  ⦃ab_group, group_arrow A B,
-     mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄
+  /- we use superscript in the following notation, because otherwise we can never write something
+     like `Πg h : G, _` anymore -/
 
-  definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup :=
-  AbGroup.mk (A → G) _
+  notation `Πᵍ` binders `, ` r:(scoped P, Group_pi P) := r
 
-  definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) :=
+  definition Group_pi_intro [constructor] {A : Type} {G : Group} {P : A → Group} (f : Πa, G →g P a)
+    : G →g Πᵍ a, P a :=
   begin
-    fapply pgroup.mk,
-    { apply is_trunc_pmap },
-    { intro f g, apply pmap.mk (λa, f a * g a),
-      exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul },
-    { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc },
-    { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt },
-    { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul },
-    { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one },
-    { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv }
+    fconstructor,
+    { intro g a, exact f a g },
+    { intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h }
   end
 
-  definition Group_pmap (A : Type*) (G : Group) : Group :=
-  Group_of_pgroup (ppmap A (pType_of_Group G))
+  -- definition AbGroup_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) :
+  --   AbGroup_trunc_pmap A B →g AbGroup_trunc_pmap A' B :=
+  -- Group_trunc_pmap_homomorphism f
 
-  definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup :=
-  AbGroup.mk (A →* pType_of_Group G)
-  ⦃ ab_group, Group.struct (Group_pmap A G),
-    mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄
 
-  definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) :
-    Group_pmap A G →g Group_pmap A' G :=
-  begin
-    fapply homomorphism.mk,
-    { intro g, exact g ∘* f},
-    { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity }
-  end
+  /- Group of functions whose codomain is a group -/
+  -- definition group_arrow [instance] (A B : Type) [group B] : group (A → B) :=
+  -- begin
+  --   fapply group.mk,
+  --   { apply is_trunc_arrow },
+  --   { intro f g a, exact f a * g a },
+  --   { intros, apply eq_of_homotopy, intro a, apply mul.assoc },
+  --   { intro a, exact 1 },
+  --   { intros, apply eq_of_homotopy, intro a, apply one_mul },
+  --   { intros, apply eq_of_homotopy, intro a, apply mul_one },
+  --   { intro f a, exact (f a)⁻¹ },
+  --   { intros, apply eq_of_homotopy, intro a, apply mul.left_inv }
+  -- end
+
+  -- definition Group_arrow (A : Type) (G : Group) : Group :=
+  -- Group.mk (A → G) _
+
+  -- definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) :=
+  -- ⦃ab_group, group_arrow A B,
+  --    mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄
+
+  -- definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup :=
+  -- AbGroup.mk (A → G) _
+
+  -- definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) :=
+  -- begin
+  --   fapply pgroup.mk,
+  --   { apply is_trunc_pmap },
+  --   { intro f g, apply pmap.mk (λa, f a * g a),
+  --     exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul },
+  --   { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc },
+  --   { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt },
+  --   { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul },
+  --   { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one },
+  --   { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv }
+  -- end
+
+  -- definition Group_pmap (A : Type*) (G : Group) : Group :=
+  -- Group_of_pgroup (ppmap A (pType_of_Group G))
+
+  -- definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup :=
+  -- AbGroup.mk (A →* pType_of_Group G)
+  -- ⦃ ab_group, Group.struct (Group_pmap A G),
+  --   mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄
+
+  -- definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) :
+  --   Group_pmap A G →g Group_pmap A' G :=
+  -- begin
+  --   fapply homomorphism.mk,
+  --   { intro g, exact g ∘* f},
+  --   { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity }
+  -- end
 
 end group

choice.hlean

@@ -0,0 +1,77 @@
+import types.trunc types.sum
+
+open pi prod sum unit bool trunc is_trunc is_equiv eq equiv
+
+namespace choice
+
+-- the following brilliant name is from Agda
+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} :=
+Π(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})
+  : trunc n (Πx, A x) ≃ (Πx, trunc n (A x)) :=
+equiv.mk _ (H A)
+
+definition has_choice_of_succ (X : Type) (H : Πk, has_choice (k.+1) X) (n : ℕ₋₂) : has_choice n X :=
+begin
+  cases n with n,
+  { intro A, apply is_equiv_of_is_contr },
+  { exact H n }
+end
+
+definition has_choice_empty (n : ℕ₋₂) : has_choice n empty :=
+begin
+  intro A, fapply adjointify,
+  { intro f, apply tr, intro x, induction x },
+  { intro f, apply eq_of_homotopy, intro x, induction x },
+  { 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 :=
+begin
+  intro n A, fapply adjointify,
+  { intro f, induction f ⋆ with a, apply tr, intro u, induction u, exact a },
+  { intro f, apply eq_of_homotopy, intro u, induction u, esimp, generalize f ⋆, intro a,
+    induction a, reflexivity },
+  { intro g, induction g with g, apply ap tr, apply eq_of_homotopy,
+    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) :=
+begin
+  intro P, fapply is_equiv_of_equiv_of_homotopy,
+  { exact calc
+     trunc n (Πx, P x) ≃ trunc n ((Πa, P (inl a)) × Πb, P (inr b))
+       : 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 _)
+     ... ≃ Π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
+
+/- currently we prove it using univalence -/
+definition has_choice_equiv_closed.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A ≃ B) (hA : has_choice n B)
+  : has_choice n A :=
+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))
+
+end choice

colim.hlean

@@ -10,7 +10,11 @@ namespace seq_colim
 
   definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
     : inclusion f (Point (X n)) = Point (pseq_colim f) :=
-  by induction n with n p; reflexivity; exact (ap (sι f) !respect_pt)⁻¹ ⬝ !glue ⬝ p
+  begin
+    induction n with n p,
+      reflexivity,
+      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ !glue ⬝ p
+  end
 
   definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
     : X n →* pseq_colim f :=
@@ -390,7 +394,7 @@ namespace seq_colim
     apply whisker_left,
     rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'],
     note s := (eq_top_of_square (natural_square_tr
-      (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹,
+      (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹ᵖ,
     rewrite [inv_con_inv_right at s, -con.assoc at s], exact s
   end
 

homotopy/cohomology.hlean

@@ -6,9 +6,83 @@ Authors: Floris van Doorn
 Reduced cohomology
 -/
 
-import algebra.arrow_group .spectrum homotopy.EM
+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
+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
+
+-- TODO: move
+structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → image f b)
+
+definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
+is_exact f g
+
+definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
+  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
+is_exact.mk H₁ H₂
+
+definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+  (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
+begin
+  constructor,
+  { intro a, esimp, induction a with a,
+    exact ap tr (is_exact_t.im_in_ker H a) },
+  { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q,
+    induction is_exact_t.ker_in_im H b q with a r,
+    exact image.mk (tr a) (ap tr r) }
+end
+
+definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C}
+  (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
+begin
+  induction p using homotopy.rec_on_idp,
+  induction q using homotopy.rec_on_idp,
+  assumption
+end
+
+-- move to arrow group
+
+definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
+  Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) :=
+begin
+  fconstructor,
+  { intro p, esimp,
+    refine ap1_gen_con_left p (respect_pt f) (respect_pt f)
+             (respect_pt g) (respect_pt g) ⬝ _,
+    refine !whisker_right_idp ◾ !whisker_left_idp2, },
+  { refine !con.assoc ⬝ _,
+    refine _ ◾ idp ⬝ _, rotate 1,
+    rexact ap1_gen_con_left_idp (respect_pt f) (respect_pt g), esimp,
+    refine !con.assoc ⬝ _,
+    apply whisker_left, apply inv_con_eq_idp,
+    refine !con2_con_con2 ⬝ ap011 concat2 _ _:
+      refine eq_of_square (!natural_square ⬝hp !ap_id) ⬝ !con_idp }
+end
+
+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,
+  { intro p, reflexivity },
+  { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _,
+    refine !ap_eq_ap011⁻¹ }
+end
+
+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,
+  { intro p, exact ap1_con2 h (f p) (g p) },
+  { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _,
+    refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _,
+    refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp }
+end
+
+definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) :
+  loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) :=
+pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose
 
 namespace cohomology
 
@@ -16,7 +90,7 @@ definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
 spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
 
 definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
-AbGroup_pmap X (πag[2] (Y (2+n)))
+AbGroup_trunc_pmap X (Y (n+2))
 
 definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
 cohomology X (EM_spectrum G) n
@@ -33,33 +107,123 @@ notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n
 definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup :=
 cohomology X₊ Y n
 
-definition cohomology_homomorphism [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
+/- functoriality -/
+
+definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
   (n : ℤ) : cohomology X Y n →g cohomology X' Y n :=
-Group_pmap_homomorphism f (πag[2] (Y (2+n)))
+Group_trunc_pmap_homomorphism f
 
-definition cohomology_homomorphism_id (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
-  cohomology_homomorphism (pid X) Y n f ~* f :=
-!pcompose_pid
+definition cohomology_functor_pid (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
+  cohomology_functor (pid X) Y n f = f :=
+!Group_trunc_pmap_pid
 
-definition cohomology_homomorphism_compose {X X' X'' : Type*} (g : X'' →* X') (f : X' →* X)
-  (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_homomorphism (f ∘* g) Y n h ~*
-  cohomology_homomorphism g Y n (cohomology_homomorphism f Y n h) :=
-!passoc⁻¹*
+definition cohomology_functor_pcompose {X X' X'' : Type*} (f : X' →* X) (g : X'' →* X')
+  (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_functor (f ∘* g) Y n h =
+  cohomology_functor g Y n (cohomology_functor f Y n h) :=
+!Group_trunc_pmap_pcompose
+
+definition cohomology_functor_phomotopy {X X' : Type*} {f g : X' →* X} (p : f ~* g)
+  (Y : spectrum) (n : ℤ) : cohomology_functor f Y n ~ cohomology_functor g Y n :=
+Group_trunc_pmap_phomotopy p
+
+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
+
+/- suspension axiom -/
+
+definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
+  Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) :=
+begin
+  apply loopn_pequiv_loopn 2,
+  exact loop_pequiv_loop (pequiv_of_eq (ap Y (add_comm_right n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ*
+end
+
+definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) :
+  psusp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) :=
+calc
+  psusp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : psusp_adjoint_loop_unpointed
+    ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left
+                                                  (cohomology_psusp_2 Y n))
+
+definition cohomology_psusp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ}
+  (f g : psusp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_psusp_1 X Y n (pmap_mul f g) ~*
+  pmap_mul (cohomology_psusp_1 X Y n f) (cohomology_psusp_1 X Y n g) :=
+begin
+  unfold [cohomology_psusp_1],
+  refine pwhisker_left _ !loop_psusp_intro_pmap_mul ⬝* _,
+  apply pcompose_pmap_mul
+end
+
+definition cohomology_psusp_equiv (X : Type*) (Y : spectrum) (n : ℤ) :
+  H^n+1[psusp X, Y] ≃ H^n[X, Y] :=
+trunc_equiv_trunc _ (cohomology_psusp_1 X Y n)
+
+definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) :
+  H^n+1[psusp X, Y] ≃g H^n[X, Y] :=
+isomorphism_of_equiv (cohomology_psusp_equiv X Y n)
+  begin
+    intro f₁ f₂, induction f₁ with f₁, induction f₂ with f₂,
+    apply ap tr, apply eq_of_phomotopy, exact cohomology_psusp_1_pmap_mul f₁ f₂
+  end
+
+definition cohomology_psusp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
+  cohomology_psusp X Y n ∘ cohomology_functor (psusp_functor f) Y (n+1) ~
+  cohomology_functor f Y n ∘ cohomology_psusp X' Y n :=
+begin
+  refine (trunc_functor_compose _ _ _)⁻¹ʰᵗʸ ⬝hty _ ⬝hty trunc_functor_compose _ _ _,
+  apply trunc_functor_homotopy, intro g,
+  apply eq_of_phomotopy, refine _ ⬝* !passoc⁻¹*, apply pwhisker_left,
+  apply loop_psusp_intro_natural
+end
+
+/- exactness -/
+
+definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
+  is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
+is_exact_trunc_functor (cofiber_exact f)
+
+/- additivity -/
+
+definition additive_hom [constructor] {I : Type} (X : I → Type*) (Y : spectrum) (n : ℤ) :
+  H^n[⋁X, Y] →g Πᵍ i, H^n[X i, Y] :=
+Group_pi_intro (λi, cohomology_functor (pinl i) Y n)
+
+definition additive_equiv.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
+  (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] :=
+trunc_fwedge_pmap_equiv H X (Ω[2] (Y (n+2)))
+
+definition additive {I : Type} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) (n : ℤ) :
+  is_equiv (additive_hom X Y n) :=
+is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction f, reflexivity end
+
+/- 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 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_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)))
+
+structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
+ (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (H n (plift pbool)))
+
+definition cohomology_theory_spectrum [constructor] (Y : spectrum) : cohomology_theory :=
+cohomology_theory.mk
+  (λn A, H^n[A, Y])
+  (λn A B f, cohomology_functor f Y n)
+  (λ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)
+  (λn A B f, cohomology_psusp_natural f Y n)
+  (λn A B f, cohomology_exact f Y n)
+  (λn I A H, additive H A Y n)
 
 end cohomology
-
-exit
-definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) :
-  H^n+1[psusp X, Y] ≃ H^n[X, Y] :=
-calc
-  H^n+1[psusp X, Y] ≃ psusp X →* πg[2] (Y (2+(n+1))) : by reflexivity
-  ... ≃ X →* Ω (πg[2] (Y (2+(n+1)))) : psusp_adjoint_loop_unpointed
---  ... ≃ X →* πg[3] (Y (2+(n+1))) : _
---... ≃ X →* πag[3] (Y ((2+n)+1)) : _
-  ... ≃ X →* πg[2] (Y (2+n)) :
-    begin
-      refine equiv_of_pequiv (pequiv_ppcompose_left _),
-      refine !homotopy_group_succ_o ⬝ _,
-      exact sorry --refine _ ⬝e* _ ⬝e* _
-    end
-  ... ≃ H^n[X, Y] : by reflexivity

homotopy/fwedge.hlean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2016 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob von Raumer, Ulrik Buchholtz
+
+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
+
+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 ⋆
+definition fwedge [constructor] {I : Type} (F : I → Type*) : Type* := pointed.MK (fwedge' F) pt'
+
+notation `⋁` := fwedge
+
+namespace fwedge
+  variables {I : Type} {F : I → Type*}
+
+  definition il {i : I} (x : F i) : ⋁F := inl ⟨i, x⟩
+  definition inl (i : I) (x : F i) : ⋁F := il x
+  definition pinl [constructor] (i : I) : F i →* ⋁F := pmap.mk (inl i) (glue i)
+  definition glue (i : I) : inl i pt = pt :> ⋁ F := glue i
+
+  protected definition rec {P : ⋁F → Type} (Pinl : Π(i : I) (x : F i), P (il x))
+    (Pinr : P pt) (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (y : fwedge' F) : P y :=
+  begin induction y, induction x, apply Pinl, induction x, apply Pinr, apply Pglue end
+
+  protected definition elim {P : Type} (Pinl : Π(i : I) (x : F i), P)
+    (Pinr : P) (Pglue : Πi, Pinl i pt = Pinr) (y : fwedge' F) : P :=
+  begin induction y with x u, induction x with i x, exact Pinl i x, induction u, apply Pinr, apply Pglue end
+
+  protected definition elim_glue {P : Type} {Pinl : Π(i : I) (x : F i), P}
+    {Pinr : P} (Pglue : Πi, Pinl i pt = Pinr) (i : I)
+    : ap (fwedge.elim Pinl Pinr Pglue) (fwedge.glue i) = Pglue i :=
+  !pushout.elim_glue
+
+  protected definition rec_glue {P : ⋁F → Type} {Pinl : Π(i : I) (x : F i), P (il x)}
+    {Pinr : P pt} (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (i : I)
+    : apd (fwedge.rec Pinl Pinr Pglue) (fwedge.glue i) = Pglue i :=
+  !pushout.rec_glue
+
+end fwedge
+
+attribute fwedge.rec fwedge.elim [recursor 7] [unfold 7]
+attribute fwedge.il fwedge.inl [constructor]
+
+namespace fwedge
+
+  definition fwedge_of_pwedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) :=
+  begin
+    induction x with a b,
+    { exact inl ff a },
+    { exact inl tt b },
+    { exact glue ff ⬝ (glue tt)⁻¹ }
+  end
+
+  definition pwedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B :=
+  begin
+    induction x with b x b,
+    { induction b, exact pushout.inl x, exact pushout.inr x },
+    { exact pushout.inr pt },
+    { induction b, exact pushout.glue ⋆, reflexivity }
+  end
+
+  definition pwedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact fwedge_of_pwedge },
+      { exact pwedge_of_fwedge },
+      { exact abstract begin intro x, induction x with b x b,
+        { induction b: reflexivity },
+        { exact glue tt },
+        { apply eq_pathover_id_right,
+          refine ap_compose fwedge_of_pwedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+          induction b, exact !elim_glue ⬝ph whisker_bl _ hrfl, apply square_of_eq idp }
+        end end },
+      { exact abstract begin intro x, induction x with a b,
+        { reflexivity },
+        { reflexivity },
+        { apply eq_pathover_id_right,
+          refine ap_compose pwedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝
+                 !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) ⬝ph _, exact hrfl } end end}},
+    { exact glue ff }
+  end
+
+  definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
+  begin
+    fconstructor,
+    { intro x, induction x,
+        exact f i x,
+        exact pt,
+        exact respect_pt (f i) },
+    { reflexivity }
+  end
+
+  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,
+    { reflexivity },
+    { exact !idp_con ⬝ !fwedge.elim_glue⁻¹ }
+  end
+
+  definition fwedge_pmap_eta [constructor] {I : Type} {F : I → Type*} {X : Type*} (g : ⋁F →* X) :
+    fwedge_pmap (λi, g ∘* pinl i) ~* g :=
+  begin
+    fconstructor,
+    { intro x, induction x,
+        reflexivity,
+        exact (respect_pt g)⁻¹,
+        apply eq_pathover, refine !elim_glue ⬝ph _, apply whisker_lb, exact hrfl },
+    { exact con.left_inv (respect_pt g) }
+  end
+
+  definition fwedge_pmap_equiv [constructor] {I : Type} (F : I → Type*) (X : Type*) :
+    ⋁F →* X ≃ Πi, F i →* X :=
+  begin
+    fapply equiv.MK,
+    { intro g i, exact g ∘* pinl i },
+    { exact fwedge_pmap },
+    { intro f, apply eq_of_homotopy, intro i, apply eq_of_phomotopy, apply fwedge_pmap_beta f i },
+    { intro g, apply eq_of_phomotopy, exact fwedge_pmap_eta g }
+  end
+
+  definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
+    (F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
+  trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv H (λi, F i →* X)
+
+end fwedge

homotopy/pushout.hlean

@@ -1,7 +1,7 @@
 
 import ..move_to_lib
 
-open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool
+open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber
 
 namespace pushout
 
@@ -268,43 +268,43 @@ namespace pushout
   /- pushout where one map is constant is a cofiber -/
 
   definition pushout_const_equiv_to [unfold 6] {A B C : Type} {f : A → B} {c₀ : C}
-    (x : pushout (const A c₀) f) : cofiber (sum_functor f (const unit c₀)) :=
+    (x : pushout f (const A c₀)) : cofiber (sum_functor f (const unit c₀)) :=
   begin
-    induction x with c b a,
-    { exact inr (sum.inr c) },
-    { exact inr (sum.inl b) },
-    { exact (glue (sum.inr ⋆))⁻¹ ⬝ glue (sum.inl a) }
+    induction x with b c a,
+    { exact !cod (sum.inl b) },
+    { exact !cod (sum.inr c) },
+    { exact glue (sum.inl a) ⬝ (glue (sum.inr ⋆))⁻¹ }
   end
 
   definition pushout_const_equiv_from [unfold 6] {A B C : Type} {f : A → B} {c₀ : C}
-    (x : cofiber (sum_functor f (const unit c₀))) : pushout (const A c₀) f :=
+    (x : cofiber (sum_functor f (const unit c₀))) : pushout f (const A c₀) :=
   begin
     induction x with v v,
-    { exact inl c₀ },
-    { induction v with b c, exact inr b, exact inl c },
+    { induction v with b c, exact inl b, exact inr c },
+    { exact inr c₀ },
     { induction v with a u, exact glue a, reflexivity }
   end
 
   definition pushout_const_equiv [constructor] {A B C : Type} (f : A → B) (c₀ : C) :
-    pushout (const A c₀) f ≃ cofiber (sum_functor f (const unit c₀)) :=
+    pushout f (const A c₀) ≃ cofiber (sum_functor f (const unit c₀)) :=
   begin
     fapply equiv.MK,
     { exact pushout_const_equiv_to },
     { exact pushout_const_equiv_from },
     { intro x, induction x with v v,
-      { exact (glue (sum.inr ⋆))⁻¹ },
       { induction v with b c, reflexivity, reflexivity },
+      { exact glue (sum.inr ⋆) },
       { apply eq_pathover_id_right,
         refine ap_compose pushout_const_equiv_to _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
         induction v with a u,
-        { refine !elim_glue ⬝ph _, esimp, apply whisker_tl, exact hrfl },
-        { induction u, exact square_of_eq !con.left_inv }}},
+        { refine !elim_glue ⬝ph _, apply whisker_bl, exact hrfl },
+        { induction u, exact square_of_eq idp }}},
     { intro x, induction x with c b a,
       { reflexivity },
       { reflexivity },
       { apply eq_pathover_id_right, apply hdeg_square,
         refine ap_compose pushout_const_equiv_from _ _ ⬝ ap02 _ !elim_glue ⬝ _,
-        refine !ap_con ⬝ (!ap_inv ⬝ !elim_glue⁻²) ◾ !elim_glue ⬝ !idp_con }}
+        refine !ap_con ⬝ !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) }}
   end
 
   /- wedge is the cofiber of the map 2 -> A + B -/
@@ -320,7 +320,6 @@ namespace pushout
   definition wedge_equiv_pushout_sum [constructor] (A B : Type*) :
     wedge A B ≃ cofiber (sum_of_bool A B) :=
   begin
-    refine !pushout.symm ⬝e _,
     refine pushout_const_equiv _ _ ⬝e _,
     fapply pushout.equiv,
       exact bool_equiv_unit_sum_unit⁻¹ᵉ,
@@ -425,9 +424,9 @@ namespace pushout
   open sigma.ops
   definition cofiber_pushout_helper' {A : Type} {B : A → Type} {a₀₀ a₀₂ a₂₀ a₂₂ : A} {p₀₁ : a₀₀ = a₀₂}
     {p₁₀ : a₀₀ = a₂₀} {p₂₁ : a₂₀ = a₂₂} {p₁₂ : a₀₂ = a₂₂} {s : square p₀₁ p₂₁ p₁₀ p₁₂}
-    {b₀₀ : B a₀₀} {b₂₀ b₂₀' : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {q₁₀ : b₀₀ =[p₁₀] b₂₀}
-    {q₀₁ : b₀₀ =[p₀₁] b₀₂} {q₂₁ : b₂₀' =[p₂₁] b₂₂} {q₁₂ : b₀₂ =[p₁₂] b₂₂} :
-    Σ(r : b₂₀' = b₂₀), squareover B s q₀₁ (r ▸ q₂₁) q₁₀ q₁₂ :=
+    {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ b₂₂' : B a₂₂} {q₁₀ : b₀₀ =[p₁₀] b₂₀}
+    {q₀₁ : b₀₀ =[p₀₁] b₀₂} {q₂₁ : b₂₀ =[p₂₁] b₂₂'} {q₁₂ : b₀₂ =[p₁₂] b₂₂} :
+    Σ(r : b₂₂' = b₂₂), squareover B s q₀₁ (r ▸ q₂₁) q₁₀ q₁₂ :=
   begin
     induction s,
     induction q₀₁ using idp_rec_on,
@@ -438,29 +437,66 @@ namespace pushout
   end
 
   definition cofiber_pushout_helper {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D}
-    {P : cofiber h → Type} {Pbase : P (cofiber.base h)} {Pcod : Πd, P (cofiber.cod h d)}
-    (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b)))
-    (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c)))
+    {P : cofiber h → Type} {Pcod : Πd, P (cofiber.cod h d)} {Pbase : P (cofiber.base h)}
+    (Pgluel : Π(b : B), Pcod (h (inl b)) =[cofiber.glue (inl b)] Pbase)
+    (Pgluer : Π(c : C), Pcod (h (inr c)) =[cofiber.glue (inr c)] Pbase)
     (a : A) : Σ(p : Pbase = Pbase), squareover P (natural_square cofiber.glue (glue a))
-    (Pgluel (f a)) (p ▸ Pgluer (g a))
-    (pathover_ap P (λa, cofiber.base h) (apd (λa, Pbase) (glue a)))
-    (pathover_ap P (λa, cofiber.cod h (h a)) (apd (λa, Pcod (h a)) (glue a))) :=
+      (Pgluel (f a)) (p ▸ Pgluer (g a))
+      (pathover_ap P (λa, cofiber.cod h (h a)) (apd (λa, Pcod (h a)) (glue a)))
+      (pathover_ap P (λa, cofiber.base h) (apd (λa, Pbase) (glue a))) :=
   !cofiber_pushout_helper'
 
   definition cofiber_pushout_rec {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D}
-    {P : cofiber h → Type} (Pbase : P (cofiber.base h)) (Pcod : Πd, P (cofiber.cod h d))
-    (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b)))
-    (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c)))
+    {P : cofiber h → Type} (Pcod : Πd, P (cofiber.cod h d)) (Pbase : P (cofiber.base h))
+    (Pgluel : Π(b : B), Pcod (h (inl b)) =[cofiber.glue (inl b)] Pbase)
+    (Pgluer : Π(c : C), Pcod (h (inr c)) =[cofiber.glue (inr c)] Pbase)
     (r : C → A) (p : Πa, r (g a) = a)
     (x : cofiber h) : P x :=
   begin
     induction x with d x,
-    { exact Pbase },
     { exact Pcod d },
+    { exact Pbase },
     { induction x with b c a,
       { exact Pgluel b },
       { exact (cofiber_pushout_helper Pgluel Pgluer (r c)).1 ▸ Pgluer c },
       { apply pathover_pathover, rewrite [p a], exact (cofiber_pushout_helper Pgluel Pgluer a).2 }}
   end
 
+  /- universal property of cofiber -/
+
+  structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
+
+  definition cofiber_exact_1 {X Y Z : Type*} (f : X →* Y) (g : pcofiber f →* Z) :
+    (g ∘* pcod f) ∘* f ~* pconst X Z :=
+  !passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst
+
+  protected definition pcofiber.elim [constructor] {X Y Z : Type*} {f : X →* Y} (g : Y →* Z)
+    (p : g ∘* f ~* pconst X Z) : pcofiber f →* Z :=
+  begin
+    fapply pmap.mk,
+    { intro w, induction w with y x, exact g y, exact pt, exact p x },
+    { reflexivity }
+  end
+
+  protected definition pcofiber.elim_pcod {X Y Z : Type*} {f : X →* Y} {g : Y →* Z}
+    (p : g ∘* f ~* pconst X Z) : pcofiber.elim g p ∘* pcod f ~* g :=
+  begin
+    fapply phomotopy.mk,
+    { intro y, reflexivity },
+    { esimp, refine !idp_con ⬝ _,
+      refine _ ⬝ (!ap_con ⬝ (!ap_compose'⁻¹ ⬝ !ap_inv) ◾ !elim_glue)⁻¹,
+      apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ }
+  end
+
+  definition cofiber_exact {X Y Z : Type*} (f : X →* Y) :
+    is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
+  begin
+    constructor,
+    { intro g, apply eq_of_phomotopy, apply cofiber_exact_1 },
+    { intro g p, note q := phomotopy_of_eq p,
+      exact fiber.mk (pcofiber.elim g q) (eq_of_phomotopy (pcofiber.elim_pcod q)) }
+  end
+
 end pushout

homotopy/smash.hlean

@@ -314,7 +314,7 @@ namespace pushout
      A + B <-- 2 --> 1 -/
   definition pushout_wedge_of_sum_equiv_unit : pushout (@wedge_of_sum A B) bool_of_sum ≃ unit :=
   begin
-    refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B)
+    refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B ⬝e !pushout.symm)
              _ _ ⬝e _,
       exact erfl,
       intro x, induction x,
@@ -350,7 +350,6 @@ namespace smash
   definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) :=
   begin
     unfold [smash, cofiber, smash'], symmetry,
-    refine !pushout.symm ⬝e _,
     fapply pushout_vcompose_equiv wedge_of_sum,
     { symmetry, apply equiv_unit_of_is_contr, apply is_contr_pushout_wedge_of_sum },
     { intro x, reflexivity },
@@ -367,7 +366,7 @@ namespace smash
   definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
   begin
     apply pequiv_of_equiv (smash_equiv_cofiber A B),
-    exact (cofiber.glue pt)⁻¹
+    exact cofiber.glue pt
   end
 
   variables {A B}

homotopy/spectrum.hlean

@@ -5,8 +5,7 @@ Authors: Michael Shulman, Floris van Doorn
 
 -/
 
-import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim
-       ..pointed_pi
+import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim ..pointed_pi
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      seq_colim
 

homotopy/splice.hlean

@@ -29,7 +29,7 @@ So far, the splicing seems to be only needed for k = 3, so it seems to be suffic
 
 -/
 
-import homotopy.chain_complex ..move_to_lib
+import homotopy.chain_complex
 
 open prod prod.ops succ_str fin pointed nat algebra eq is_trunc equiv is_equiv
 

move_to_lib.hlean

@@ -3,7 +3,7 @@
 import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     is_trunc function sphere
+     is_trunc function sphere unit sum prod
 
 attribute equiv_unit_of_is_contr [constructor]
 attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructor]
@@ -13,9 +13,33 @@ attribute pushout.transpose [unfold 6]
 attribute ap_eq_apd10 [unfold 5]
 attribute eq_equiv_eq_symm [constructor]
 
+definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
+!add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
+
+namespace algebra
+  definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) :=
+  by induction H; exact _
+end algebra
 
 namespace eq
 
+  definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t}
+    (h : p = p') (h' : q = q') (h'' : r = r') :
+    square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') :=
+  by induction h; induction h'; induction h''; exact hrfl
+
+  definition con_left_inv_idp {A : Type} {x : A} {p : x = x} (q : p = idp)
+    : con.left_inv p = q⁻² ◾ q :=
+  by cases q; reflexivity
+
+  definition eckmann_hilton_con2 {A : Type} {x : A} {p p' q q': idp = idp :> x = x}
+    (h : p = p') (h' : q = q') : square (h ◾ h') (h' ◾ h) (eckmann_hilton p q) (eckmann_hilton p' q') :=
+  by induction h; induction h'; exact hrfl
+
+  definition ap_con_fn {A B : Type} {a a' : A} {b : B} (g h : A → b = b) (p : a = a') :
+    ap (λa, g a ⬝ h a) p = ap g p ◾ ap h p :=
+  by induction p; reflexivity
+
   protected definition homotopy.rfl [reducible] [unfold_full] {A B : Type} {f : A → B} : f ~ f :=
   homotopy.refl f
 
@@ -48,16 +72,6 @@ namespace eq
 
 end eq open eq
 
-namespace cofiber
-
-  -- replace the one in homotopy.cofiber, which has an superfluous argument
-  protected theorem elim_glue' {A B : Type} {f : A → B} {P : Type} (Pbase : P) (Pcod : B → P)
-    (Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A)
-    : ap (cofiber.elim Pbase Pcod Pglue) (cofiber.glue a) = Pglue a :=
-  !pushout.elim_glue
-
-end cofiber
-
 namespace wedge
   open pushout unit
   protected definition glue (A B : Type*) : inl pt = inr pt :> wedge A B :=
@@ -87,6 +101,48 @@ namespace pointed
     { apply is_set.elim }
   end
 
+  definition ap1_gen {A B : Type} (f : A → B) {a a' : A} (p : a = a')
+    {b b' : B} (q : f a = b) (q' : f a' = b') : b = b' :=
+  q⁻¹ ⬝ ap f p ⬝ q'
+
+  definition ap1_gen_con {A B : Type} (f : A → B) {a₁ a₂ a₃ : A} (p₁ : a₁ = a₂) (p₂ : a₂ = a₃)
+    {b₁ b₂ b₃ : B} (q₁ : f a₁ = b₁) (q₂ : f a₂ = b₂) (q₃ : f a₃ = b₃) :
+    ap1_gen f (p₁ ⬝ p₂) q₁ q₃ = ap1_gen f p₁ q₁ q₂ ⬝ ap1_gen f p₂ q₂ q₃ :=
+  begin induction p₂, induction q₃, induction q₂, reflexivity end
+
+  definition ap1_gen_con_natural {A B : Type} (f : A → B) {a₁ a₂ a₃ : A} {p₁ p₁' : a₁ = a₂}
+    {p₂ p₂' : a₂ = a₃}
+    {b₁ b₂ b₃ : B} (q₁ : f a₁ = b₁) (q₂ : f a₂ = b₂) (q₃ : f a₃ = b₃)
+    (r₁ : p₁ = p₁') (r₂ : p₂ = p₂') :
+      square (ap1_gen_con f p₁ p₂ q₁ q₂ q₃)
+             (ap1_gen_con f p₁' p₂' q₁ q₂ q₃)
+             (ap (λp, ap1_gen f p q₁ q₃) (r₁ ◾ r₂))
+             (ap (λp, ap1_gen f p q₁ q₂) r₁ ◾ ap (λp, ap1_gen f p q₂ q₃) r₂) :=
+  begin induction r₁, induction r₂, exact vrfl end
+
+  definition ap1_gen_con_idp {A B : Type} (f : A → B) {a : A} {b : B} (q : f a = b) :
+    ap1_gen_con f idp idp q q q ⬝ con.left_inv q ◾ con.left_inv q = con.left_inv q :=
+  by induction q; reflexivity
+
+  -- TODO: replace with ap1_con
+  definition ap1_con2 {A B : Type*} (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
+  ap1_gen_con f p q (respect_pt f) (respect_pt f) (respect_pt f)
+
+
+  definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B}
+    {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
+    (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') :
+      ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') =
+      whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') :=
+  begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end
+
+  definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B}
+    {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂}
+    (r₀ : f a = q₀) (r₁ : f' a = q₁) :
+      ap1_gen_con_left idp r₀ r₀ r₁ r₁ =
+      !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ :=
+  begin induction r₀, induction r₁, reflexivity end
+
   -- /- the pointed type of (unpointed) dependent maps -/
   -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
   -- pointed.mk' (Πa, P a)
@@ -713,6 +769,11 @@ end circle
 
 namespace susp
 
+  definition loop_psusp_intro_natural {X Y Z : Type*} (g : psusp Y →* Z) (f : X →* Y) :
+    loop_psusp_intro (g ∘* psusp_functor f) ~* loop_psusp_intro g ∘* f :=
+  pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_psusp_unit_natural⁻¹* ⬝*
+  !passoc⁻¹*
+
   definition psusp_functor_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
     psusp_functor f ~* psusp_functor g :=
   begin

pointed_pi.hlean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz
 -/
 
-import move_to_lib
+import .move_to_lib
 
 open eq pointed equiv sigma