Reduce universe variables in a number of places

theories/Algebra/AbGroups/AbelianGroup.v

@@ -256,7 +256,7 @@ Definition ab_image_in_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f}
   := grp_image_in_embedding f.
 
 (** The cokernel of a homomorphism into an abelian group. *)
-Definition ab_cokernel {G : Group} {A : AbGroup} (f : GroupHomomorphism G A)
+Definition ab_cokernel {G : Group@{u}} {A : AbGroup@{u}} (f : GroupHomomorphism G A)
   : AbGroup := QuotientAbGroup _ (grp_image f).
 
 Definition ab_cokernel_embedding {G : Group} {A : AbGroup} (f : G $-> A) `{IsEmbedding f}

theories/Algebra/AbGroups/Cyclic.v

@@ -73,4 +73,4 @@ Defined.
 
 (** The [n]-th cyclic group is the cokernel of [Z1_mul_nat n]. *)
 Definition cyclic@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u}
-  := ab_cokernel@{u u u v} (Z1_mul_nat n).
+  := ab_cokernel@{u v} (Z1_mul_nat n).

theories/Algebra/AbSES/Core.v

@@ -668,7 +668,7 @@ Proof.
     + exact (grp_kernel_quotient_iso _ o ab_image_in_embedding i).
     + intro a.
       by rapply (isinj_embedding (subgroup_incl _)).
-    + rapply conn_map_isequiv@{u u u u u}.
+    + rapply conn_map_isequiv.
 Defined.
 
 (** Conversely, given a short exact sequence [A -> E -> B], [A] is the kernel of [E -> B]. (We don't need exactness at [B], so we drop this assumption.) *)
@@ -711,7 +711,7 @@ Proof.
   - apply phomotopy_homotopy_hset.
     intros [e q]; cbn.
     exact q.
-  - rapply conn_map_isequiv@{u u u u u}.
+  - rapply conn_map_isequiv.
 Defined.
 
 (** Conversely, given a short exact sequence [A -> E -> B], [B] is the cokernel of [A -> E]. In fact, we don't need exactness at [A], so we drop this from the statement. *)
@@ -726,7 +726,7 @@ Proof.
     refine (ap _ p^ @ _).
     rapply cx_isexact.
   - apply isequiv_surj_emb.
-    1: rapply cancelR_conn_map@{u u u u u}.
+    1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.
     srapply Quotient_ind_hprop; intro x.
     srapply Quotient_ind_hprop; intro y.

theories/Algebra/AbSES/SixTerm.v

@@ -194,7 +194,7 @@ Local Definition ext_cyclic_exact@{u v w +} `{Univalence}
          o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
 Proof.
   (* we first move [equiv_Z1_hom] across the total space *)
-  apply moveL_isexact_equiv@{v v v w v v v}.
+  apply moveL_isexact_equiv@{v v v w}.
   (* now we change the left map so as to apply exactness at iii from above *)
   snrapply (isexact_homotopic_i (Tr (-1))).
   1: exact (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A o*
@@ -208,14 +208,14 @@ Proof.
     1: apply Z1_rec_beta.
     exact (ab_mul_nat_homo f n Z1_gen).
   - (* we get rid of [equiv_Z1_hom] *)
-    apply isexact_equiv_fiber@{v v v v v u v v v v v}.
+    apply isexact_equiv_fiber.
     apply isexact_ext_cyclic_ab_iii.
 Defined.
 
 (** The main result of this section. *)
 Theorem ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence}
   (n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
-  : ab_cokernel@{u u v w} (ab_mul_nat (A:=A) n)
+  : ab_cokernel@{v w} (ab_mul_nat (A:=A) n)
       $<~> ab_ext@{u v} (cyclic'@{u v} n) A.
   (* We take a large cokernel in order to apply [abses_cokernel_iso]. *)
 Proof.
@@ -225,9 +225,9 @@ Proof.
              (abses_pushout_ext E)
              (grp_iso_inverse (equiv_Z1_hom A))).
   - apply (conn_map_compose _ (grp_iso_inverse (equiv_Z1_hom A))).
-    1: rapply conn_map_isequiv@{v u u u u}.
+    1: rapply conn_map_isequiv.
     (* Coq knows that [Ext Z1 A] is contractible since [Z1] is projective, so exactness at spot iv gives us this: *)
-    exact (isconnmap_O_isexact_base_contr@{u v v v v v u u} _ _
+    exact (isconnmap_O_isexact_base_contr _ _
              (fmap (pTr 0)
                 (abses_pullback_pmap (A:=A)
                    (projection E)))).

theories/Basics/Overture.v

@@ -557,7 +557,7 @@ Arguments center A {_}.
    Next, 0-truncated means "the space of paths between any two points is a sub-singleton". Thus, two points might not have any paths between them, or they have a unique path. Such a space may have many points but it is discrete in the sense that all paths are trivial. We call such spaces "sets".
 *)
 
-Inductive trunc_index : Type :=
+Inductive trunc_index : Type0 :=
 | minus_two : trunc_index
 | trunc_S : trunc_index -> trunc_index.
 
@@ -584,7 +584,7 @@ Local Open Scope trunc_scope.
 
 (** n-truncatedness is defined by recursion on [n].  We could simply define [IsTrunc] as a fixpoint and an [Existing Class], but we want to also declare [IsTrunc] to be [simpl nomatch], so that when we say [simpl] or [cbn], [IsTrunc n.+1 A] doesn't get unfolded to [forall x y:A, IsTrunc n (x = y)].  But we also want to be able to use this equality, e.g. by proving [IsTrunc n.+1 A] starting with [intros x y], and if [IsTrunc] is a fixpoint declared as [simpl nomatch] then that doesn't work, because [intros] uses [hnf] to expose a [forall] and [hnf] respects [simpl nomatch] on fixpoints.  But we can make it work if we define the fixpoint separately as [IsTrunc_internal] and then take the class [IsTrunc] to be a definitional wrapper around it, since [hnf] is willing to unfold non-fixpoints even if they are defined as [simpl never].  This behavior of [hnf] is arguably questionable (see https://github.com/coq/coq/issues/11619), but it is useful for us here. *)
 
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type@{u}) : Type@{u} :=
   match n with
     | minus_two => Contr_internal A
     | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
@@ -695,7 +695,7 @@ Ltac path_via mid :=
 Local Set Elimination Schemes.
 
 (**  Natural numbers. *)
-Inductive nat : Type :=
+Inductive nat : Type0 :=
 | O : nat
 | S : nat -> nat.
 
@@ -721,7 +721,7 @@ Scheme Empty_ind := Induction for Empty Sort Type.
 Scheme Empty_rec := Minimality for Empty Sort Type.
 Definition Empty_rect := Empty_ind.
 
-Definition not (A:Type) : Type := A -> Empty.
+Definition not (A : Type) := A -> Empty.
 Notation "~ x" := (not x) : type_scope.
 Notation "~~ x" := (~ ~x) : type_scope.
 #[export]

theories/Classes/implementations/family_prod.v

@@ -1,6 +1,6 @@
 Require Import
   HoTT.Utf8
-  HoTT.Basics.Overture
+  HoTT.Basics.Overture Types.Unit
   HoTT.Classes.implementations.list.
 
 (** The following section implements a datatype [FamilyProd] which
@@ -32,7 +32,7 @@ Section family_prod.
       (f : ∀ i, F i → G i)
       : FamilyProd F ℓ → FamilyProd G ℓ :=
     match ℓ with
-    | nil => const tt
+    | nil => const_tt _
     | i :: ℓ' => λ '(x,s), (f i x, map_family_prod f s)
     end.
 

theories/Classes/interfaces/abstract_algebra.v

@@ -186,7 +186,7 @@ Section upper_classes.
   Class FieldCharacteristic@{j} {Aap : Apart@{i j} A} (k : nat) : Type@{j}
     := field_characteristic : forall n : nat,
         Nat.Core.lt 0 n ->
-        iff@{j j j} (forall m : nat, not@{j j} (paths@{Set} n
+        iff@{j j j} (forall m : nat, not@{j} (paths@{Set} n
                                                   (Nat.Core.mul k m)))
         (@apart A Aap (nat_iter n (1 +) 0) 0).
 

theories/Colimits/SpanPushout.v

@@ -5,7 +5,7 @@ Require Import HoTT.Basics HoTT.Colimits.Pushout.
 Section SpanPushout.
   Context {X Y : Type} (Q : X -> Y -> Type).
 
-  Definition SPushout := @Pushout {xy:X * Y & Q (fst xy) (snd xy)} X Y
+  Definition SPushout := @Pushout@{up _ _ up} (sig@{up _} (fun (xy : X * Y) => Q (fst xy) (snd xy))) X Y
                                   (fst o pr1) (snd o pr1).
   Definition spushl : X -> SPushout := pushl.
   Definition spushr : Y -> SPushout := pushr.

theories/Extensions.v

@@ -414,7 +414,7 @@ Section Extensions.
 
   (** Extendability of a family [C] along a map [f] can be detected by extendability of the constant family [C b] along the projection from the corresponding fiber of [f] to [Unit].  Note that this is *not* an if-and-only-if; the hypothesis can be genuinely stronger than the conclusion. *)
   Definition ooextendable_isnull_fibers {A B} (f : A -> B) (C : B -> Type)
-  : (forall b, ooExtendableAlong (@const (hfiber f b) Unit tt)
+  : (forall b, ooExtendableAlong (const_tt (hfiber f b))
                                  (fun _ => C b))
     -> ooExtendableAlong f C.
   Proof.
@@ -423,7 +423,7 @@ Section Extensions.
     - intros g.
       exists (fun b => (fst (orth b 1%nat) (fun x => x.2 # g x.1)).1 tt).
       intros a.
-      rewrite (path_unit tt (const tt a)).
+      rewrite (path_unit tt (const_tt _ a)).
       exact ((fst (orth (f a) 1%nat) _).2 (a ; 1)).
     - intros h k.
       apply IHn; intros b.

theories/HIT/SetCone.v

@@ -1,5 +1,5 @@
 (* -*- mode: coq; mode: visual-line -*- *)
-Require Import HoTT.Basics.
+Require Import HoTT.Basics Types.Unit.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core.
 
@@ -8,7 +8,7 @@ Require Import Truncations.Core.
 Section SetCone.
   Context {A B : HSet} (f : A -> B).
 
-  Definition setcone := Trunc 0 (Pushout f (const tt)).
+  Definition setcone := Trunc 0 (Pushout@{_ _ Set _} f (const_tt A)).
 
   Global Instance istrunc_setcone : IsHSet setcone := _.
 

theories/HIT/epi.v

@@ -56,7 +56,7 @@ Section cones.
   Proof.
     intros hepi.
     exists (setcone_point _).
-    pose (alpha1 := @pglue A B Unit f (const tt)).
+    pose (alpha1 := @pglue A B Unit f (const_tt _)).
     pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }).
     transparent assert (l : tot).
     { simple refine (tr o _ o inl; _).
@@ -83,7 +83,7 @@ Section cones.
     subst I0. simpl.
     pose (X..2) as p. simpl in p.
     rewrite (transport_precompose f _ _ X..1) in p.
-    assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const tt) pglue) _)).
+    assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const_tt _) pglue) _)).
     rewrite ap10_path_arrow in H'.
     clear p.
     (** Apparently [pose; clearbody] is only ~.8 seconds, while [pose proof] is ~4 seconds? *)

theories/Homotopy/ExactSequence.v

@@ -175,11 +175,11 @@ Proof.
 Defined.
 
 (** If the base is contractible, then [i] is [O]-connected. *)
-Definition isconnmap_O_isexact_base_contr (O : Modality) {F X Y : pType}
+Definition isconnmap_O_isexact_base_contr (O : Modality@{u}) {F X Y : pType}
   `{Contr Y} (i : F ->* X) (f : X ->* Y)
-  `{IsExact O _ _ _ i f}
+  `{IsExact@{_ _ _ u u u} O _ _ _ i f}
   : IsConnMap O i
-  := conn_map_compose O (cxfib cx_isexact) pr1.
+  := conn_map_compose@{u _ u _} O (cxfib@{u u _ _ _} cx_isexact) pr1.
 
 (** Passage across homotopies preserves exactness. *)
 Definition isexact_homotopic_i n  {F X Y : pType}

theories/Homotopy/Freudenthal.v

@@ -9,24 +9,25 @@ Require Import Homotopy.BlakersMassey.
 (** * The Freudenthal Suspension Theorem *)
 
 (** The Freudenthal suspension theorem is a fairly trivial corollary of the Blakers-Massey theorem.  The only real work is to relate the span-pushout that we used for Blakers-Massey to the naive pushout that we used to define suspension. *)
-
-Global Instance freudenthal `{Univalence} (n : trunc_index)
+Local Definition freudenthal' `{Univalence} (n : trunc_index)
            (X : Type) `{IsConnected n.+1 X}
   : IsConnMap (n +2+ n) (@merid X).
 Proof.
-  pose (blakers_massey n n (fun (u v:Unit) => X) tt tt).
-  pose (f := equiv_pushout (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
-                           (equiv_idmap Unit) (equiv_idmap Unit)
-                           (fun x : X => idpath) (fun x : X => idpath)
-        : Susp X <~> SPushout (fun (u v:Unit) => X)).
-  srefine (@cancelR_equiv_conn_map (n +2+ n) _ _ _ _
-             (equiv_ap' f North South)
-             (@conn_map_homotopic _ _ _ _ _ _
-               (blakers_massey n n (fun (u v:Unit) => X) tt tt))).
+  snrapply cancelR_equiv_conn_map.
+  2: { refine (equiv_ap' (B:=SPushout (fun (u v : Unit) => X)) _ North South).
+       exact (equiv_pushout (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
+                            (equiv_idmap Unit) (equiv_idmap Unit)
+                            (fun x : X => idpath) (fun x : X => idpath)). }
+  refine (conn_map_homotopic _ _ _ _
+                             (blakers_massey n n (fun (u v:Unit) => X) tt tt)).
   intros x.
   refine (_ @ (equiv_pushout_pglue
                  (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
                  (equiv_idmap Unit) (equiv_idmap Unit)
                  (fun x : X => idpath) (fun x : X => idpath) x)^).
   exact ((concat_p1 _ @ concat_1p _)^).
 Defined.
+
+Definition freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u}.
+
+Global Existing Instance freudenthal.

theories/Homotopy/Suspension.v

@@ -18,7 +18,7 @@ Local Open Scope path_scope.
 (* ** Definition of suspension *)
 
 (** We define the suspension of a type X as the pushout of 1 <- X -> 1 *)
-Definition Susp (X : Type) := Pushout (@const X _ tt) (const tt).
+Definition Susp (X : Type) := Pushout@{_ Set Set _} (const_tt X) (const_tt X).
 Definition North {X} : Susp X := pushl tt.
 Definition South {X} : Susp X := pushr tt.
 Definition merid {X} (x : X) : North = South := pglue x.

theories/Limits/Pullback.v

@@ -59,7 +59,7 @@ Defined.
 
 (** Pullback over [Unit] is equivalent to a product. *)
 Definition equiv_pullback_unit_prod (A B : Type)
-: Pullback (@const A Unit tt) (@const B Unit tt) <~> A * B.
+: Pullback (const_tt A) (const_tt B) <~> A * B.
 Proof.
   simple refine (equiv_adjointify _ _ _ _).
   - intros [a [b _]]; exact (a , b).

theories/Metatheory/Core.v

@@ -14,4 +14,4 @@ Definition Funext_type@{i j max} :=
 
 (** Univalence is a property of a single universe; its statement lives in a higher universe *)
 Definition Univalence_type@{i iplusone} : Type@{iplusone} :=
-  forall (A B : Type@{i}), IsEquiv (equiv_path@{i i iplusone i} A B).
+  forall (A B : Type@{i}), IsEquiv (equiv_path@{i iplusone} A B).

theories/Modalities/Accessible.v

@@ -91,7 +91,7 @@ End IsNull_Internal.
 (** A central fact: if a type [X] is null for all the fibers of a map [f], then it is [f]-local.  (NB: the converse is *not* generally true.)  TODO: Should this go in [Extensions]? *)
 Definition extendable_isnull_fibers (n : nat)
            {A B} (f : A -> B) (C : B -> Type)
-: (forall b, ooExtendableAlong (@const (hfiber f b) Unit tt)
+: (forall b, ooExtendableAlong (const_tt (hfiber f b))
                                (fun _ => C b))
   -> ExtendableAlong n f C.
 Proof.
@@ -100,15 +100,15 @@ Proof.
   - intros g.
     exists (fun b => (fst (null b 1%nat) (fun x => x.2 # g x.1)).1 tt).
     intros a.
-    rewrite (path_unit tt (const tt a)).
+    rewrite (path_unit tt (const_tt _ a)).
     exact ((fst (null (f a) 1%nat) _).2 (a ; 1)).
   - intros h k.
     apply IHn; intros b.
     apply ooextendable_homotopy, null.
 Defined.
 
 Definition ooextendable_isnull_fibers {A B} (f : A -> B) (C : B -> Type)
-: (forall b, ooExtendableAlong (@const (hfiber f b) Unit tt)
+: (forall b, ooExtendableAlong (const_tt (hfiber f b))
                                (fun _ => C b))
   -> ooExtendableAlong f C
 := fun null n => extendable_isnull_fibers n f C null.

theories/Modalities/Descent.v

@@ -147,7 +147,7 @@ Global Instance inO_TypeO_lex_leq `{Univalence} `{IsAccRSU O'}
   := fun i => ooextendable_TypeO_lex_leq (acc_lgen O' i).
 
 (** If [f] is an [O']-equivalence, then [ap f] is an [O]-equivalence. *)
-Definition OO_inverts_ap'
+Global Instance OO_inverts_ap@{}
        {A B : Type@{i}} (f : A -> B) `{O_inverts O' f} (x y : A)
   : O_inverts O (@ap _ _ f x y).
 Proof.
@@ -181,12 +181,6 @@ Proof.
     srapply eisretr.
 Defined.
 
-(** We give a version that only has one universe variable. *)
-Global Instance OO_inverts_ap
-       {A B : Type@{i}} (f : A -> B) `{O_inverts O' f} (x y : A)
-  : O_inverts O (@ap _ _ f x y)
-  := OO_inverts_ap'@{i i i i i i i} f x y.
-
 Definition equiv_O_functor_ap_OO_inverts
        {A B : Type} (f : A -> B) `{O_inverts O' f} (x y : A)
   : O (x = y) <~> O (f x = f y)
@@ -197,8 +191,8 @@ Definition OO_isconnected_paths
            {A : Type} `{IsConnected O' A} (x y : A)
   : IsConnected O (x = y).
 Proof.
-  rapply (contr_equiv' _ (equiv_O_functor_ap_OO_inverts (const tt) x y)^-1).
-Defined.  
+  rapply (contr_equiv' _ (equiv_O_functor_ap_OO_inverts (const_tt _) x y)^-1).
+Defined.
 
 (** Proposition 2.26 of CORS and Theorem 3.1(ix) of RSS; also generalizes Theorem 7.3.12 of the book.  Here we need to add the extra assumption that [O' <= Sep O], which is satisfied when [O' = Sep O] but also when [O] is lex and [O' = O].  That some such extra hypothesis is necessary can be seen from the fact that [Tr (-2) <<< O'] for any [O'], whereas this statement is certainly not true in that generality. *)
 Definition path_OO `{O' <= Sep O}
@@ -363,7 +357,7 @@ End LeftExactness.
 
 (** Here's the "only if" direction of CORS Proposition 2.31.  Note that the hypotheses are different from those of the "if" direction, and the proof is shorter than the one given in CORS. *)
 Definition OO_cancelR_conn_map
-       (O' O : ReflectiveSubuniverse) `{O <= O', O' <= Sep O}
+       (O' O : ReflectiveSubuniverse@{u}) `{O_leq@{u u u} O O', O' <= Sep O}
        {Y X Z : Type} (f : Y -> X) (g : X -> Z)
        `{IsConnMap O' _ _ (g o f)} `{IsConnMap O _ _ f}
   : IsConnMap O' g.
@@ -386,7 +380,7 @@ Definition OO_isconnected_from_conn_map
   : IsConnected O' X.
 Proof.
   apply isconnected_conn_map_to_unit.
-  apply (OO_cancelR_conn_map O' O f (const tt)).
+  apply (OO_cancelR_conn_map O' O f (const_tt _)).
 Defined.
 
 (** An interesting scholium to Proposition 2.31. *)
@@ -408,7 +402,7 @@ Definition OO_inverts_conn_map_isconnected_domain
        `{IsConnected O' Y} `{IsConnMap O _ _ f}
   : O_inverts O' f.
 Proof.
-  apply (OO_inverts_conn_map_factor_conn_map O' O f (const tt)).
+  apply (OO_inverts_conn_map_factor_conn_map O' O f (const_tt _)).
 Defined.
 
 (** Here is the converse of [ooextendable_TypeO_lex_leq]. *)

theories/Modalities/Lex.v

@@ -304,7 +304,7 @@ Section ImpliesLex.
     apply conn_map_isequiv.
     apply H; [ | exact _ | exact _ ].
     apply isconnected_conn_map_to_unit.
-    apply (cancelR_conn_map O (factor1 (image O f)) (const tt)).
+    apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)).
   Defined.
 
   (** RSS Theorem 3.1 (vii) implies lex-ness *)
@@ -318,7 +318,7 @@ Section ImpliesLex.
   Proof.
     apply lex_from_isequiv_ismodal_isconnected_types.
     intros A B f AC BC fM.
-    specialize (H A Unit B Unit (const tt) (const tt) f idmap _ _ _ _
+    specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _
                   (fun _ => 1)).
     unfold IsPullback, pullback_corec in H.
     refine (@isequiv_compose _ _ _ H _ (fun x => x.2.1) _).