fix universe variance in IsSmall

Signed-off-by: Ali Caglayan <[email protected]>

theories/Basics/Overture.v

@@ -763,7 +763,7 @@ Global Arguments hfiber {A B}%_type_scope f%_function_scope y.
 (** ** Smallness *)
 
 (** We say that [X : Type@{j}] is small (relative to Type@{i}) if it is equivalent to a type in [Type@{i}].  We use a record to avoid an extra universe variable.  This version has no constraints on [i] and [j].  It lands in [max(i+1,j)], as expected. *)
-Class IsSmall@{i j | } (X : Type@{j}) := {
+Class IsSmall@{=i j | } (X : Type@{j}) := {
   smalltype : Type@{i} ;
   equiv_smalltype : smalltype <~> X ;
 }.