diff --git a/choice.hlean b/choice.hlean
index df700ba..ea2e52b 100644
--- a/choice.hlean
+++ b/choice.hlean
@@ -3,26 +3,35 @@ import types.trunc types.sum types.lift types.unit
 open pi prod sum unit bool trunc is_trunc is_equiv eq equiv lift pointed
 
 namespace choice
+universe variables u v
 
 -- 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} [class] (n : ℕ₋₂) (X : Type.{u}) : Type.{u+1} :=
-Π(A : X → Type.{u}), is_equiv (unchoose n A)
+definition has_choice [class] (n : ℕ₋₂) (X : Type.{u}) : Type.{max u (v+1)} :=
+Π(A : X → Type.{v}), 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)) :=
+definition choice_equiv [constructor] {n : ℕ₋₂} {X : Type} [H : has_choice.{u v} n X]
+  (A : X → Type) : 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 :=
+definition has_choice_of_succ (X : Type) (H : Πk, has_choice.{_ v} (k.+1) X) (n : ℕ₋₂) :
+  has_choice.{_ v} n X :=
 begin
   cases n with n,
   { intro A, exact is_equiv_of_is_contr _ _ _ },
   { exact H n }
 end
 
-definition has_choice_empty [instance] (n : ℕ₋₂) : has_choice n empty :=
+/- currently we prove it using univalence, which means we cannot apply it to lift. -/
+definition has_choice_equiv_closed (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (hA : has_choice.{u v} n B)
+  : has_choice.{u v} n A :=
+begin
+  induction f using rec_on_ua_idp, exact hA
+end
+
+definition has_choice_empty [instance] (n : ℕ₋₂) : has_choice.{_ v} n empty :=
 begin
   intro A, fapply adjointify,
   { intro f, apply tr, intro x, induction x },
@@ -30,7 +39,7 @@ begin
   { intro g, induction g with g, apply ap tr, apply eq_of_homotopy, intro x, induction x }
 end
 
-definition has_choice_unit [instance] : Πn, has_choice n unit :=
+definition has_choice_unit [instance] : Πn, has_choice.{_ v} n unit :=
 begin
   intro n A, fapply adjointify,
   { intro f, induction f ⋆ with a, apply tr, intro u, induction u, exact a },
@@ -40,8 +49,8 @@ begin
     intro u, induction u, reflexivity }
 end
 
-definition has_choice_sum.{u} [instance] (n : ℕ₋₂) (A B : Type.{u})
-  [has_choice n A] [has_choice n B] : has_choice n (A ⊎ B) :=
+definition has_choice_sum [instance] (n : ℕ₋₂) (A B : Type.{u})
+  [has_choice.{_ v} n A] [has_choice.{_ v} n B] : has_choice.{_ v} n (A ⊎ B) :=
 begin
   intro P, fapply is_equiv_of_equiv_of_homotopy,
   { exact calc
@@ -54,25 +63,18 @@ begin
   { intro f, induction f, apply eq_of_homotopy, intro x, esimp, induction x with a b: reflexivity }
 end
 
-/- currently we prove it using univalence, which means we cannot apply it to lift. TODO: change -/
-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 [instance] (n : ℕ₋₂) : has_choice n bool :=
+definition has_choice_bool [instance] (n : ℕ₋₂) : has_choice.{_ v} n bool :=
 has_choice_equiv_closed n bool_equiv_unit_sum_unit _
 
-definition has_choice_lift.{u v} [instance] (n : ℕ₋₂) (A : Type) [has_choice n A] :
-  has_choice n (lift.{u v} A) :=
+definition has_choice_lift.{u'} [instance] (n : ℕ₋₂) (A : Type) [has_choice.{_ v} n A] :
+  has_choice.{_ v} n (lift.{u u'} A) :=
 sorry --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
+definition has_choice_punit [instance] (n : ℕ₋₂) : has_choice.{_ v} n punit := has_choice_unit n
+definition has_choice_pbool [instance] (n : ℕ₋₂) : has_choice.{_ v} n pbool := has_choice_bool n
+definition has_choice_plift [instance] (n : ℕ₋₂) (A : Type*) [has_choice.{_ v} n A]
+  : has_choice.{_ v} n (plift A) := has_choice_lift n A
+definition has_choice_psum [instance] (n : ℕ₋₂) (A B : Type*) [has_choice.{_ v} n A] [has_choice.{_ v} n B]
+  : has_choice.{_ v} n (psum A B) := has_choice_sum n A B
 
 end choice
diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean
index 5ce09d2..6c485c2 100644
--- a/cohomology/basic.hlean
+++ b/cohomology/basic.hlean
@@ -133,7 +133,7 @@ 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
 
-notation `H^≃` n `[`:0 e:0 `, ` Y:0 `]`:0   := cohomology_isomorphism e Y n
+notation `H^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := cohomology_isomorphism e Y n
 
 definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : H^n[X,Y]) :
   H^≃n[pequiv.refl X, Y] x = x :=
@@ -149,6 +149,8 @@ definition unreduced_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (Y : sp
   uH^n[X, Y] ≃g uH^n[X', Y] :=
 cohomology_isomorphism (add_point_pequiv f) Y n
 
+notation `uH^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := unreduced_cohomology_isomorphism e Y n
+
 definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n)
   (n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] :=
 cohomology_isomorphism_right X₊ e n
@@ -157,6 +159,8 @@ definition unreduced_ordinary_cohomology_isomorphism {X X' : Type} (f : X' ≃ X
   (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X', G] :=
 unreduced_cohomology_isomorphism f (EM_spectrum G) n
 
+notation `uoH^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := unreduced_ordinary_cohomology_isomorphism e Y n
+
 definition unreduced_ordinary_cohomology_isomorphism_right (X : Type) {G G' : AbGroup}
   (e : G ≃g G') (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X, G'] :=
 unreduced_cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
@@ -355,10 +359,10 @@ definition cohomology_punit (Y : spectrum) (n : ℤ) :
   is_contr (H^n[punit, Y]) :=
 @is_trunc_trunc_of_is_trunc _ _ _ !is_contr_punit_pmap
 
-definition cohomology_wedge (X X' : Type*) (Y : spectrum) (n : ℤ) :
+definition cohomology_wedge.{u} (X X' : Type*) (Y : spectrum.{u}) (n : ℤ) :
   H^n[wedge X X', Y] ≃g H^n[X, Y] ×ag H^n[X', Y] :=
 H^≃n[(wedge_pequiv_fwedge X X')⁻¹ᵉ*, Y] ⬝g
-cohomology_fwedge (has_choice_pbool 0) _ _ _ ⬝g
+cohomology_fwedge (has_choice_bool 0) _ _ _ ⬝g
 Group_pi_isomorphism_Group_pi erfl begin intro b, induction b: reflexivity end ⬝g
 (product_isomorphism_Group_pi H^n[X, Y] H^n[X', Y])⁻¹ᵍ ⬝g
 proof !isomorphism.refl qed
@@ -406,6 +410,10 @@ is_contr_equiv_closed_rev
   (equiv_of_isomorphism (unreduced_ordinary_cohomology_nonzero (sphere k) G n q))
   (ordinary_cohomology_sphere_of_neq G p)
 
+definition unreduced_ordinary_cohomology_sphere_of_neq_nat (G : AbGroup) {n k : ℕ} (p : n ≠ k)
+  (q : n ≠ 0) : is_contr (uoH^n[sphere k, G]) :=
+unreduced_ordinary_cohomology_sphere_of_neq G (λh, p (of_nat.inj h)) (λh, q (of_nat.inj h))
+
 theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum)
   (H : is_contr (Y n)) : is_contr (H^n[X, Y]) :=
 begin
@@ -454,7 +462,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
   (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
     Hsusp n X ∘ Hh (succ n) (susp_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 →
+  (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice.{u u} 0 I →
     is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
 structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean
index 416e387..63e8a90 100644
--- a/homotopy/fwedge.hlean
+++ b/homotopy/fwedge.hlean
@@ -246,15 +246,11 @@ sorry
     { reflexivity }
   end
 
-
-
-
   open trunc
-  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) :=
+  definition trunc_fwedge_pmap_equiv.{u v w} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
+    (F : I → pType.{v}) (X : pType.{w}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
   trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv (λi, F i →* X)
 
-
   definition fwedge_functor [constructor] {I : Type} {F F' : I → Type*} (f : Π i, F i →* F' i)
     : ⋁ F →* ⋁ F' := fwedge_pmap (λ i, pinl i ∘* f i)