clarify Smallness require

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

theories/PropResizing/ImpredicativeTruncation.v

@@ -2,7 +2,7 @@
 (** * Impredicative truncations. *)
 
 Require Import HoTT.Basics.
-Require Import Smallness.
+Require Import Universes.Smallness.
 Local Open Scope path_scope.
 
 (* Be careful about [Import]ing this file!  It defines truncations

theories/PropResizing/Nat.v

@@ -3,7 +3,7 @@
 Require Import Basics.
 Require Import Types.
 Require Import HProp.
-Require Import Smallness.
+Require Import Universes.Smallness.
 Local Open Scope path_scope.
 
 (* Be careful about [Import]ing this file!  Usually you want to use the standard [Nat] instead. *)

theories/Sets/GCH.v

@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Nat.Core Spaces.Card.
 
 Local Open Scope type.

theories/Sets/GCHtoAC.v

@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Nat.Core Spaces.Card.
 From HoTT Require Import Equiv.BiInv.
 From HoTT Require Import HIT.unique_choice.

theories/Sets/Hartogs.v

@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Card.
 
 From HoTT.Sets Require Import Ordinals Powers.

theories/Sets/Ordinals.v

@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Colimits.Quotient.
 From HoTT Require Import HSet.