better terminology

martinescardo · Jan 3, 2025 · 80f5919 · 80f5919
1 parent 84f6b4a
commit 80f5919
Show file tree

Hide file tree

Showing 9 changed files with 21 additions and 21 deletions.
diff --git a/source/AllModulesIndex.lagda b/source/AllModulesIndex.lagda
@@ -6,7 +6,7 @@
 
    Tested with Agda 2.7.0.1. (It may still work with Agda 2.6.4.3.)
 
-   Martin Escardo and collaborators, 2010--2024--∞
+   Martin Escardo and collaborators, 2010--2025--∞
    Continuously evolving.
 
    https://github.com/martinescardo/TypeTopology

diff --git a/source/Fin/ArithmeticViaEquivalence.lagda b/source/Fin/ArithmeticViaEquivalence.lagda
@@ -497,7 +497,7 @@ open import UF.PropIndexedPiSigma
 Σ-construction : (n : ℕ) (a : Fin n → ℕ)
                → Σ k ꞉ ℕ , Fin k ≃ (Σ i ꞉ Fin n , Fin (a i))
 Σ-construction 0 a = 0 , (Fin 0                    ≃⟨ ≃-refl _ ⟩
-                         𝟘                        ≃⟨ ≃-sym (prop-indexed-sum-zero id) ⟩
+                         𝟘                        ≃⟨ ≃-sym (empty-indexed-sum-is-𝟘 id) ⟩
                          (Σ i ꞉ 𝟘 , Fin (a i)) ■)
 Σ-construction (succ n) a = g
  where
@@ -565,7 +565,7 @@ module _ (fe : funext 𝓤₀ 𝓤₀) where
   where
    i   = ≃-refl _
    ii  = 𝟘-lneutral
-   iii = ≃-sym (prop-indexed-product-one fe id)
+   iii = ≃-sym (empty-indexed-product-is-𝟙 fe id)
    iv  = ≃-refl _
 
  Π-construction (succ n) a = g

diff --git a/source/Games/Discussion.lagda b/source/Games/Discussion.lagda
@@ -512,10 +512,10 @@ hg-path (Xt , d) = γ Xt d
      have-e = e
 
      I : is-empty X ≃ 𝟙
-     I = prop-indexed-product-one fe (λ x → e ∣ x ∣)
+     I = empty-indexed-product-is-𝟙 fe (λ x → e ∣ x ∣)
 
      II : (Σ x ꞉ X , 𝔸-Path (Xf x)) ≃ 𝟘
-     II = prop-indexed-sum-zero (λ x → e ∣ x ∣)
+     II = empty-indexed-sum-is-𝟘 (λ x → e ∣ x ∣)
 
      III = +-cong I II
 

diff --git a/source/GamesExperimental/Discussion.lagda b/source/GamesExperimental/Discussion.lagda
@@ -519,10 +519,10 @@ hg-path (Xt , d) = γ Xt d
      have-e = e
 
      I : is-empty X ≃ 𝟙
-     I = prop-indexed-product-one fe (λ x → e ∣ x ∣)
+     I = empty-indexed-product-is-𝟙 fe (λ x → e ∣ x ∣)
 
      II : (Σ x ꞉ X , 𝔸-Path (Xf x)) ≃ 𝟘
-     II = prop-indexed-sum-zero (λ x → e ∣ x ∣)
+     II = empty-indexed-sum-is-𝟘 (λ x → e ∣ x ∣)
 
      III = +-cong I II
 

diff --git a/source/InjectiveTypes/Article.lagda b/source/InjectiveTypes/Article.lagda
@@ -354,15 +354,15 @@ give 𝟘 and 𝟙 respectively:
                          → (y : Y)
                          → ((x : X) → j x ≠ y)
                          → (f ↓ j) y ≃ 𝟘 {𝓣}
-Σ-extension-out-of-range f j y φ = prop-indexed-sum-zero (uncurry φ)
+Σ-extension-out-of-range f j y φ = empty-indexed-sum-is-𝟘 (uncurry φ)
 
 
 Π-extension-out-of-range : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → 𝓦 ̇ ) (j : X → Y)
                          → (y : Y)
                          → ((x : X) → j x ≠ y)
                          → (f ↑ j) y ≃ 𝟙 {𝓣}
 Π-extension-out-of-range {𝓤} {𝓥} {𝓦} f j y φ =
- prop-indexed-product-one (fe (𝓤 ⊔ 𝓥) 𝓦) (uncurry φ)
+ empty-indexed-product-is-𝟙 (fe (𝓤 ⊔ 𝓥) 𝓦) (uncurry φ)
 
 \end{code}
 

diff --git a/source/InjectiveTypes/Blackboard.lagda b/source/InjectiveTypes/Blackboard.lagda
@@ -303,14 +303,14 @@ module _ {X : 𝓤 ̇ }
   Π-extension-out-of-range : {𝓦 : Universe} (y : Y)
                            → ((x : X) → j x ≠ y) → f/j (y) ≃ 𝟙 {𝓦}
   Π-extension-out-of-range y φ =
-   prop-indexed-product-one (fe (𝓤 ⊔ 𝓥) 𝓦) (uncurry φ)
+   empty-indexed-product-is-𝟙 (fe (𝓤 ⊔ 𝓥) 𝓦) (uncurry φ)
 
   Σ-extension-property : is-embedding j → (x : X) → f∖j (j x) ≃ f x
   Σ-extension-property e x = prop-indexed-sum (e (j x)) (x , refl)
 
   Σ-extension-out-of-range : {𝓦 : Universe} (y : Y)
                            → ((x : X) → j x ≠ y) → f∖j (y) ≃ 𝟘 {𝓦}
-  Σ-extension-out-of-range y φ = prop-indexed-sum-zero (uncurry φ)
+  Σ-extension-out-of-range y φ = empty-indexed-sum-is-𝟘 (uncurry φ)
 
 \end{code}
 

diff --git a/source/UF/PropIndexedPiSigma.lagda b/source/UF/PropIndexedPiSigma.lagda
@@ -50,11 +50,11 @@ prop-indexed-product : funext 𝓤 𝓥
                      → (a : X) → Π Y ≃ Y a
 prop-indexed-product fe i a = Π-proj a , Π-proj-is-equiv fe i a
 
-prop-indexed-product-one : funext 𝓤 𝓥
-                         → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
-                         → (X → 𝟘 {𝓦})
-                         → Π Y ≃ 𝟙 {𝓣}
-prop-indexed-product-one {𝓤} {𝓥} {𝓦} {𝓣} fe {X} {Y} v = γ
+empty-indexed-product-is-𝟙 : funext 𝓤 𝓥
+                           → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
+                           → (X → 𝟘 {𝓦})
+                           → Π Y ≃ 𝟙 {𝓣}
+empty-indexed-product-is-𝟙 {𝓤} {𝓥} {𝓦} {𝓣} fe {X} {Y} v = γ
  where
   g : 𝟙 → Π Y
   g ⋆ x = unique-from-𝟘 {𝓥} {𝓦} (v x)
@@ -100,10 +100,10 @@ prop-indexed-sum {𝓤} {𝓥} {X} {Y} i a = qinveq f (g , ε , η)
   ε : (σ : Σ Y) → g (f σ) ＝ σ
   ε (x , y) = to-Σ-＝ (i a x , c x y (i x a))
 
-prop-indexed-sum-zero : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
+empty-indexed-sum-is-𝟘 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
                       → (X → 𝟘 {𝓦})
                       → Σ Y ≃ (𝟘 {𝓣})
-prop-indexed-sum-zero {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} φ = qinveq f (g , ε , η)
+empty-indexed-sum-is-𝟘 {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} φ = qinveq f (g , ε , η)
  where
   f : Σ Y → 𝟘
   f (x , y) = 𝟘-elim (φ x)

diff --git a/source/W/Numbers.lagda b/source/W/Numbers.lagda
@@ -266,7 +266,7 @@ by 𝓕𝓲𝓷 : 𝓝 → 𝓥.
  Fin-factor : (n : ℕ) → 𝓕𝓲𝓷 (ℕ-to-𝓝 n) ≃ Fin n
  Fin-factor zero =
   𝟘 + (Σ h ꞉ 𝟘 , 𝓕𝓲𝓷 (𝟘-elim h)) ≃⟨ 𝟘-lneutral ⟩
-  (Σ h ꞉ 𝟘 , 𝓕𝓲𝓷 (𝟘-elim h))     ≃⟨ prop-indexed-sum-zero id ⟩
+  (Σ h ꞉ 𝟘 , 𝓕𝓲𝓷 (𝟘-elim h))     ≃⟨ empty-indexed-sum-is-𝟘 id ⟩
   𝟘                              ■
 
  Fin-factor (succ n) = I

diff --git a/source/index.lagda b/source/index.lagda
@@ -4,7 +4,7 @@
    -------------------------------------------------------------
 
    Martin Escardo and collaborators,
-   2010--2024--∞, continuously evolving.
+   2010--2025--∞, continuously evolving.
    https://www.cs.bham.ac.uk/~mhe/
    https://github.com/martinescardo/TypeTopology
 
@@ -55,7 +55,7 @@
 
      (https://www.cs.bham.ac.uk/~mhe/TypeTopology/AllModulesIndex.html)
 
-   * In our last count, on 2024.12.18, this development has 796 Agda
+   * In our last count, on 2024.12.18, this development has 797 Agda
      files with 229K lines of code, including comments and blank
      lines.