Rename Axiom L to Preunivalence

src/category-theory/categories.lagda.md

@@ -32,7 +32,7 @@ A **category** in Homotopy Type Theory is a
 [isomorphisms](category-theory.isomorphisms-in-precategories.md). More
 specifically, an equality between objects gives rise to an isomorphism between
 them, by the J-rule. A precategory is a category if this function, called
-`iso-eq`, is an [equivalence](foundation-core.equivalences.md). In particular.
+`iso-eq`, is an [equivalence](foundation-core.equivalences.md). In particular,
 being a category is a [proposition](foundation-core.propositions.md) since
 `is-equiv` is a proposition.
 

src/category-theory/preunivalent-categories.lagda.md

@@ -30,7 +30,7 @@ objects [embed](foundation-core.embeddings.md) into the
 [isomorphisms](category-theory.isomorphisms-in-precategories.md). More
 specifically, an equality between objects gives rise to an isomorphism between
 them, by the J-rule. A precategory is a preunivalent category if this function,
-called `iso-eq`, is an embedding. In particular. being preunivalent is a
+called `iso-eq`, is an embedding. In particular, being preunivalent is a
 [proposition](foundation-core.propositions.md) since `is-emb` is a proposition.
 
 The idea of preunivalence is that it is a common generalization of univalent
@@ -217,4 +217,4 @@ module _
 
 ## See also
 
-- [Axiom L](foundation.axiom-l.md)
+- [The preunivalence axiom](foundation.preunivalence.md)

src/foundation-core/sets.lagda.md

@@ -55,24 +55,28 @@ module _
 ### A type is a set if and only if it satisfies Streicher's axiom K
 
 ```agda
-axiom-K : {l : Level} → UU l → UU l
-axiom-K A = (x : A) (p : x ＝ x) → refl ＝ p
+statement-axiom-K : {l : Level} → UU l → UU l
+statement-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
 
 module _
   {l : Level} {A : UU l}
   where
 
   abstract
-    is-set-axiom-K' : axiom-K A → (x y : A) → all-elements-equal (x ＝ y)
+    is-set-axiom-K' :
+      statement-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 : axiom-K A → is-set A
+    is-set-axiom-K : statement-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 → axiom-K A
+    axiom-K-is-set : is-set A → statement-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,8 +39,11 @@ 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
 
-UNIVALENCE : {l : Level} (A B : UU l) → UU (lsuc l)
-UNIVALENCE A B = is-equiv (equiv-eq {A = A} {B = B})
+statement-univalence : {l : Level} (A B : UU l) → UU (lsuc l)
+statement-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
 ```
 
 ## Properties
@@ -49,21 +52,21 @@ UNIVALENCE A B = is-equiv (equiv-eq {A = A} {B = B})
 
 ```agda
 abstract
-  is-contr-total-equiv-UNIVALENCE :
+  is-contr-total-equiv-univalence :
     {l : Level} (A : UU l) →
-    ((B : UU l) → UNIVALENCE A B) → is-contr (Σ (UU l) (λ X → A ≃ X))
-  is-contr-total-equiv-UNIVALENCE A UA =
+    ((B : UU l) → statement-univalence A B) → is-contr (Σ (UU l) (A ≃_))
+  is-contr-total-equiv-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 :
+  univalence-is-contr-total-equiv :
     {l : Level} (A : UU l) →
-    is-contr (Σ (UU l) (λ X → A ≃ X)) → (B : UU l) → UNIVALENCE A B
-  UNIVALENCE-is-contr-total-equiv A c =
+    is-contr (Σ (UU l) (A ≃_)) → (B : UU l) → statement-univalence A B
+  univalence-is-contr-total-equiv A c =
     fundamental-theorem-id c (λ B → equiv-eq)
 ```
 

src/foundation.lagda.md

@@ -21,7 +21,6 @@ open import foundation.apartness-relations public
 open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
 open import foundation.arithmetic-law-product-and-pi-decompositions public
 open import foundation.automorphisms public
-open import foundation.axiom-l public
 open import foundation.axiom-of-choice public
 open import foundation.bands public
 open import foundation.binary-embeddings public
@@ -214,6 +213,7 @@ open import foundation.pointed-torsorial-type-families public
 open import foundation.powersets public
 open import foundation.preidempotent-maps public
 open import foundation.preimages-of-subtypes public
+open import foundation.preunivalence public
 open import foundation.principle-of-omniscience public
 open import foundation.product-decompositions public
 open import foundation.product-decompositions-subuniverse public

src/foundation/preunivalence.lagda.md

@@ -0,0 +1,82 @@
+# The preunivalence axiom
+
+```agda
+module foundation.preunivalence where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.univalence
+```
+
+</details>
+
+## Idea
+
+**The preunivalence axiom**, or **axiom L**, which is due to Peter Lumsdaine,
+asserts that for any two types `X` and `Y` in a common universe, the map
+`X ＝ Y → X ≃ Y` is an [embedding](foundation-core.embeddings.md). This axiom is
+a common generalization of the [univalence axiom](foundation.univalence.md) and
+[axiom K](foundation-core.sets.md), in the sense that both univalence and axiom
+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})
+
+axiom-preunivalence : (l : Level) → UU (lsuc l)
+axiom-preunivalence l = (X Y : UU l) → statement-preunivalence X Y
+
+emb-preunivalence :
+  {l : Level} → axiom-preunivalence 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)
+emb-map-preunivalence L X Y =
+  comp-emb (emb-subtype is-equiv-Prop) (emb-preunivalence preuniv X Y)
+```
+
+## Properties
+
+### Preunivalence generalizes univalence
+
+```agda
+preunivalence-univalence :
+  {l : Level} → axiom-univalence l → axiom-preunivalence l
+preunivalence-univalence ua A B = is-emb-is-equiv (ua A B)
+```
+
+### Preunivalence generalizes axiom K
+
+To show that preunivalence generalizes axiom K, we assume axiom K both for
+types, and for the universe itself.
+
+```agda
+preunivalence-axiom-K :
+  {l : Level} → axiom-K l → statement-axiom-K (UU l) → axiom-preunivalence l
+preunivalence-axiom-K K K-Type A B =
+  is-emb-is-prop-is-set
+    ( 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)))
+```
+
+## See also
+
+- Preunivalence is sufficient to prove that `Id : A → (A → 𝒰)` is an embedding.
+  This fact is proven in
+  [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md)

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} (A B : UU l) → UNIVALENCE A B
+postulate univalence : {l : Level} → axiom-univalence l
 ```
 
 ## Properties
@@ -86,7 +86,7 @@ module _
     is-contr-total-equiv :
       (A : UU l) → is-contr (Σ (UU l) (λ X → A ≃ X))
     is-contr-total-equiv A =
-      is-contr-total-equiv-UNIVALENCE A (univalence A)
+      is-contr-total-equiv-univalence A (univalence A)
 
     is-contr-total-equiv' :
       (A : UU l) → is-contr (Σ (UU l) (λ X → X ≃ A))

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

@@ -8,7 +8,6 @@ module foundation.universal-property-identity-types where
 
 ```agda
 open import foundation.action-on-identifications-functions
-open import foundation.axiom-l
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
@@ -17,6 +16,7 @@ open import foundation.function-extensionality
 open import foundation.functoriality-dependent-function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
+open import foundation.preunivalence
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.univalence
 open import foundation.universe-levels
@@ -34,9 +34,9 @@ open import foundation-core.propositions
 
 ## Idea
 
-The universal property of identity types characterizes families of maps out of
-the identity type. This universal property is also known as the type theoretic
-Yoneda lemma.
+The **universal property of identity types** characterizes families of maps out
+of the [identity type](foundation-core.identity-types.md). This universal
+property is also known as the **type theoretic Yoneda lemma**.
 
 ## Theorem
 
@@ -76,15 +76,16 @@ equiv-ev-refl' a {B} =
 
 ### `Id : A → (A → 𝒰)` is an embedding
 
-We first show that [axiom L](foundation.axiom-l.md) implies that the map
-`Id : A → (A → 𝒰)` is an [embedding](foundation.embeddings.md). Since the
-[univalence axiom](foundation.univalence.md) implies axiom L, it follows that
-`Id : A → (A → 𝒰)` is an embedding under the postulates of agda-unimath.
+We first show that [the preunivalence axiom](foundation.preunivalence.md)
+implies that the map `Id : A → (A → 𝒰)` is an
+[embedding](foundation.embeddings.md). Since the
+[univalence axiom](foundation.univalence.md) implies preunivalence, it follows
+that `Id : A → (A → 𝒰)` is an embedding under the postulates of agda-unimath.
 
-#### Axiom L implies that `Id : A → (A → 𝒰)` is an embedding
+#### Preunivalence implies that `Id : A → (A → 𝒰)` is an embedding
 
-The proof that axiom L implies that `Id : A → (A → 𝒰)` is an embedding proceeds
-via the
+The proof that preunivalence implies that `Id : A → (A → 𝒰)` is an embedding
+proceeds via the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md)
 by showing that the [fiber](foundation.fibers-of-maps.md) of `Id` at `Id a` is
 [contractible](foundation.contractible-types.md) for each `a : A`. To see this,
@@ -108,18 +109,17 @@ above embedding is constructed as the composite of the following embeddings
     ↪ Σ (x : A), a ＝ x.
 ```
 
-In this composite, we used axiom L at the second step.
+In this composite, we used preunivalence at the second step.
 
 ```agda
 module _
-  {l : Level} (L : axiom-L l) (A : UU l)
+  {l : Level} (L : axiom-preunivalence l) (A : UU l)
   where
 
-  is-emb-Id-axiom-L : is-emb (Id {A = A})
-  is-emb-Id-axiom-L a =
+  is-emb-Id-axiom-preunivalence : is-emb (Id {A = A})
+  is-emb-Id-axiom-preunivalence a =
     fundamental-theorem-id
-      ( pair
-        ( pair a refl)
+      ( ( a , refl) ,
         ( λ _ →
           is-injective-emb
             ( emb-fiber a)
@@ -143,7 +143,7 @@ module _
             ( id-emb)
             ( λ x →
               comp-emb
-                ( emb-Π (λ y → emb-L L (Id x y) (Id a y)))
+                ( emb-Π (λ y → emb-preunivalence L (Id x y) (Id a y)))
                 ( emb-equiv equiv-funext))))
         ( emb-equiv (inv-equiv (equiv-fiber Id (Id a))))
 ```
@@ -156,7 +156,8 @@ module _
   where
 
   is-emb-Id : is-emb (Id {A = A})
-  is-emb-Id = is-emb-Id-axiom-L (axiom-L-univalence univalence) A
+  is-emb-Id =
+    is-emb-Id-axiom-preunivalence (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
@@ -195,11 +196,12 @@ module _
 
 - In
   [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md)
-  we will show that the fiber of `Id : A → (A → 𝒰)`at`B : A → 𝒰`is equivalent
-  to`is-contr (Σ A B)`.
+  we will show that the fiber of `Id : A → (A → 𝒰)` at `B : A → 𝒰` is equivalent
+  to `is-contr (Σ A B)`.
 
 ## References
 
-- The fact that axiom L is sufficient to prove that `Id : A → (A → 𝒰)` is an
-  embedding was first observed and formalized by Martín Escardó,
+- The fact that preunivalence, or axiom L, is sufficient to prove that
+  `Id : A → (A → 𝒰)` is an embedding was first observed and formalized by Martín
+  Escardó,
   [https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html).