From 09837f53361789131312979a725a0229460a4ab5 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 20 Oct 2023 17:17:09 +0200
Subject: [PATCH] rename axioms

---
 src/foundation-core/sets.lagda.md             | 17 +++++++-----
 src/foundation-core/univalence.lagda.md       | 26 ++++++++++++-------
 src/foundation/preunivalence.lagda.md         | 25 +++++++++++-------
 src/foundation/univalence.lagda.md            |  2 +-
 ...universal-property-identity-types.lagda.md |  8 +++---
 5 files changed, 47 insertions(+), 31 deletions(-)

diff --git a/src/foundation-core/sets.lagda.md b/src/foundation-core/sets.lagda.md
index 5ce7e3374c..cecd9e33de 100644
--- a/src/foundation-core/sets.lagda.md
+++ b/src/foundation-core/sets.lagda.md
@@ -55,11 +55,14 @@ 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}
@@ -67,16 +70,16 @@ module _
 
   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)
diff --git a/src/foundation-core/univalence.lagda.md b/src/foundation-core/univalence.lagda.md
index 3bc7bb2cd1..8bceae69f9 100644
--- a/src/foundation-core/univalence.lagda.md
+++ b/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,10 +58,10 @@ 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
 ```
 
@@ -63,10 +69,10 @@ abstract
 
 ```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)
 ```
 
diff --git a/src/foundation/preunivalence.lagda.md b/src/foundation/preunivalence.lagda.md
index a5027d3ee2..aee63e5691 100644
--- a/src/foundation/preunivalence.lagda.md
+++ b/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)
diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md
index 15f2058a79..e0804edd00 100644
--- a/src/foundation/univalence.lagda.md
+++ 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
diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index 5b1be62ef1..1a4d46a125 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/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