preliminary work for something to come

martinescardo · Aug 25, 2023 · 54a736a · 54a736a
1 parent 67495b5
commit 54a736a
Show file tree

Hide file tree

Showing 11 changed files with 118 additions and 42 deletions.
diff --git a/source/InjectiveTypes/CounterExamples.lagda b/source/InjectiveTypes/CounterExamples.lagda
@@ -33,6 +33,7 @@ module InjectiveTypes.CounterExamples
 open PropositionalTruncation pt
 
 open import MLTT.Spartan
+open import Taboos.Decomposability ua
 open import UF.Embeddings
 open import UF.ExcludedMiddle
 open import UF.FunExt
@@ -41,7 +42,6 @@ open import UF.Retracts
 open import UF.Subsingletons
 open import UF.Subsingletons-FunExt
 open import UF.UA-FunExt
-open import Taboos.Decomposability ua
 
 private
  fe : FunExt
@@ -50,8 +50,11 @@ private
  fe' : Fun-Ext
  fe' {𝓤} {𝓥} = fe 𝓤 𝓥
 
- pe : Prop-Ext
- pe = Univalence-gives-Prop-Ext ua
+ pe : PropExt
+ pe = Univalence-gives-PropExt ua
+
+ pe' : Prop-Ext
+ pe' {𝓤} = pe 𝓤
 
 open import InjectiveTypes.Blackboard fe
 open import TypeTopology.SimpleTypes fe pt
@@ -98,7 +101,7 @@ WEM-gives-𝟚-retract-of-Ω {𝓤} wem = II
 
 WEM-gives-𝟚-ainjective : WEM 𝓤 → ainjective-type 𝟚 𝓤 𝓤
 WEM-gives-𝟚-ainjective {𝓤} wem =
- retract-of-ainjective 𝟚 (Ω 𝓤) (Ω-ainjective pe) (WEM-gives-𝟚-retract-of-Ω wem)
+ retract-of-ainjective 𝟚 (Ω 𝓤) (Ω-ainjective pe') (WEM-gives-𝟚-retract-of-Ω wem)
 
 WEM-gives-𝟚-aflabby : WEM 𝓤 → aflabby 𝟚 𝓤
 WEM-gives-𝟚-aflabby wem = ainjective-types-are-aflabby 𝟚 (WEM-gives-𝟚-ainjective wem)
@@ -144,8 +147,8 @@ universe 𝓤₁.
 
 \begin{code}
 
-open import DedekindReals.Type fe' pe pt
-open import DedekindReals.Order fe' pe pt
+open import DedekindReals.Type fe' pe' pt
+open import DedekindReals.Order fe' pe' pt
 open import Notation.Order
 
 ℝ-ainjective-gives-Heaviside-function : ainjective-type ℝ 𝓤₁ 𝓤₁
@@ -220,13 +223,13 @@ open import Rationals.Order
   I-II u v = contrapositive II v (contrapositive I u)
 
   I-II₀ : r ≠ 1ℝ → r ＝ 0ℝ
-  I-II₀ v = ℝ-is-¬¬-separated (r) 0ℝ (λ u → I-II u v)
+  I-II₀ v = ℝ-is-¬¬-separated r 0ℝ (λ u → I-II u v)
 
   I-II₁ : r ≠ 0ℝ → r ＝ 1ℝ
-  I-II₁ u = ℝ-is-¬¬-separated (r) 1ℝ (I-II u)
+  I-II₁ u = ℝ-is-¬¬-separated r 1ℝ (I-II u)
 
   III : (1/4 < r) ∨ (r < 1/2)
-  III = ℝ-locatedness (r) 1/4 1/2 1/4<1/2
+  III = ℝ-locatedness r 1/4 1/2 1/4<1/2
 
   IV : 1/4 < r → r ＝ 1ℝ
   IV l = I-II₁ IV₀

diff --git a/source/Iterative/Multisets-Addendum.lagda b/source/Iterative/Multisets-Addendum.lagda
@@ -14,12 +14,12 @@ open import MLTT.Spartan
 open import UF.Univalence
 
 module Iterative.Multisets-Addendum
-        (𝓤 : Universe)
         (ua : Univalence)
+        {𝓤 : Universe}
        where
 
 open import Iterative.Multisets 𝓤
-open import Iterative.Sets 𝓤 ua
+open import Iterative.Sets ua {𝓤}
 open import Taboos.Decomposability ua
 open import UF.Base
 open import UF.Embeddings

diff --git a/source/Iterative/Ordinals-Addendum.lagda b/source/Iterative/Ordinals-Addendum.lagda
@@ -13,8 +13,8 @@ open import MLTT.Spartan
 open import UF.Univalence
 
 module Iterative.Ordinals-Addendum
-        (𝓤 : Universe)
         (ua : Univalence)
+        {𝓤 : Universe}
        where
 
 open import UF.FunExt
@@ -39,8 +39,8 @@ add all we wanted to add, and clean-up when we finish.
 
 open import InjectiveTypes.Blackboard fe'
 open import Iterative.Multisets 𝓤
-open import Iterative.Ordinals 𝓤 ua
-open import Iterative.Sets 𝓤 ua
+open import Iterative.Ordinals ua {𝓤}
+open import Iterative.Sets ua {𝓤}
 open import Ordinals.Injectivity
 open import Ordinals.OrdinalOfOrdinals ua
 open import Ordinals.Type hiding (Ord)

diff --git a/source/Iterative/Ordinals.lagda b/source/Iterative/Ordinals.lagda
@@ -36,8 +36,8 @@ open import MLTT.Spartan
 open import UF.Univalence
 
 module Iterative.Ordinals
-        (𝓤 : Universe)
         (ua : Univalence)
+        {𝓤 : Universe}
        where
 
 open import UF.FunExt
@@ -54,7 +54,7 @@ private
  fe' 𝓤 𝓥 = fe {𝓤} {𝓥}
 
 open import Iterative.Multisets 𝓤
-open import Iterative.Sets 𝓤 ua
+open import Iterative.Sets ua {𝓤}
 open import Ordinals.Equivalence
 open import Ordinals.Notions
 open import Ordinals.OrdinalOfOrdinals ua

diff --git a/source/Iterative/Sets-Addendum.lagda b/source/Iterative/Sets-Addendum.lagda
@@ -12,13 +12,13 @@ open import MLTT.Spartan
 open import UF.Univalence
 
 module Iterative.Sets-Addendum
-        (𝓤 : Universe)
         (ua : Univalence)
+        {𝓤 : Universe}
        where
 
 open import Iterative.Multisets 𝓤
-open import Iterative.Multisets-Addendum 𝓤 ua
-open import Iterative.Sets 𝓤 ua
+open import Iterative.Multisets-Addendum ua {𝓤}
+open import Iterative.Sets ua {𝓤}
 open import Taboos.Decomposability ua
 open import UF.ExcludedMiddle
 open import UF.FunExt

diff --git a/source/Iterative/Sets.lagda b/source/Iterative/Sets.lagda
@@ -23,8 +23,8 @@ open import MLTT.Spartan
 open import UF.Univalence
 
 module Iterative.Sets
-        (𝓤 : Universe)
         (ua : Univalence)
+        {𝓤 : Universe}
        where
 
 open import UF.FunExt

diff --git a/source/TypeTopology/DiscreteAndSeparated.lagda b/source/TypeTopology/DiscreteAndSeparated.lagda
@@ -530,7 +530,8 @@ Another logical place for these three lemmas would be Negation.lagda, but
 
 being-¬¬-stable-is-prop : {X : 𝓤 ̇ }
                         → funext 𝓤 𝓤
-                        → is-prop X → is-prop (¬¬-stable X)
+                        → is-prop X
+                        → is-prop (¬¬-stable X)
 being-¬¬-stable-is-prop fe i = Π-is-prop fe (λ _ → i)
 
 Ω¬¬ : (𝓤 : Universe)  → 𝓤 ⁺ ̇

diff --git a/source/UF/Embeddings.lagda b/source/UF/Embeddings.lagda
@@ -193,13 +193,18 @@ embedding-gives-embedding' {𝓤} {𝓥} {X} {Y} f ise = g
          (center (c x))
          (centrality (c x)))
 
+embedding-criterion-converse' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
+                             → is-embedding f
+                             → (x' x : X)
+                             → (x' ＝ x) ≃ (f x' ＝ f x)
+embedding-criterion-converse' f e x' x = ap f {x'} {x} ,
+                                         embedding-gives-embedding' f e x' x
+
 embedding-criterion-converse : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                              → is-embedding f
                              → (x' x : X)
                              → (f x' ＝ f x) ≃ (x' ＝ x)
-embedding-criterion-converse f e x' x = ≃-sym
-                                         (ap f {x'} {x} ,
-                                          embedding-gives-embedding' f e x' x)
+embedding-criterion-converse f e x' x = ≃-sym (embedding-criterion-converse' f e x' x)
 
 embedding'-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                        (f : X → Y)

diff --git a/source/UF/Miscelanea.lagda b/source/UF/Miscelanea.lagda
@@ -338,3 +338,62 @@ constant-maps-are-h-isolated fe y₀ y₀-iso {f} = II
   II = equiv-to-prop I (Π-is-prop fe (λ _ → y₀-iso))
 
 \end{code}
+
+Added 25 August 2023.
+
+\begin{code}
+
+open import TypeTopology.DiscreteAndSeparated
+
+Ω¬¬-is-set : FunExt
+           → PropExt
+           → is-set (Ω¬¬ 𝓤)
+Ω¬¬-is-set {𝓤} fe pe = ¬¬-separated-types-are-sets
+                        (fe (𝓤 ⁺) 𝓤₀)
+                        (Ω¬¬-is-¬¬-separated (fe 𝓤 𝓤) (pe 𝓤))
+
+𝟘-is-¬¬-stable : ¬¬ 𝟘 {𝓤} → 𝟘 {𝓥}
+𝟘-is-¬¬-stable ϕ = 𝟘-elim (ϕ 𝟘-elim)
+
+𝟙-is-¬¬-stable : ¬¬ 𝟙 {𝓤} → 𝟙 {𝓥}
+𝟙-is-¬¬-stable _ = ⋆
+
+⊥Ω¬¬ ⊤Ω¬¬ : Ω¬¬ 𝓤
+⊥Ω¬¬ = ⊥ , 𝟘-is-¬¬-stable
+⊤Ω¬¬ = ⊤ , 𝟙-is-¬¬-stable
+
+𝟚-to-Ω¬¬ : 𝟚 → Ω¬¬ 𝓤
+𝟚-to-Ω¬¬ ₀ = ⊥Ω¬¬
+𝟚-to-Ω¬¬ ₁ = ⊤Ω¬¬
+
+module _ (fe : FunExt) (pe : PropExt) where
+
+ 𝟚-to-Ω¬¬-is-embedding : is-embedding (𝟚-to-Ω¬¬ {𝓤})
+ 𝟚-to-Ω¬¬-is-embedding _ (₀ , p) (₀ , q) = to-Σ-＝ (refl , Ω¬¬-is-set fe pe p q)
+ 𝟚-to-Ω¬¬-is-embedding _ (₀ , p) (₁ , q) = 𝟘-elim (⊥-is-not-⊤ (ap pr₁ p ∙ (ap pr₁ q)⁻¹))
+ 𝟚-to-Ω¬¬-is-embedding _ (₁ , p) (₀ , q) = 𝟘-elim (⊥-is-not-⊤ (ap pr₁ q ∙ (ap pr₁ p ⁻¹)))
+ 𝟚-to-Ω¬¬-is-embedding _ (₁ , p) (₁ , q) = to-Σ-＝ (refl , Ω¬¬-is-set fe pe p q)
+
+ 𝟚-to-Ω¬¬-fiber : ((p , s) : Ω¬¬ 𝓤) → fiber 𝟚-to-Ω¬¬ (p , s) ≃ (¬ (p holds) + p holds)
+ 𝟚-to-Ω¬¬-fiber {𝓤} 𝕡@(p , s) =
+  fiber (𝟚-to-Ω¬¬ {𝓤}) 𝕡                        ≃⟨ ≃-refl _ ⟩
+  (Σ n ꞉ 𝟚 , 𝟚-to-Ω¬¬ {𝓤} n ＝ 𝕡 )              ≃⟨ alternative-+ ⟩
+  (𝟚-to-Ω¬¬ ₀ ＝ p , s) + (𝟚-to-Ω¬¬ ₁ ＝ p , s) ≃⟨ I ⟩
+  (⊥ ＝ p) + (⊤ ＝ p)                           ≃⟨ II ⟩
+  (¬ (p holds) + (p holds))                     ■
+  where
+   I = +-cong
+        (embedding-criterion-converse' pr₁
+          (pr₁-is-embedding (λ p → being-¬¬-stable-is-prop (fe _ _) (holds-is-prop p))) _ _)
+        (embedding-criterion-converse' pr₁
+          (pr₁-is-embedding (λ p → being-¬¬-stable-is-prop (fe _ _) (holds-is-prop p))) _ _)
+
+   II = +-cong
+           (＝-flip ● equal-⊥-≃ (pe _) (fe _ _) p)
+           (＝-flip ● equal-⊤-≃ (pe _) (fe _ _) p)
+
+ 𝟚-to-Ω¬¬-is-small-map : (𝟚-to-Ω¬¬ {𝓤}) is 𝓤 small-map
+ 𝟚-to-Ω¬¬-is-small-map (p , s) = (¬ (p holds) + p holds) ,
+                                   ≃-sym (𝟚-to-Ω¬¬-fiber (p , s))
+
+\end{code}
diff --git a/source/UF/Size.lagda b/source/UF/Size.lagda
@@ -58,6 +58,9 @@ equivalent to a type in the universe 𝓥:
 _is_small : 𝓤 ̇ → (𝓥 : Universe) → 𝓥 ⁺  ⊔ 𝓤 ̇
 X is 𝓥 small = Σ Y ꞉ 𝓥 ̇ , Y ≃ X
 
+native-size : (X : 𝓤 ̇ ) → X is 𝓤 small
+native-size X = X , ≃-refl X
+
 resized : (X : 𝓤 ̇ ) → X is 𝓥 small → 𝓥 ̇
 resized X = pr₁
 
@@ -700,6 +703,10 @@ f is 𝓦 small-map = ∀ y → fiber f y is 𝓦 small
 _is-small-map : {X Y : 𝓤 ⁺ ̇ } → (X → Y) → 𝓤 ⁺ ̇
 _is-small-map {𝓤} f = f is 𝓤 small-map
 
+native-size-of-map : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
+                   → f is 𝓤 ⊔ 𝓥 small-map
+native-size-of-map f y = native-size (fiber f y)
+
 \end{code}
 
 Obsolete notation used in some publications:
@@ -793,30 +800,38 @@ size-of-section-embedding {𝓤} {𝓥} {X} {Y} s (r , η) e y = γ
   γ : (fiber s y) is 𝓥 small
   γ = B , δ
 
-section-embedding-size-contravariance : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
-                                      → is-embedding f
-                                      → is-section f
+section-embedding-size-contravariance : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (s : X → Y)
+                                      → is-embedding s
+                                      → is-section s
                                       → Y is 𝓦 small
                                       → X is 𝓦 small
-section-embedding-size-contravariance {𝓤} {𝓥} {𝓦} {X} {Y} f e (g , η) (Y' , h , i) = γ
+section-embedding-size-contravariance {𝓤} {𝓥} {𝓦} {X} {Y} s e (g , η) (Y' , h , i) = γ
  where
   h⁻¹ : Y → Y'
   h⁻¹ = inverse h i
 
-  f' : X → Y'
-  f' = h⁻¹ ∘ f
+  s' : X → Y'
+  s' = h⁻¹ ∘ s
 
-  η' = λ x → g (h (h⁻¹ (f x))) ＝⟨ ap g (inverses-are-sections h i (f x)) ⟩
-             g (f x)           ＝⟨ η x ⟩
+  η' = λ x → g (h (h⁻¹ (s x))) ＝⟨ ap g (inverses-are-sections h i (s x)) ⟩
+             g (s x)           ＝⟨ η x ⟩
              x                 ∎
 
-  δ : f' is 𝓦 small-map
-  δ = size-of-section-embedding f' (g ∘ h , η')
+  δ : s' is 𝓦 small-map
+  δ = size-of-section-embedding s' (g ∘ h , η')
        (∘-is-embedding e (equivs-are-embeddings h⁻¹
                          (inverses-are-equivs h i)))
 
   γ : X is 𝓦 small
-  γ = size-contravariance f' δ (Y' , ≃-refl Y')
+  γ = size-contravariance s' δ (Y' , ≃-refl Y')
+
+embedded-retract-is-small : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
+                            (ρ : retract X of Y)
+                          → is-embedding (section ρ)
+                          → Y is 𝓦 small
+                          → X is 𝓦 small
+embedded-retract-is-small (r , s , rs) s-is-embedding Y-is-small =
+ section-embedding-size-contravariance s s-is-embedding (r , rs) Y-is-small
 
 ≃-size-contravariance : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                       → X ≃ Y

diff --git a/source/UF/SmallnessProperties.lagda b/source/UF/SmallnessProperties.lagda
@@ -23,13 +23,6 @@ open import UF.PropTrunc
 open import UF.Size
 open import UF.Subsingletons
 
-native-size : (X : 𝓤 ̇ ) → X is 𝓤 small
-native-size X = X , ≃-refl X
-
-native-size-of-map : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
-                   → f is 𝓤 ⊔ 𝓥 small-map
-native-size-of-map f y = native-size (fiber f y)
-
 smallness-closed-under-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                          → X is 𝓦 small
                          → X ≃ Y