include PropResizing axiom

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Sep 24, 2024 · 151ae53 · 151ae53
1 parent 291a203
commit 151ae53
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
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.