rename axioms

src/foundation-core/sets.lagda.md

@@ -55,28 +55,31 @@ module _
 ### A type is a set if and only if it satisfies Streicher's axiom K
 
 ```agda
-statement-axiom-K : {l : Level} → UU l → UU l
-statement-axiom-K A = (x : A) (p : x ＝ x) → refl ＝ p
+instance-axiom-K : {l : Level} → UU l → UU l
+instance-axiom-K A = (x : A) (p : x ＝ x) → refl ＝ p
 
-axiom-K : (l : Level) → UU (lsuc l)
-axiom-K l = (A : UU l) → statement-axiom-K A
+axiom-K-Level : (l : Level) → UU (lsuc l)
+axiom-K-Level l = (A : UU l) → instance-axiom-K A
+
+axiom-K : UUω
+axiom-K = {l : Level} → axiom-K-Level l
 
 module _
   {l : Level} {A : UU l}
   where
 
   abstract
     is-set-axiom-K' :
-      statement-axiom-K A → (x y : A) → all-elements-equal (x ＝ y)
+      instance-axiom-K A → (x y : A) → all-elements-equal (x ＝ y)
     is-set-axiom-K' K x .x refl q with K x q
     ... | refl = refl
 
   abstract
-    is-set-axiom-K : statement-axiom-K A → is-set A
+    is-set-axiom-K : instance-axiom-K A → is-set A
     is-set-axiom-K H x y = is-prop-all-elements-equal (is-set-axiom-K' H x y)
 
   abstract
-    axiom-K-is-set : is-set A → statement-axiom-K A
+    axiom-K-is-set : is-set A → instance-axiom-K A
     axiom-K-is-set H x p =
       ( inv (contraction (is-proof-irrelevant-is-prop (H x x) refl) refl)) ∙
       ( contraction (is-proof-irrelevant-is-prop (H x x) refl) p)

src/foundation-core/univalence.lagda.md

@@ -39,11 +39,17 @@ equiv-eq refl = id-equiv
 map-eq : {l : Level} {A : UU l} {B : UU l} → A ＝ B → A → B
 map-eq = map-equiv ∘ equiv-eq
 
-statement-univalence : {l : Level} (A B : UU l) → UU (lsuc l)
-statement-univalence A B = is-equiv (equiv-eq {A = A} {B = B})
+instance-univalence : {l : Level} (A B : UU l) → UU (lsuc l)
+instance-univalence A B = is-equiv (equiv-eq {A = A} {B = B})
 
-axiom-univalence : (l : Level) → UU (lsuc l)
-axiom-univalence l = (A B : UU l) → statement-univalence A B
+axiom-based-univalence : {l : Level} (A : UU l) → UU (lsuc l)
+axiom-based-univalence {l} A = (B : UU l) → instance-univalence A B
+
+axiom-univalence-Level : (l : Level) → UU (lsuc l)
+axiom-univalence-Level l = (A B : UU l) → instance-univalence A B
+
+axiom-univalence : UUω
+axiom-univalence = {l : Level} → axiom-univalence-Level l
 ```
 
 ## Properties
@@ -52,21 +58,21 @@ axiom-univalence l = (A B : UU l) → statement-univalence A B
 
 ```agda
 abstract
-  is-contr-total-equiv-univalence :
+  is-contr-total-equiv-based-univalence :
     {l : Level} (A : UU l) →
-    ((B : UU l) → statement-univalence A B) → is-contr (Σ (UU l) (A ≃_))
-  is-contr-total-equiv-univalence A UA =
+    axiom-based-univalence A → is-contr (Σ (UU l) (A ≃_))
+  is-contr-total-equiv-based-univalence A UA =
     fundamental-theorem-id' (λ B → equiv-eq) UA
 ```
 
 ### Contractibility of the total space of equivalences implies univalence
 
 ```agda
 abstract
-  univalence-is-contr-total-equiv :
+  based-univalence-is-contr-total-equiv :
     {l : Level} (A : UU l) →
-    is-contr (Σ (UU l) (A ≃_)) → (B : UU l) → statement-univalence A B
-  univalence-is-contr-total-equiv A c =
+    is-contr (Σ (UU l) (A ≃_)) → axiom-based-univalence A
+  based-univalence-is-contr-total-equiv A c =
     fundamental-theorem-id c (λ B → equiv-eq)
 ```
 

src/foundation/preunivalence.lagda.md

@@ -32,21 +32,27 @@ K imply preunivalence.
 ## Definition
 
 ```agda
-statement-preunivalence : {l : Level} (X Y : UU l) → UU (lsuc l)
-statement-preunivalence X Y = is-emb (equiv-eq {A = X} {B = Y})
+instance-preunivalence : {l : Level} (X Y : UU l) → UU (lsuc l)
+instance-preunivalence X Y = is-emb (equiv-eq {A = X} {B = Y})
 
-axiom-preunivalence : (l : Level) → UU (lsuc l)
-axiom-preunivalence l = (X Y : UU l) → statement-preunivalence X Y
+axiom-based-preunivalence : {l : Level} (X : UU l) → UU (lsuc l)
+axiom-based-preunivalence {l} X = (Y : UU l) → instance-preunivalence X Y
+
+axiom-preunivalence-Level : (l : Level) → UU (lsuc l)
+axiom-preunivalence-Level l = (X Y : UU l) → instance-preunivalence X Y
+
+axiom-preunivalence : UUω
+axiom-preunivalence = {l : Level} → axiom-preunivalence-Level l
 
 emb-preunivalence :
-  {l : Level} → axiom-preunivalence l → (X Y : UU l) → (X ＝ Y) ↪ (X ≃ Y)
+  {l : Level} → axiom-preunivalence-Level l → (X Y : UU l) → (X ＝ Y) ↪ (X ≃ Y)
 pr1 (emb-preunivalence L X Y) = equiv-eq
 pr2 (emb-preunivalence L X Y) = L X Y
 
 emb-map-preunivalence :
-  {l : Level} → axiom-preunivalence l → (X Y : UU l) → (X ＝ Y) ↪ (X → Y)
+  {l : Level} → axiom-preunivalence-Level l → (X Y : UU l) → (X ＝ Y) ↪ (X → Y)
 emb-map-preunivalence L X Y =
-  comp-emb (emb-subtype is-equiv-Prop) (emb-preunivalence preuniv X Y)
+  comp-emb (emb-subtype is-equiv-Prop) (emb-preunivalence L X Y)
 ```
 
 ## Properties
@@ -55,7 +61,7 @@ emb-map-preunivalence L X Y =
 
 ```agda
 preunivalence-univalence :
-  {l : Level} → axiom-univalence l → axiom-preunivalence l
+  {l : Level} → axiom-univalence-Level l → axiom-preunivalence-Level l
 preunivalence-univalence ua A B = is-emb-is-equiv (ua A B)
 ```
 
@@ -66,7 +72,8 @@ types, and for the universe itself.
 
 ```agda
 preunivalence-axiom-K :
-  {l : Level} → axiom-K l → statement-axiom-K (UU l) → axiom-preunivalence l
+  {l : Level} →
+  axiom-K-Level l → instance-axiom-K (UU l) → axiom-preunivalence-Level l
 preunivalence-axiom-K K K-Type A B =
   is-emb-is-prop-is-set
     ( is-set-axiom-K K-Type A B)

src/foundation/univalence.lagda.md

@@ -39,7 +39,7 @@ In this file we postulate the univalence axiom. Its statement is defined in
 ## Postulate
 
 ```agda
-postulate univalence : {l : Level} → axiom-univalence l
+postulate univalence : {l : Level} → axiom-univalence-Level l
 ```
 
 ## Properties

src/foundation/universal-property-identity-types.lagda.md

@@ -113,11 +113,11 @@ In this composite, we used preunivalence at the second step.
 
 ```agda
 module _
-  {l : Level} (L : axiom-preunivalence l) (A : UU l)
+  {l : Level} (L : axiom-preunivalence-Level l) (A : UU l)
   where
 
-  is-emb-Id-axiom-preunivalence : is-emb (Id {A = A})
-  is-emb-Id-axiom-preunivalence a =
+  is-emb-Id-axiom-preunivalence-Level : is-emb (Id {A = A})
+  is-emb-Id-axiom-preunivalence-Level a =
     fundamental-theorem-id
       ( ( a , refl) ,
         ( λ _ →
@@ -157,7 +157,7 @@ module _
 
   is-emb-Id : is-emb (Id {A = A})
   is-emb-Id =
-    is-emb-Id-axiom-preunivalence (preunivalence-univalence univalence) A
+    is-emb-Id-axiom-preunivalence-Level (preunivalence-univalence univalence) A
 ```
 
 #### For any type family `B` over `A`, the type of pairs `(a , e)` consisting of `a : A` and a family of equivalences `e : (x : A) → (a ＝ x) ≃ B x` is a proposition