postfix axiom

src/foundation-core/univalence.lagda.md

@@ -43,14 +43,14 @@ map-eq = map-equiv ∘ equiv-eq
 instance-univalence : {l : Level} (A B : UU l) → UU (lsuc l)
 instance-univalence A B = is-equiv (equiv-eq {A = A} {B = B})
 
-axiom-based-univalence : {l : Level} (A : UU l) → UU (lsuc l)
-axiom-based-univalence {l} A = (B : UU l) → instance-univalence A B
+based-univalence-axiom : {l : Level} (A : UU l) → UU (lsuc l)
+based-univalence-axiom {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
+univalence-axiom-Level : (l : Level) → UU (lsuc l)
+univalence-axiom-Level l = (A B : UU l) → instance-univalence A B
 
-axiom-univalence : UUω
-axiom-univalence = {l : Level} → axiom-univalence-Level l
+univalence-axiom : UUω
+univalence-axiom = {l : Level} → univalence-axiom-Level l
 ```
 
 ## Properties
@@ -61,7 +61,7 @@ axiom-univalence = {l : Level} → axiom-univalence-Level l
 abstract
   is-torsorial-equiv-based-univalence :
     {l : Level} (A : UU l) →
-    axiom-based-univalence A → is-torsorial (λ (B : UU l) → A ≃ B)
+    based-univalence-axiom A → is-torsorial (λ (B : UU l) → A ≃ B)
   is-torsorial-equiv-based-univalence A UA =
     fundamental-theorem-id' (λ B → equiv-eq) UA
 ```
@@ -72,7 +72,7 @@ abstract
 abstract
   based-univalence-is-torsorial-equiv :
     {l : Level} (A : UU l) →
-    is-torsorial (λ (B : UU l) → A ≃ B) → axiom-based-univalence A
+    is-torsorial (λ (B : UU l) → A ≃ B) → based-univalence-axiom A
   based-univalence-is-torsorial-equiv A c =
     fundamental-theorem-id c (λ B → equiv-eq)
 ```

src/foundation/preunivalence.lagda.md

@@ -34,22 +34,22 @@ a common generalization of the [univalence axiom](foundation.univalence.md) and
 instance-preunivalence : {l : Level} (X Y : UU l) → UU (lsuc l)
 instance-preunivalence X Y = is-emb (equiv-eq {A = X} {B = Y})
 
-axiom-based-preunivalence : {l : Level} (X : UU l) → UU (lsuc l)
-axiom-based-preunivalence {l} X = (Y : UU l) → instance-preunivalence X Y
+based-preunivalence-axiom : {l : Level} (X : UU l) → UU (lsuc l)
+based-preunivalence-axiom {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
+preunivalence-axiom-Level : (l : Level) → UU (lsuc l)
+preunivalence-axiom-Level l = (X Y : UU l) → instance-preunivalence X Y
 
-axiom-preunivalence : UUω
-axiom-preunivalence = {l : Level} → axiom-preunivalence-Level l
+preunivalence-axiom : UUω
+preunivalence-axiom = {l : Level} → preunivalence-axiom-Level l
 
 emb-preunivalence :
-  axiom-preunivalence → {l : Level} (X Y : UU l) → (X ＝ Y) ↪ (X ≃ Y)
+  preunivalence-axiom → {l : Level} (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 :
-  axiom-preunivalence → {l : Level} (X Y : UU l) → (X ＝ Y) ↪ (X → Y)
+  preunivalence-axiom → {l : Level} (X Y : UU l) → (X ＝ Y) ↪ (X → Y)
 emb-map-preunivalence L X Y =
   comp-emb (emb-subtype is-equiv-Prop) (emb-preunivalence L X Y)
 ```
@@ -74,8 +74,8 @@ module _
       ( is-set-axiom-K K-Type A B)
       ( is-set-equiv-is-set (is-set-axiom-K K-A) (is-set-axiom-K K-B))
 
-axiom-preunivalence-axiom-K : axiom-K → axiom-preunivalence
-axiom-preunivalence-axiom-K K {l} X Y =
+preunivalence-axiom-axiom-K : axiom-K → preunivalence-axiom
+preunivalence-axiom-axiom-K K {l} X Y =
   instance-preunivalence-instance-axiom-K X Y (K (UU l)) (K X) (K Y)
 ```
 
@@ -90,16 +90,16 @@ module _
     instance-univalence A B → instance-preunivalence A B
   instance-preunivalence-instance-univalence = is-emb-is-equiv
 
-axiom-preunivalence-axiom-univalence : axiom-univalence → axiom-preunivalence
-axiom-preunivalence-axiom-univalence UA X Y =
+preunivalence-axiom-univalence-axiom : univalence-axiom → preunivalence-axiom
+preunivalence-axiom-univalence-axiom UA X Y =
   instance-preunivalence-instance-univalence X Y (UA X Y)
 ```
 
 ### Preunivalence holds in univalent foundations
 
 ```agda
-preunivalence : axiom-preunivalence
-preunivalence = axiom-preunivalence-axiom-univalence univalence
+preunivalence : preunivalence-axiom
+preunivalence = preunivalence-axiom-univalence-axiom univalence
 ```
 
 ## See also

src/foundation/replacement.lagda.md

@@ -32,19 +32,19 @@ instance-replacement :
 instance-replacement l {A = A} {B} f =
   is-small l A → is-locally-small l B → is-small l (im f)
 
-axiom-replacement-Level : (l l1 l2 : Level) → UU (lsuc l ⊔ lsuc l1 ⊔ lsuc l2)
-axiom-replacement-Level l l1 l2 =
+replacement-axiom-Level : (l l1 l2 : Level) → UU (lsuc l ⊔ lsuc l1 ⊔ lsuc l2)
+replacement-axiom-Level l l1 l2 =
   {A : UU l1} {B : UU l2} → (f : A → B) → instance-replacement l f
 
-axiom-replacement : UUω
-axiom-replacement = {l l1 l2 : Level} → axiom-replacement-Level l l1 l2
+replacement-axiom : UUω
+replacement-axiom = {l l1 l2 : Level} → replacement-axiom-Level l l1 l2
 ```
 
 ## Postulate
 
 ```agda
 postulate
-  replacement : axiom-replacement
+  replacement : replacement-axiom
 ```
 
 ```agda

src/foundation/univalence.lagda.md

@@ -41,7 +41,7 @@ In this file we postulate the univalence axiom. Its statement is defined in
 
 ```agda
 postulate
-  univalence : axiom-univalence
+  univalence : univalence-axiom
 ```
 
 ## Properties

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

@@ -148,11 +148,11 @@ module _
       ( λ _ → ap Id)
 
 module _
-  (L : axiom-preunivalence) {l : Level} (A : UU l)
+  (L : preunivalence-axiom) {l : Level} (A : UU l)
   where
 
-  is-emb-Id-axiom-preunivalence : is-emb (Id {A = A})
-  is-emb-Id-axiom-preunivalence =
+  is-emb-Id-preunivalence-axiom : is-emb (Id {A = A})
+  is-emb-Id-preunivalence-axiom =
     is-emb-Id-preunivalent-Id A (λ a x y → L (Id x y) (Id a y))
 ```
 
@@ -164,7 +164,7 @@ module _
   where
 
   is-emb-Id : is-emb (Id {A = A})
-  is-emb-Id = is-emb-Id-axiom-preunivalence preunivalence A
+  is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence 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