Merge pull request #2373 from jdchristensen/conn_point_incl-universes

Connectedness: remove one universe variable from conn_point_incl

Author: jdchristensen

theories/Truncations/Connectedness.v

@@ -114,10 +114,10 @@ Proof.
   exact (OO_cancelR_conn_map (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)
-  := OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A).
+  := OO_cancelL_conn_map@{u _ _ _} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A).
 
 (** [conn_point_incl] can be made an instance, but at the time of writing, this doesn't cause any additional goals to be solved compared to making it an immediate hint, so we do the latter. *)
 #[export] Hint Immediate conn_point_incl : typeclass_instances.