HoTT · jdchristensen · Sep 24, 2024 · Feb 19, 2024 · Sep 21, 2024 · Sep 21, 2024
diff --git a/STYLE.md b/STYLE.md
@@ -27,7 +27,7 @@
     - [3.6. Truncation](#36-truncation)
     - [3.7. Coercions and Existing Instances](#37-coercions-and-existing-instances)
   - [4. Axioms](#4-axioms)
-    - [4.1. Univalence and function extensionality](#41-univalence-and-function-extensionality)
+    - [4.1. Univalence, function extensionality and propositional resizing](#41-univalence-function-extensionality-and-propositional-resizing)
     - [4.2. Higher inductive types](#42-higher-inductive-types)
     - [4.3. Relationships between axioms](#43-relationships-between-axioms)
     - [4.4. Assuming axioms](#44-assuming-axioms)
@@ -103,13 +103,19 @@ corresponding file `Foo.v` that imports everything in the subdirectory.
   studied further in their `Types/` file.  Files in `Types/` should
   not depend on anything except `Basics` and other `Types/` files.
 
-- There are many other files in the root `theories/` directory,
-  including `TruncType`, `HProp`, `DProp`, `HSet`, `HFiber`,
-  `ObjectClassifier`, `Extensions`, `NullHomotopy`, `PathAny`,
-  `Projective`, `Idempotents`, `Constant`, etc.  These contain more
-  advanced facts and theories which may depend on files in `Types/`.
-  We try to limit the number of files in the top-level folder, and
-  would like to reduce the number.
+- `Universes/*`: Files related to universe levels, classifying maps, or
+  to particular subuniverses, including `UniverseLevel`, `Smallness`,
+  `ObjectClassifier`, `BAut`, `HProp`, `HSet`, `DProp`, and `TruncType`.
+  The files here depend on files in `Types/`, and occasionally on some
+  files mentioned below.
+
+- There are files in the root `theories/` directory, including
+  `EquivGroupoids`, `ExcludedMiddle`, `Factorization`, `HFiber`,
+  `Extensions`, `NullHomotopy`, `PathAny`, `Projective`,
+  `Idempotents`, `Constant`, `BoundedSearch`, etc.  These contain more
+  advanced results which may depend on files in the whole library.  We
+  try to limit the number of files in the top-level folder, and would
+  like to reduce the number.
 
 - `WildCat/*`: Files related to wild categories.  They are used
   extensively in the library, so we try to minimize the files they
@@ -165,9 +171,6 @@ corresponding file `Foo.v` that imports everything in the subdirectory.
   the HoTT library, you can say simply `Require Import HoTT` to pull
   in everything (but don't do this for files in the core itself).
 
-- `PropResizing/*`: Files related to propositional resizing.  Only
-  `PropResizing/PropResizing` is exported by `HoTT`.
-
 - `theories/Classes/*`: The math classes library.  While we don't
   regard this as part of the core library, and don't explicitly
   export the contents in `HoTT`, some files in the classes library
@@ -180,7 +183,9 @@ corresponding file `Foo.v` that imports everything in the subdirectory.
   core, we track them with typeclasses).
 
 - `theories/Metatheory/*`: Contains `UnivalenceImpliesFunext`,
-  `IntervalImpliesFunext` and other meta-theoretic results.
+  `IntervalImpliesFunext`, `ImpredicativeTruncation`, `PropTrunc`,
+  `Nat` (a definition of the natural numbers using univalence and
+  propositional resizing), and other meta-theoretic results.
 
 - `theories/Utf8` and `theories/Utf8Minimal`: optional Unicode
   notations for the basic definitions (we avoid Unicode in the core
@@ -514,15 +519,17 @@ for `x, y : A`.)
 
 ## 4. Axioms ##
 
-### 4.1. Univalence and function extensionality ###
+### 4.1. Univalence, function extensionality and propositional resizing ###
+
+The "axioms" of `Univalence`, `Funext` (function extensionality) and
+`PropResizing` (propositional resizing) are typeclasses rather than
+Coq `Axiom`s.  (But see the technical note below on universe
+polymorphism.)  In the core, we use these typeclasses to keep track
+of which theorems depend on the axioms and which don't.
 
-The "axioms" of `Univalence` and `Funext` (function extensionality)
-are typeclasses rather than Coq `Axiom`s.  (But see the technical note
-below on universe polymorphism.)  In the core, we use these
-typeclasses to keep track of which theorems depend on the axioms and
-which don't.  This means that any theorem which depends on one or the
-other must take an argument of the appropriate type.  It is simple to
-write this using typeclass magic as follows:
+This means that any theorem which depends on one or the other must
+take an argument of the appropriate type.  It is simple to write
+this using typeclass magic as follows:
 
 ```coq
 Theorem uses_univalence `{Univalence} (A : Type) ...
@@ -833,15 +840,19 @@ See also [bug #4868](https://coq.inria.fr/bugs/show_bug.cgi?id=4868).
 
 ### 6.4. Lifting and lowering ###
 
-The file `Basics/UniverseLevel` contains an operation `Lift` which
+The file `Universes/UniverseLevel` contains an operation `Lift` which
 lifts a type from one universe to a larger one, with maps `lift` and
-`lower` relating the two types and forming an equivalence.  This is
-occasionally useful when universe wrangling; for instance, using a
-lifted version of a type rather than a type itself can prevent
-collapse of two universes that ought to remain distinct.  There are
+`lower` relating the two types and forming an equivalence.  There are
 primed versions `Lift'`, `lift'`, and `lower'` which allow the two
 universe levels to possibly be the same.
 
+In the past, `Lift` was used to force universe levels to be distinct,
+but now that Coq supports constraints between universe variables,
+this is no longer needed in practice.
+
+The file `Universes/Smallness` contains results allowing us to show
+that a type lives in a certain universe.
+
 ### 6.5. Universes and HITs ###
 
 Another use for universe annotations is to force HITs to live in the
@@ -856,7 +867,6 @@ We have not yet formulated a general method for resolving this.  In
 the few cases when it arises, it should be solvable with universe
 annotations, but we have not yet implemented such a fix; see bug #565.
 
-
 ## 7. Transparency and Opacity ##
 
 If the value of something being defined matters, then you must either

diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v
@@ -390,7 +390,7 @@ Definition Book_3_3_1 := fun A => @HoTT.Basics.Overture.IsTrunc (-1) A.
 (* ================================================== thm:inhabprop-eqvunit *)
 (** Lemma 3.3.2 *)
 
-Definition Book_3_3_2 := @HoTT.HProp.if_hprop_then_equiv_Unit.
+Definition Book_3_3_2 := @HoTT.Universes.HProp.if_hprop_then_equiv_Unit.
 
 (* ================================================== lem:equiv-iff-hprop *)
 (** Lemma 3.3.3 *)
@@ -694,12 +694,12 @@ Definition Book_4_8_2 := @HoTT.HFiber.equiv_fibration_replacement.
 (* ================================================== thm:nobject-classifier-appetizer *)
 (** Theorem 4.8.3 *)
 
-Definition Book_4_8_3 := @HoTT.ObjectClassifier.equiv_sigma_fibration.
+Definition Book_4_8_3 := @HoTT.Universes.ObjectClassifier.equiv_sigma_fibration.
 
 (* ================================================== thm:object-classifier *)
 (** Theorem 4.8.4 *)
 
-Definition Book_4_8_4 := @HoTT.ObjectClassifier.ispullback_objectclassifier_square.
+Definition Book_4_8_4 := @HoTT.Universes.ObjectClassifier.ispullback_objectclassifier_square.
 
 (* ================================================== weakfunext *)
 (** Definition 4.9.1 *)
@@ -1000,7 +1000,7 @@ Definition Book_7_1_9 := @HoTT.Basics.Trunc.istrunc_forall.
 (* ================================================== thm:hleveln-of-hlevelSn *)
 (** Theorem 7.1.11 *)
 
-Definition Book7_1_11 := @HoTT.TruncType.istrunc_trunctype.
+Definition Book7_1_11 := @HoTT.Universes.TruncType.istrunc_trunctype.
 
 (* ================================================== thm:h-set-uip-K *)
 (** Theorem 7.2.1 *)
@@ -1010,7 +1010,7 @@ Definition Book7_1_11 := @HoTT.TruncType.istrunc_trunctype.
 (* ================================================== thm:h-set-refrel-in-paths-sets *)
 (** Theorem 7.2.2 *)
 
-Definition Book_7_2_2 := @HoTT.HSet.ishset_hrel_subpaths.
+Definition Book_7_2_2 := @HoTT.Universes.HSet.ishset_hrel_subpaths.
 
 (* ================================================== notnotstable-equality-to-set *)
 (** Corollary 7.2.3 *)

diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v
@@ -803,7 +803,7 @@ Defined.
 (* ================================================== ex:prop-inhabcontr *)
 (** Exercise 3.5 *)
 
-Definition Book_3_5_solution_1 := @HoTT.HProp.equiv_hprop_inhabited_contr.
+Definition Book_3_5_solution_1 := @HoTT.Universes.HProp.equiv_hprop_inhabited_contr.
 
 (* ================================================== ex:lem-mereprop *)
 (** Exercise 3.6 *)
@@ -1712,7 +1712,7 @@ End Book_6_9.
 Section Book_7_1.
   Lemma Book_7_1_part_i (H : forall A, merely A -> A) A : IsHSet A.
   Proof.
-    apply (@HoTT.HSet.ishset_hrel_subpaths
+    apply (@HoTT.Universes.HSet.ishset_hrel_subpaths
              A (fun x y => merely (x = y)));
     try typeclasses eauto.
     - intros ?.

diff --git a/theories/Algebra/Aut.v b/theories/Algebra/Aut.v
@@ -2,7 +2,7 @@
 Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.
-Require Import Spaces.BAut.
+Require Import Universes.BAut.
 Require Import Pointed.Core.
 
 Local Open Scope pointed_scope.

diff --git a/theories/Algebra/Universal/Congruence.v b/theories/Algebra/Universal/Congruence.v
@@ -7,7 +7,7 @@
 Require Export HoTT.Algebra.Universal.Algebra.
 
 Require Import
-  HoTT.HProp
+  HoTT.Universes.HProp
   HoTT.Classes.interfaces.canonical_names
   HoTT.Algebra.Universal.Homomorphism.
 

diff --git a/theories/Algebra/Universal/TermAlgebra.v b/theories/Algebra/Universal/TermAlgebra.v
@@ -13,7 +13,7 @@
 Require Export HoTT.Algebra.Universal.Algebra.
 
 Require Import
-  HoTT.HSet
+  HoTT.Universes.HSet
   HoTT.Classes.interfaces.canonical_names
   HoTT.Algebra.Universal.Homomorphism
   HoTT.Algebra.Universal.Congruence.

diff --git a/theories/Axioms/Funext.v b/theories/Axioms/Funext.v
@@ -1,9 +1,6 @@
-(** To assume the Funext axiom outright, import this file.
-    (Doing this instead of simply positing Funext directly
-    avoids creating multiple witnesses for the axiom in
-    different developments.) *)
-
 Require Import Basics.Overture.
 
+(** To assume the Funext axiom outright, import this file. (Doing this instead of simply positing Funext directly avoids creating multiple witnesses for the axiom in different developments.) *)
+
 Axiom funext_axiom : Funext.
 Global Existing Instance funext_axiom.
diff --git a/theories/Axioms/PropResizing.v b/theories/Axioms/PropResizing.v
@@ -0,0 +1,6 @@
+Require Import Basics.Overture.
+
+(** To assume the PropResizing axiom outright, import this file. (Doing this instead of simply positing PropResizing directly avoids creating multiple witnesses for the axiom in different developments.) *)
+
+Axiom propresizing_axiom : PropResizing.
+Global Existing Instance propresizing_axiom.
diff --git a/theories/Axioms/Univalence.v b/theories/Axioms/Univalence.v
@@ -1,9 +1,6 @@
-(** To assume the Univalence axiom outright, import this file.
-    (Doing this instead of simply positing Univalence directly
-    avoids creating multiple witnesses for the axiom in
-    different developments.) *)
-
 Require Import Types.Universe.
 
+(** To assume the Univalence axiom outright, import this file. (Doing this instead of simply positing Univalence directly avoids creating multiple witnesses for the axiom in different developments.) *)
+
 Axiom univalence_axiom : Univalence.
 Global Existing Instance univalence_axiom.
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
@@ -759,3 +759,24 @@ Global Existing Instance ispointed_type.
 Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
 
 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.  We mark the [i] variable as being invariant, so that Coq is better at guessing universe variables when this is used. *)
+Class IsSmall@{=i j | } (X : Type@{j}) := {
+  smalltype : Type@{i} ;
+  equiv_smalltype : smalltype <~> X ;
+}.
+Arguments smalltype X {_}.
+Arguments equiv_smalltype X {_}.
+
+(** *** Propositional resizing *)
+
+(** See the note by [Funext] above regarding classes for axioms. *)
+Monomorphic Axiom PropResizing : Type0.
+Existing Class PropResizing.
+
+(** Propositional resizing says that every (-1)-truncated type is small. *)
+Axiom issmall_hprop@{i j | } : forall `{PropResizing} (X : Type@{j})
+  (T : IsHProp X), IsSmall@{i j} X.
+Existing Instance issmall_hprop.
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
@@ -404,6 +404,9 @@ Global Hint Mode IsGlobalAxiom + : typeclass_instances.
 (** We add [Funext] to the list here, and will later add [Univalence]. *)
 Global Instance is_global_axiom_funext : IsGlobalAxiom Funext := {}.
 
+(** Add [PropResizing] to the list of global axioms. *)
+Global Instance is_global_axiom_propresizing : IsGlobalAxiom PropResizing := {}.
+
 Ltac is_global_axiom A := let _ := constr:(_ : IsGlobalAxiom A) in idtac.
 
 Ltac global_axiom := try match goal with

diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v
@@ -105,6 +105,13 @@ Definition trunc_index_to_num_int@{} n :=
 Number Notation trunc_index num_int_to_trunc_index trunc_index_to_num_int
   : trunc_scope.
 
+(** Sends a trunc_index [n] to the natural number [n+2]. *)
+Fixpoint trunc_index_to_nat (n : trunc_index) : nat
+  := match n with
+    | minus_two => 0%nat
+    | n'.+1 => (trunc_index_to_nat n').+1
+    end.
+
 (** ** Arithmetic on truncation-levels. *)
 Fixpoint trunc_index_add@{} (m n : trunc_index) : trunc_index
   := match m with

diff --git a/theories/Classes/implementations/hprop_lattice.v b/theories/Classes/implementations/hprop_lattice.v
@@ -1,6 +1,6 @@
 Require Import
   HoTT.Classes.interfaces.abstract_algebra
-  HoTT.TruncType.
+  HoTT.Universes.TruncType.
 
 (** Demonstrate the [HProp] is a (bounded) lattice w.r.t. the logical
 operations. This requires Univalence. *)

diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v
@@ -1,5 +1,5 @@
 Require Import HoTT.HIT.quotient
-  HoTT.TruncType.
+  HoTT.Universes.TruncType.
 Require Import
   HoTT.Classes.implementations.peano_naturals
   HoTT.Classes.interfaces.abstract_algebra

diff --git a/theories/Classes/interfaces/ua_algebra.v b/theories/Classes/interfaces/ua_algebra.v
@@ -8,7 +8,7 @@ Require Export
 
 Require Import
   HoTT.Types
-  HoTT.HSet
+  HoTT.Universes.HSet
   HoTT.Spaces.List.Core.
 
 Import ne_list.notations.

diff --git a/theories/Classes/interfaces/ua_congruence.v b/theories/Classes/interfaces/ua_congruence.v
@@ -1,5 +1,5 @@
 Require Import
-  HoTT.HProp
+  HoTT.Universes.HProp
   HoTT.Classes.interfaces.canonical_names
   HoTT.Classes.interfaces.ua_algebra.
 

diff --git a/theories/Classes/theory/ua_subalgebra.v b/theories/Classes/theory/ua_subalgebra.v
@@ -1,5 +1,5 @@
 Require Import
-  HoTT.HProp
+  HoTT.Universes.HProp
   HoTT.Types
   HoTT.Classes.theory.ua_homomorphism.
 

diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v
@@ -4,7 +4,8 @@ Require Import HSet.
 Require Import TruncType.
 Require Import Colimits.GraphQuotient.
 Require Import Truncations.Core.
-Require Import PropResizing.
+
+Set Universe Minimization ToSet.
 
 Local Open Scope path_scope.
 
@@ -396,5 +397,6 @@ Definition quotient_kernel_factor_small@{a a' b ab | a < a', a <= ab, b <= ab}
       IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
 Proof.
   exact (quotient_kernel_factor_general@{a a a a' b ab ab}
-           f (fun a b => resize_hprop@{b a} (f a = f b)) (fun x y => equiv_resize_hprop _)).
+           f (fun a b => smalltype@{a b} (f a = f b))
+           (fun x y => (equiv_smalltype _)^-1%equiv)).
 Defined.
diff --git a/theories/Colimits/Quotient/Choice.v b/theories/Colimits/Quotient/Choice.v
@@ -1,7 +1,7 @@
 Require Import
   HoTT.Basics
   HoTT.Types
-  HoTT.HSet
+  HoTT.Universes.HSet
   HoTT.Truncations.Core
   HoTT.Colimits.Quotient
   HoTT.Projective.