chore(hott/init/axioms) remove +1 in universe levels from axioms

hott/init/axioms/funext_from_ua.hlean

@@ -11,7 +11,7 @@ open eq function prod sigma truncation equiv is_equiv unit
 context
   universe variables l
 
-  protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
+  protected theorem ua_isequiv_postcompose {A B : Type.{l}} {C : Type}
       {w : A → B} {H0 : is_equiv w} : is_equiv (@compose C A B w) :=
     let w' := equiv.mk w H0 in
     let eqinv : A = B := ((@is_equiv.inv _ _ _ (ua_is_equiv A B)) w') in
@@ -25,7 +25,7 @@ context
           from inv_eq eq' w' eqretr,
         have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
           from (λ p,
-            (@eq.rec_on Type.{l+1} A
+            (@eq.rec_on Type.{l} A
               (λ B' p', Π (x' : C → B'), (to_fun (equiv_path p'))
                 ∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') = x')
               B p (λ x', idp))
@@ -77,7 +77,7 @@ context
             (λ xy, prod.rec_on xy
               (λ b c p, eq.rec_on p idp))))
 
-  theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}}
+  theorem nondep_funext_from_ua {A : Type} {B : Type}
       : Π {f g : A → B}, f ∼ g → f = g :=
     (λ (f g : A → B) (p : f ∼ g),
         let d := λ (x : A), sigma.mk (f x , f x) idp in
@@ -103,8 +103,7 @@ end
 
 -- Now we use this to prove weak funext, which as we know
 -- implies (with dependent eta) also the strong dependent funext.
-universe variables l k
-theorem weak_funext_from_ua : weak_funext.{l+1 k+1} :=
+theorem weak_funext_from_ua : weak_funext :=
   (λ (A : Type) (P : A → Type) allcontr,
     let U := (λ (x : A), unit) in
   have pequiv : Π (x : A), P x ≃ U x,

hott/init/axioms/funext_varieties.hlean

@@ -21,8 +21,8 @@ definition naive_funext :=
   Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
 
 -- Weak funext says that a product of contractible types is contractible.
-definition weak_funext.{l k} :=
-  Π {A : Type.{l}} (P : A → Type.{k}) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
+definition weak_funext :=
+  Π {A : Type} (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
 
 -- The obvious implications are Funext -> NaiveFunext -> WeakFunext
 -- TODO: Get class inference to work locally
@@ -53,7 +53,7 @@ definition weak_funext_from_naive_funext : naive_funext → weak_funext :=
 
 context
   universes l k
-  parameters (wf : weak_funext.{l+1 k+1}) {A : Type.{l+1}} {B : A → Type.{k+1}} (f : Π x, B x)
+  parameters (wf : weak_funext.{l k}) {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
 
   protected definition idhtpy : f ∼ f := (λ x, idp)
 
@@ -93,7 +93,7 @@ end
 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
 universe variables l k
 
-theorem funext_from_weak_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+1} :=
+theorem funext_from_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
   funext.mk (λ A B f g,
     let eq_to_f := (λ g' x, f = g') in
     let sim2path := htpy_ind _ f eq_to_f idp in