From ab91f7d5025bcf3ecf892e0bd9602aec0dfb73e5 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 20 Feb 2023 19:28:02 -0500
Subject: [PATCH 01/10] Define and use const_tt to eliminate unneeded universe
 variables in many places

---
 theories/Classes/implementations/family_prod.v |  4 ++--
 theories/Extensions.v                          |  4 ++--
 theories/HIT/SetCone.v                         |  4 ++--
 theories/HIT/epi.v                             |  4 ++--
 theories/Homotopy/Suspension.v                 |  2 +-
 theories/Limits/Pullback.v                     |  2 +-
 theories/Modalities/Accessible.v               |  6 +++---
 theories/Modalities/Descent.v                  |  8 ++++----
 theories/Modalities/Lex.v                      |  4 ++--
 theories/Modalities/Nullification.v            | 12 ++++++------
 theories/Modalities/Open.v                     |  4 ++--
 theories/Modalities/ReflectiveSubuniverse.v    | 16 ++++++++--------
 theories/Modalities/Separated.v                |  2 +-
 theories/Types/Unit.v                          |  3 +++
 14 files changed, 39 insertions(+), 36 deletions(-)

diff --git a/theories/Classes/implementations/family_prod.v b/theories/Classes/implementations/family_prod.v
index bb2cf0230e8..e81b445949c 100644
--- a/theories/Classes/implementations/family_prod.v
+++ b/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.
 
diff --git a/theories/Extensions.v b/theories/Extensions.v
index b17ebc53a26..cdc5da80b82 100644
--- a/theories/Extensions.v
+++ b/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.
diff --git a/theories/HIT/SetCone.v b/theories/HIT/SetCone.v
index b0db1d7c90c..5c787a7fe69 100644
--- a/theories/HIT/SetCone.v
+++ 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 := _.
 
diff --git a/theories/HIT/epi.v b/theories/HIT/epi.v
index a94915e4585..743df0c17a5 100644
--- a/theories/HIT/epi.v
+++ b/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? *)
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index 9e6498ab0f2..a0143603bee 100644
--- a/theories/Homotopy/Suspension.v
+++ b/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.
diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v
index 0367247fcd8..f8abd085c5d 100644
--- a/theories/Limits/Pullback.v
+++ b/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).
diff --git a/theories/Modalities/Accessible.v b/theories/Modalities/Accessible.v
index 97193db7fa3..582a358a17f 100644
--- a/theories/Modalities/Accessible.v
+++ 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,7 +100,7 @@ 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.
@@ -108,7 +108,7 @@ Proof.
 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.
diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index 7c0e0c25474..4721d8ef608 100644
--- a/theories/Modalities/Descent.v
+++ b/theories/Modalities/Descent.v
@@ -197,8 +197,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}
@@ -386,7 +386,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 +408,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]. *)
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index 5b6749d9a78..0af6f78e299 100644
--- a/theories/Modalities/Lex.v
+++ b/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) _).
diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
index 54dfac9caa7..2d1a1630079 100644
--- a/theories/Modalities/Nullification.v
+++ b/theories/Modalities/Nullification.v
@@ -14,10 +14,10 @@ Local Open Scope path_scope.
 
 Definition extendable_over_unit (n : nat)
   (A : Type@{a}) (C : Unit -> Type@{i}) (D : forall u, C u -> Type@{j})
-  (ext : ExtendableAlong@{a a i k} n (@const A Unit tt) C)
+  (ext : ExtendableAlong@{a a i k} n (const_tt A) C)
   (ext' : forall (c : forall u, C u),
-            ExtendableAlong@{a a j k} n (@const A Unit tt) (fun u => (D u (c u))))
-: ExtendableAlong_Over@{a a i j k} n (@const A Unit tt) C D ext.
+            ExtendableAlong@{a a j k} n (const_tt A) (fun u => (D u (c u))))
+  : ExtendableAlong_Over@{a a i j k} n (const_tt A) C D ext.
 Proof.
   generalize dependent C; simple_induction n n IH;
     intros C D ext ext'; [exact tt | split].
@@ -35,10 +35,10 @@ Defined.
 
 Definition ooextendable_over_unit@{i j k l m}
   (A : Type@{i}) (C : Unit -> Type@{j}) (D : forall u, C u -> Type@{k})
-  (ext : ooExtendableAlong@{l l j m} (@const@{l l} A Unit tt) C)
+  (ext : ooExtendableAlong@{l l j m} (const_tt A) C)
   (ext' : forall (c : forall u, C u),
-            ooExtendableAlong (@const A Unit tt) (fun u => (D u (c u))))
-: ooExtendableAlong_Over (@const A Unit tt) C D ext
+            ooExtendableAlong (const_tt A) (fun u => (D u (c u))))
+  : ooExtendableAlong_Over (const_tt A) C D ext
   := fun n => extendable_over_unit n A C D (ext n) (fun c => ext' c n).
 
 #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
diff --git a/theories/Modalities/Open.v b/theories/Modalities/Open.v
index f0167bab8d5..126afb4ea0c 100644
--- a/theories/Modalities/Open.v
+++ b/theories/Modalities/Open.v
@@ -81,8 +81,8 @@ Proof.
       apply X_inO.
     + intros ext; specialize (ext tt).
       refine (isequiv_compose (f := (fun x => unit_name x))
-                              (g := (fun h => h o (@const U Unit tt)))).
-      refine (isequiv_ooextendable (fun _ => X) (@const U Unit tt) ext).
+                              (g := (fun h => h o const_tt U))).
+      refine (isequiv_ooextendable (fun _ => X) (const_tt U) ext).
 Defined.
 
 (** Thus, arguably a better definition of [Op] would be as a nullification modality, as it would not require [Funext] and would have a judgmental computation rule.  However, the above definition is also nice to know, as it doesn't use HITs.  We name the other version [Op']. *)
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index 064ac3e1ce1..e4769816531 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1413,7 +1413,7 @@ Section ConnectedTypes.
   Definition extendable_const_isconnected_inO (n : nat)
              (A : Type) `{IsConnected O A}
              (C : Type) `{In O C}
-  : ExtendableAlong n (@const A Unit tt) (fun _ => C).
+  : ExtendableAlong n (const_tt A) (fun _ => C).
   Proof.
     generalize dependent C;
       simple_induction n n IHn; intros C ?;
@@ -1429,7 +1429,7 @@ Section ConnectedTypes.
   Definition ooextendable_const_isconnected_inO
              (A : Type@{i}) `{IsConnected@{i} O A}
              (C : Type@{j}) `{In O C}
-  : ooExtendableAlong (@const A Unit tt) (fun _ => C)
+  : ooExtendableAlong (const_tt A) (fun _ => C)
     := fun n => extendable_const_isconnected_inO n A C.
 
   Definition isequiv_const_isconnected_inO `{Funext}
@@ -1437,7 +1437,7 @@ Section ConnectedTypes.
   : IsEquiv (@const A C).
   Proof.
     refine (@isequiv_compose _ _ (fun c u => c) _ _ _
-              (isequiv_ooextendable (fun _ => C) (@const A Unit tt)
+              (isequiv_ooextendable (fun _ => C) (const_tt A)
                                     (ooextendable_const_isconnected_inO A C))).
   Defined.
 
@@ -1768,11 +1768,11 @@ Section ConnectedMaps.
 
   (** The constant map to [Unit] is connected just when its domain is. *)
   Definition isconnected_conn_map_to_unit {A : Type}
-             `{IsConnMap O _ _ (@const A Unit tt)}
+             `{IsConnMap O _ _ (const_tt A)}
   : IsConnected O A.
   Proof.
-    refine (isconnected_equiv O (hfiber (@const A Unit tt) tt)
-              (equiv_sigma_contr (fun a:A => const tt a = tt)) _).
+    refine (isconnected_equiv O (hfiber (const_tt A) tt)
+              (equiv_sigma_contr _) _).
   Defined.
 
   #[local]
@@ -1780,11 +1780,11 @@ Section ConnectedMaps.
 
   Global Instance conn_map_to_unit_isconnected {A : Type}
          `{IsConnected O A}
-  : IsConnMap O (@const A Unit tt).
+  : IsConnMap O (const_tt A).
   Proof.
     intros u.
     refine (isconnected_equiv O A
-              (equiv_sigma_contr (fun a:A => const tt a = u))^-1 _).
+              (equiv_sigma_contr _)^-1 _).
   Defined.
 
   (* Lemma 7.5.10: A map to a type in [O] exhibits its codomain as the [O]-reflection of its domain if it is [O]-connected.  (The converse is true if and only if [O] is a modality.) *)
diff --git a/theories/Modalities/Separated.v b/theories/Modalities/Separated.v
index 36eed46b16b..8d6bc57f781 100644
--- a/theories/Modalities/Separated.v
+++ b/theories/Modalities/Separated.v
@@ -130,7 +130,7 @@ Global Instance in_SepO_hprop (O : ReflectiveSubuniverse)
        {A : Type} `{IsHProp A}
   : In (Sep O) A.
 Proof.
-  srapply (in_SepO_embedding O (const tt)).
+  srapply (in_SepO_embedding O (const_tt _)).
   intros x y; exact _.
 Defined.
 
diff --git a/theories/Types/Unit.v b/theories/Types/Unit.v
index e9078a82307..f53b58dc200 100644
--- a/theories/Types/Unit.v
+++ b/theories/Types/Unit.v
@@ -124,3 +124,6 @@ Defined.
 Global Instance contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A | 10000
   := Build_Contr A (f^-1 tt)
   (fun a => ap f^-1 (contr (f a)) @ eissect f a).
+
+(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when this is not annotated. *)
+Definition const_tt@{u} (A : Type@{u}) := @const@{Set u} A Unit tt.

From 3e4055dd5336609055fbb98f28753141784c11a5 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 21 Feb 2023 15:07:56 -0500
Subject: [PATCH 02/10] Reduce universe variables

---
 theories/Algebra/AbSES/Core.v               |  6 +++---
 theories/Algebra/AbSES/SixTerm.v            |  8 ++++----
 theories/Metatheory/Core.v                  |  2 +-
 theories/Modalities/Descent.v               | 10 ++--------
 theories/Modalities/Nullification.v         |  2 +-
 theories/Modalities/ReflectiveSubuniverse.v |  6 +++---
 theories/Truncations/Connectedness.v        | 12 ++++++++----
 theories/Types/Universe.v                   |  6 +++---
 8 files changed, 25 insertions(+), 27 deletions(-)

diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 531094af7f9..9328db5e2bf 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/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.
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index d3d723bc0c1..5188cf1c2bb 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/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,7 +208,7 @@ 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.
 
@@ -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)))).
diff --git a/theories/Metatheory/Core.v b/theories/Metatheory/Core.v
index 43e5fd33083..9916146588d 100644
--- a/theories/Metatheory/Core.v
+++ 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).
diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index 4721d8ef608..f129294e4c3 100644
--- a/theories/Modalities/Descent.v
+++ b/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)
@@ -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.
diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
index 2d1a1630079..effc14fddad 100644
--- a/theories/Modalities/Nullification.v
+++ b/theories/Modalities/Nullification.v
@@ -59,7 +59,7 @@ Proof.
                 (fun u => transport B (ap c (path_unit@{a} tt u))) _).
       refine (ooextendable_islocal _ i).
     + reflexivity.
-    + apply inO_paths@{i i i}.
+    + apply inO_paths@{i i}.
   Defined.
 
 (** And here is the "real" definition of the notation [IsNull]. *)
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index e4769816531..0f4462c42ab 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -996,7 +996,7 @@ Section Reflective_Subuniverse.
 
     (** ** Paths *)
 
-    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In O S} (x y : S)
+    Definition inO_paths@{i} (S : Type@{i}) {S_inO : In O S} (x y : S)
     : In O (x=y).
     Proof.
       simple refine (inO_to_O_retract@{i} _ _ _); intro u.
@@ -1388,10 +1388,10 @@ Section ConnectedTypes.
   Defined.
 
   (** Contractible types are connected. *)
-  Global Instance isconnected_contr {A : Type} `{Contr A}
+  Global Instance isconnected_contr@{u} {A : Type@{u}} `{Contr A}
     : IsConnected O A.
   Proof.
-    apply contr_O_contr; exact _.
+    apply contr_O_contr@{u u u u}; exact _.
   Defined.    
 
   (** A type which is both connected and modal is contractible. *)
diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index e9ef3148bf0..ae0bddd7b60 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -62,19 +62,23 @@ Defined.
 (** The connectivity of a pointed type and (the inclusion of) its point are intimately connected. *)
 
 (** We can't make both of these [Instance]s, as that would result in infinite loops. *)
-Global Instance conn_pointed_type {n : trunc_index} {A : Type} (a0:A)
+Global Instance conn_pointed_type@{u} {n : trunc_index} {A : Type@{u}} (a0:A)
        `{IsConnMap n _ _ (unit_name a0)}
   : IsConnected n.+1 A | 1000.
 Proof.
   apply isconnected_conn_map_to_unit.
-  rapply (OO_cancelR_conn_map (Tr n.+1) (Tr n) (unit_name a0) (fun _:A => tt)).
+  (* Coq can find [conn_map_to_unit_isconnected] via typeclass search, but we manually pose it to get rid of an unneeded universe variable. *)
+  pose conn_map_to_unit_isconnected@{u u}.
+  rapply (OO_cancelR_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
 Defined.
 
-Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type} (a0:A)
+Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type@{u}} (a0:A)
            `{IsConnected n.+1 A}
   : IsConnMap n (unit_name a0).
 Proof.
-  rapply (OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (fun _:A => tt)).
+  (* Coq can find [conn_map_to_unit_isconnected] via typeclass search, but we manually pose it to get rid of an unneeded universe variable. *)
+  pose conn_map_to_unit_isconnected@{u u}.
+  rapply (OO_cancelL_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
   apply O_lex_leq_Tr.
 Defined.
 
diff --git a/theories/Types/Universe.v b/theories/Types/Universe.v
index 09e560fe59e..57034ccc8a4 100644
--- a/theories/Types/Universe.v
+++ b/theories/Types/Universe.v
@@ -10,8 +10,8 @@ Generalizable Variables A B f.
 
 (** ** Paths *)
 
-Definition equiv_path (A B : Type) (p : A = B) : A <~> B
-  := equiv_transport (fun X:Type => X) p.
+Definition equiv_path (A B : Type@{u}) (p : A = B) : A <~> B
+  := equiv_transport (fun X => X) p.
 
 Definition equiv_path_V `{Funext} (A B : Type) (p : A = B) :
   equiv_path B A (p^) = (equiv_path A B p)^-1%equiv.
@@ -27,7 +27,7 @@ Existing Class Univalence.
 (** Mark this axiom as a "global axiom", which some of our tactics will automatically handle. *)
 Global Instance is_global_axiom_univalence : IsGlobalAxiom Univalence := {}.
 
-Axiom isequiv_equiv_path : forall `{Univalence} (A B : Type), IsEquiv (equiv_path A B).
+Axiom isequiv_equiv_path : forall `{Univalence} (A B : Type@{u}), IsEquiv (equiv_path A B).
 Global Existing Instance isequiv_equiv_path.
 
 (** A proof that univalence implies function extensionality can be found in the metatheory file [UnivalenceImpliesFunext], but that actual proof can't be used on our dummy typeclasses.  So we assert the following axiomatic instance.  *)

From 14dea02ed6c973f2b950c762bcdf06cabe5444f4 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 22 Feb 2023 10:49:17 -0500
Subject: [PATCH 03/10] Reduce more universe variables

---
 theories/Algebra/AbGroups/AbelianGroup.v    | 2 +-
 theories/Algebra/AbGroups/Cyclic.v          | 2 +-
 theories/Algebra/AbSES/SixTerm.v            | 2 +-
 theories/Homotopy/ExactSequence.v           | 6 +++---
 theories/Modalities/ReflectiveSubuniverse.v | 4 ++--
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 5920fecc12b..6e30745d68d 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/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}
diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v
index bc04ac7d08b..afd11ec5191 100644
--- a/theories/Algebra/AbGroups/Cyclic.v
+++ b/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).
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 5188cf1c2bb..b380380b6ef 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -215,7 +215,7 @@ 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.
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index ad8c01b0386..18914ccd3ed 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/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}
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index 0f4462c42ab..02d97a9a03e 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1737,8 +1737,8 @@ Section ConnectedMaps.
   : IsConnMap O (g o f).
   Proof.
     apply conn_map_from_extension_elim; intros P ? d.
-    exists (conn_map_elim g P (conn_map_elim f (P o g) d)); intros a.
-    exact (conn_map_comp g P _ _ @ conn_map_comp f (P o g) d a).
+    exists (conn_map_elim g P (conn_map_elim f (fun b => P (g b)) d)); intros a.
+    exact (conn_map_comp g P _ _ @ conn_map_comp f (fun b => P (g b)) d a).
   Defined.      
 
   Definition cancelR_conn_map {A B C : Type} (f : A -> B) (g : B -> C)

From d0cd8e915b0a333e47cec98fcf6b799433d5674a Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 10:46:13 -0500
Subject: [PATCH 04/10] Overture.v: document that nat and trunc_index land in
 Type0

---
 theories/Basics/Overture.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 9ed5e671228..14e7b6cd157 100644
--- a/theories/Basics/Overture.v
+++ b/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.
 
@@ -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.
 

From f4762f82bb743116dbd910df5d67cb2d640999e0 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 10:46:49 -0500
Subject: [PATCH 05/10] Unit.v: add comment about minimization to set

---
 theories/Types/Unit.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Types/Unit.v b/theories/Types/Unit.v
index f53b58dc200..7231a839e3b 100644
--- a/theories/Types/Unit.v
+++ b/theories/Types/Unit.v
@@ -125,5 +125,5 @@ Global Instance contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A | 10000
   := Build_Contr A (f^-1 tt)
   (fun a => ap f^-1 (contr (f a)) @ eissect f a).
 
-(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when this is not annotated. *)
+(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when this is not annotated. If we ever turn on [Universe Minimization ToSet], then we could get rid of this and remove some imports of this file. *)
 Definition const_tt@{u} (A : Type@{u}) := @const@{Set u} A Unit tt.

From 23cf3334141bc037c3758bb840281b4b43eba9a2 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 10:59:41 -0500
Subject: [PATCH 06/10] Reduce universes in IsTrunc_internal and not

---
 theories/Basics/Overture.v                     | 4 ++--
 theories/Classes/interfaces/abstract_algebra.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 14e7b6cd157..3b813c80383 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -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)
@@ -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@{u}) : Type@{u} := A -> Empty.
 Notation "~ x" := (not x) : type_scope.
 Notation "~~ x" := (~ ~x) : type_scope.
 #[export]
diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v
index 3a35bb7497b..81bc1e34104 100644
--- a/theories/Classes/interfaces/abstract_algebra.v
+++ b/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).
 

From 386fa0832dd3b314924c20ec04aa5f4d9c52da46 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 17:45:13 -0500
Subject: [PATCH 07/10] Reduce universe vars in SPushout and freudenthal

Closes #1531
---
 theories/Colimits/SpanPushout.v |  2 +-
 theories/Homotopy/Freudenthal.v | 23 ++++++++++++-----------
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/theories/Colimits/SpanPushout.v b/theories/Colimits/SpanPushout.v
index bb114988832..fd7ab529553 100644
--- a/theories/Colimits/SpanPushout.v
+++ b/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.
diff --git a/theories/Homotopy/Freudenthal.v b/theories/Homotopy/Freudenthal.v
index edc78dfcd90..5aba6c54510 100644
--- a/theories/Homotopy/Freudenthal.v
+++ b/theories/Homotopy/Freudenthal.v
@@ -9,20 +9,17 @@ 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)
+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
@@ -30,3 +27,7 @@ Proof.
                  (fun x : X => idpath) (fun x : X => idpath) x)^).
   exact ((concat_p1 _ @ concat_1p _)^).
 Defined.
+
+Definition freudenthal@{u v | u < v} := @freudenthal'@{u u u u u v u u u}.
+
+Global Existing Instance freudenthal.

From b514d6985508becdd3d2582382c4eb958002a4d9 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 17:50:39 -0500
Subject: [PATCH 08/10] Overture: simplify not

---
 theories/Basics/Overture.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 3b813c80383..da8d29c7d5e 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -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@{u}) : Type@{u} := A -> Empty.
+Definition not (A : Type) := A -> Empty.
 Notation "~ x" := (not x) : type_scope.
 Notation "~~ x" := (~ ~x) : type_scope.
 #[export]

From 64e7acbb2afffb858cdca5c0b883113d0b448765 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 25 Feb 2023 18:49:04 -0500
Subject: [PATCH 09/10] Freudenthal.v: use Eval unfold trick to get rid of
 indirection

---
 theories/Homotopy/Freudenthal.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Homotopy/Freudenthal.v b/theories/Homotopy/Freudenthal.v
index 5aba6c54510..5792faae853 100644
--- a/theories/Homotopy/Freudenthal.v
+++ b/theories/Homotopy/Freudenthal.v
@@ -9,7 +9,7 @@ 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. *)
-Definition 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.
@@ -28,6 +28,6 @@ Proof.
   exact ((concat_p1 _ @ concat_1p _)^).
 Defined.
 
-Definition freudenthal@{u v | u < v} := @freudenthal'@{u u u u u v u u u}.
+Definition freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u}.
 
 Global Existing Instance freudenthal.

From ae48644c8b9ffa53f8821c733947af9848e07108 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 26 Feb 2023 16:20:12 -0500
Subject: [PATCH 10/10] ReflectiveSubuniverse: get rid of a couple more
 universe variables and adapt other files

---
 theories/Homotopy/Freudenthal.v             |  2 +-
 theories/Modalities/ReflectiveSubuniverse.v | 12 ++++++------
 theories/Truncations/Connectedness.v        |  5 +++--
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/theories/Homotopy/Freudenthal.v b/theories/Homotopy/Freudenthal.v
index 5792faae853..829d85cf316 100644
--- a/theories/Homotopy/Freudenthal.v
+++ b/theories/Homotopy/Freudenthal.v
@@ -28,6 +28,6 @@ Proof.
   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}.
+Definition freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u u u}.
 
 Global Existing Instance freudenthal.
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index 02d97a9a03e..261dfa38400 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -743,14 +743,14 @@ Section Reflective_Subuniverse.
     (** ** The [Unit] type *)
     Global Instance inO_unit : In O Unit.
     Proof.
-      apply inO_to_O_retract with (mu := fun x => tt).
-      exact (@contr Unit _).
+      apply inO_to_O_retract@{Set} with (mu := fun x => tt).
+      exact (@contr@{Set} Unit _).
     Defined.
 
     (** It follows that any contractible type is in [O]. *)
     Global Instance inO_contr {A : Type} `{Contr A} : In O A.
     Proof.
-      exact (inO_equiv_inO Unit equiv_contr_unit^-1).
+      exact (inO_equiv_inO@{Set _ _} Unit equiv_contr_unit^-1).
     Defined.
 
     (** And that the reflection of a contractible type is still contractible. *)
@@ -1388,11 +1388,11 @@ Section ConnectedTypes.
   Defined.
 
   (** Contractible types are connected. *)
-  Global Instance isconnected_contr@{u} {A : Type@{u}} `{Contr A}
+  Global Instance isconnected_contr {A : Type} `{Contr A}
     : IsConnected O A.
   Proof.
-    apply contr_O_contr@{u u u u}; exact _.
-  Defined.    
+    rapply contr_O_contr.
+  Defined.
 
   (** A type which is both connected and modal is contractible. *)
   Definition contr_trunc_conn {A : Type} `{In O A} `{IsConnected O A}
diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index ae0bddd7b60..fbfaf91875a 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -67,9 +67,10 @@ Global Instance conn_pointed_type@{u} {n : trunc_index} {A : Type@{u}} (a0:A)
   : IsConnected n.+1 A | 1000.
 Proof.
   apply isconnected_conn_map_to_unit.
-  (* Coq can find [conn_map_to_unit_isconnected] via typeclass search, but we manually pose it to get rid of an unneeded universe variable. *)
+  (* Coq can find [conn_map_to_unit_isconnected] and [isconnected_contr] via typeclass search, but we manually pose them to get rid of an unneeded universe variable. *)
   pose conn_map_to_unit_isconnected@{u u}.
-  rapply (OO_cancelR_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
+  pose isconnected_contr@{u u}.
+  apply (OO_cancelR_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
 Defined.
 
 Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type@{u}} (a0:A)