A few lemmas for the formalizations of connections between small and connected types

source/UF/H-Levels.lagda

@@ -25,6 +25,7 @@ open import UF.EquivalenceExamples
 open import UF.Equiv-FunExt
 open import UF.FunExt
 open import UF.IdentitySystems
+open import UF.PropTrunc
 open import UF.Retracts
 open import UF.Sets
 open import UF.Singleton-Properties
@@ -35,7 +36,10 @@ open import UF.Univalence
 open import UF.UA-FunExt
 open import Naturals.Order
 
-module UF.H-Levels (fe : FunExt) (fe' : Fun-Ext) where
+module UF.H-Levels (fe : FunExt)
+                   (fe' : Fun-Ext)
+                   (pt : propositional-truncations-exist)
+                    where
 
 _is-of-hlevel_ : 𝓤 ̇ → ℕ → 𝓤 ̇
 X is-of-hlevel zero = is-contr X
@@ -126,7 +130,7 @@ Using closure under equivalence we can show closure under Σ and Π.
 \begin{code}
 
 hlevel-closed-under-Σ : (n : ℕ)
-                      → (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
+                      → (X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ )
                       → X is-of-hlevel n
                       → ((x : X) → (Y x) is-of-hlevel n)
                       → (Σ Y) is-of-hlevel n
@@ -141,17 +145,24 @@ hlevel-closed-under-Σ (succ n) X Y l m (x , y) (x' , y') =
                                                             (transport Y p y)
                                                             y'))
 
-hlevel-closed-under-Π : {𝓤 : Universe}
+hlevel-closed-under-Π : {𝓤 𝓥 : Universe}
                       → (n : ℕ)
-                      → (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
+                      → (X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ )
                       → ((x : X) → (Y x) is-of-hlevel n)
                       → (Π Y) is-of-hlevel n
-hlevel-closed-under-Π {𝓤} zero X Y m = Π-is-singleton (fe 𝓤 𝓤) m
-hlevel-closed-under-Π {𝓤} (succ n) X Y m f g =
-  hlevel-closed-under-equiv n (f ＝ g) (f ∼ g) (happly-≃ (fe 𝓤 𝓤))
+hlevel-closed-under-Π {𝓤} {𝓥} zero X Y m = Π-is-singleton (fe 𝓤 𝓥) m
+hlevel-closed-under-Π {𝓤} {𝓥} (succ n) X Y m f g = 
+  hlevel-closed-under-equiv n (f ＝ g) (f ∼ g) (happly-≃ (fe 𝓤 𝓥))
                             (hlevel-closed-under-Π n X (λ x → f x ＝ g x)
                                                    (λ x → m x (f x) (g x)))
 
+hlevel-closed-under-→ : {𝓤 𝓥 : Universe}
+                      → (n : ℕ)
+                      → (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
+                      → Y is-of-hlevel n
+                      → (X → Y) is-of-hlevel n
+hlevel-closed-under-→ n X Y m = hlevel-closed-under-Π n X (λ - → Y) (λ - → m)
+
 \end{code}
 
 The subuniverse of types of hlevel n is defined as follows.
@@ -241,30 +252,247 @@ We now define the notion of a k-truncation using record types.
 
 record H-level-truncations-exist : 𝓤ω where
  field
-  ∣∣_∣∣_ : {𝓤 : Universe} → 𝓤 ̇ → ℕ → 𝓤 ̇
-  ∣∣∣∣-is-prop : {𝓤 : Universe} {X : 𝓤 ̇ } {n : ℕ} → is-prop (∣∣ X ∣∣ n)
-  ∣_∣_ :  {𝓤 : Universe} {X : 𝓤 ̇ } → X → (n : ℕ) → ∣∣ X ∣∣ n
-  ∣∣∣∣-rec : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
-           → Y is-of-hlevel n → (X → Y) → ∣∣ X ∣∣ n → Y
- infix 0 ∣∣_∣∣_
- infix 0 ∣_∣_
+  ∣∣_∣∣[_] : {𝓤 : Universe} → 𝓤 ̇ → ℕ → 𝓤 ̇
+  ∣∣∣∣-h-level : {𝓤 : Universe} {X : 𝓤 ̇ } (n : ℕ) → X is-of-hlevel n
+  ∣_∣[_] :  {𝓤 : Universe} {X : 𝓤 ̇ } → X → (n : ℕ) → ∣∣ X ∣∣[ n ]
+  ∣∣∣∣-ind : {X : 𝓤 ̇ } {n : ℕ} {P : ∣∣ X ∣∣[ n ] → 𝓥 ̇ }
+           → ((s : ∣∣ X ∣∣[ n ]) → (P s) is-of-hlevel n)
+           → ((x : X) → P (∣ x ∣[ n ]))
+           → (s : ∣∣ X ∣∣[ n ]) → P s
+  ∣∣∣∣-ind-comp : {X : 𝓤 ̇ } {n : ℕ} {P : ∣∣ X ∣∣[ n ] → 𝓥 ̇ }
+                → (m : (s : ∣∣ X ∣∣[ n ]) → (P s) is-of-hlevel n)
+                → (g : (x : X) → P (∣ x ∣[ n ]))
+                → (x : X) → ∣∣∣∣-ind m g (∣ x ∣[ n ]) ＝ g x
+ infix 0 ∣∣_∣∣[_]
+ infix 0 ∣_∣[_]
+
+\end{code}
+
+We add truncation recursion.
+
+\begin{code}
+
+module GeneralTruncations
+        (te : H-level-truncations-exist)
+        (ua : Univalence)
+       where
+
+ open H-level-truncations-exist te
+
+ ∣∣∣∣-rec : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+          → Y is-of-hlevel n → (X → Y) → ∣∣ X ∣∣[ n ] → Y
+ ∣∣∣∣-rec {𝓤} {𝓥} {X} {Y} {n} Y-h-level f s = ∣∣∣∣-ind (λ - → Y-h-level) f s
+
+ ∣∣∣∣-rec-comp : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+               → (m : Y is-of-hlevel n)
+               → (g : X → Y)
+               → (x : X) → ∣∣∣∣-rec m g ∣ x ∣[ n ] ＝ g x
+ ∣∣∣∣-rec-comp m g = ∣∣∣∣-ind-comp (λ - → m) g
+
+ ∣∣∣∣-rec-double : {𝓤 𝓥 𝓦 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {n : ℕ}
+                 → Z is-of-hlevel n
+                 → (X → Y → Z)
+                 → ∣∣ X ∣∣[ n ] → ∣∣ Y ∣∣[ n ] → Z
+ ∣∣∣∣-rec-double {𝓤} {𝓥} {𝓦} {X} {Y} {Z} {n} Z-h-level g =
+  ∣∣∣∣-rec (hlevel-closed-under-→ n (∣∣ Y ∣∣[ n ]) Z Z-h-level)
+           (λ x → ∣∣∣∣-rec Z-h-level (λ y → g x y))
+
+ ∣∣∣∣-rec-double-comp : {𝓤 𝓥 𝓦 : Universe}
+                        {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {n : ℕ}
+                      → (m : Z is-of-hlevel n)
+                      → (g : X → Y → Z)
+                      → (x : X) → (y : Y)
+                      → ∣∣∣∣-rec-double m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝ g x y
+ ∣∣∣∣-rec-double-comp {𝓤} {𝓥} {𝓦} {X} {Y} {Z} {n} m g x y =
+  ∣∣∣∣-rec-double m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝⟨ happly
+                                              (∣∣∣∣-rec-comp
+                                              (hlevel-closed-under-→ n
+                                                (∣∣ Y ∣∣[ n ]) Z m)
+                                              (λ x → ∣∣∣∣-rec m (λ y → g x y)) x)
+                                              ∣ y ∣[ n ]  ⟩
+  ∣∣∣∣-rec m (λ y → g x y) ∣ y ∣[ n ]       ＝⟨ ∣∣∣∣-rec-comp m (λ y → g x y) y ⟩
+  g x y                                     ∎
+
+ ∣∣∣∣-ind-double : {𝓤 𝓥 𝓦 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+                   {P : ∣∣ X ∣∣[ n ] → ∣∣ Y ∣∣[ n ] → 𝓦 ̇ } 
+                 → ((u : ∣∣ X ∣∣[ n ]) → (v : ∣∣ Y ∣∣[ n ])
+                    → (P u v) is-of-hlevel n)
+                 → ((x : X) → (y : Y) → P (∣ x ∣[ n ]) (∣ y ∣[ n ]))
+                 → (u : ∣∣ X ∣∣[ n ]) → (v : ∣∣ Y ∣∣[ n ]) → P u v
+ ∣∣∣∣-ind-double {𝓤} {𝓥} {𝓦} {X} {Y} {n} {P} P-h-level f =
+  ∣∣∣∣-ind (λ u → hlevel-closed-under-Π n ∣∣ Y ∣∣[ n ] (P u)
+                                        (λ v → P-h-level u v))
+           (λ x → ∣∣∣∣-ind (λ v → P-h-level ∣ x ∣[ n ] v) (λ y → f x y))
+
+ ∣∣∣∣-ind-double-comp : {𝓤 𝓥 𝓦 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+                        {P : ∣∣ X ∣∣[ n ] → ∣∣ Y ∣∣[ n ] → 𝓦 ̇ } 
+                      → (m : (u : ∣∣ X ∣∣[ n ]) → (v : ∣∣ Y ∣∣[ n ])
+                       → (P u v) is-of-hlevel n)
+                      → (g : (x : X) → (y : Y) → P (∣ x ∣[ n ]) (∣ y ∣[ n ]))
+                      → (x : X) → (y : Y)
+                      → ∣∣∣∣-ind-double m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝ g x y
+ ∣∣∣∣-ind-double-comp {𝓤} {𝓥} {𝓦} {X} {Y} {n} {P} m g x y =
+  ∣∣∣∣-ind-double m g ∣ x ∣[ n ] ∣ y ∣[ n ] ＝⟨ happly
+                                               (∣∣∣∣-ind-comp
+                                                (λ u → hlevel-closed-under-Π
+                                                 n ∣∣ Y ∣∣[ n ] (P u)
+                                                 (λ v → m u v))
+                                                (λ x' → ∣∣∣∣-ind
+                                                 (λ v → m ∣ x' ∣[ n ] v)
+                                                 (λ y' → g x' y')) x)
+                                               ∣ y ∣[ n ] ⟩
+  ∣∣∣∣-ind (λ v → m ∣ x ∣[ n ] v)
+           (λ y' → g x y') ∣ y ∣[ n ]       ＝⟨ ∣∣∣∣-ind-comp
+                                                (λ v → m ∣ x ∣[ n ] v)
+                                                (λ y' → g x y') y ⟩
+  g x y                                     ∎
+
+\end{code}
+
+We now set out to define a critical eqeuivalence that characterizes the
+truncated identity type.
+
+\begin{code}
+
+ canonical-id-trunc-map : {𝓤 : Universe} {X : 𝓤 ̇} {x y : X} {n : ℕ}
+                        → ∣∣ x ＝ y ∣∣[ n ]
+                        → ∣ x ∣[ succ n ] ＝ ∣ y ∣[ succ n ]
+ canonical-id-trunc-map {𝓤} {X} {x} {y} {n} =
+  ∣∣∣∣-rec (∣∣∣∣-h-level n) (ap (λ x → ∣ x ∣[ (succ n) ]))
+
+ private
+  P' : {𝓤 : Universe} {X : 𝓤 ̇} {n : ℕ}
+    → ∣∣ X ∣∣[ succ n ] → ∣∣ X ∣∣[ succ n ] → ℍ n 𝓤
+  P' {𝓤} {X} {n} =
+   ∣∣∣∣-rec-double (ℍ-is-of-next-hlevel n 𝓤 (ua 𝓤))
+                   (λ x x' → (∣∣ x ＝ x' ∣∣[ n ] , ∣∣∣∣-h-level n))
+
+  P : {𝓤 : Universe} {X : 𝓤 ̇} {n : ℕ}
+    → ∣∣ X ∣∣[ succ n ] → ∣∣ X ∣∣[ succ n ] → 𝓤 ̇
+  P u v = pr₁ (P' u v)
+
+  P-computes : {𝓤 : Universe} {X : 𝓤 ̇} {x y : X} {n : ℕ}
+             → P ∣ x ∣[ succ n ] ∣ y ∣[ succ n ] ＝ ∣∣ x ＝ y ∣∣[ n ]
+  P-computes {𝓤} {X} {x} {y} {n} =
+   ap pr₁ (∣∣∣∣-rec-double-comp (ℍ-is-of-next-hlevel n 𝓤 (ua 𝓤))
+        (λ x x' → (∣∣ x ＝ x' ∣∣[ n ] , ∣∣∣∣-h-level n)) x y)
+
+ gen-trunc-id-type-char : {𝓤 : Universe} {X : 𝓤 ̇} {n : ℕ}
+                        → (u v : ∣∣ X ∣∣[ succ n ])
+                        → P u v ≃ (u ＝ v)
+ gen-trunc-id-type-char {𝓤} {X} {n} u v =
+  (decode u v , qinvs-are-equivs (decode u v) (encode u v , H u v , G u v))
+  where
+   decode : (u v : ∣∣ X ∣∣[ succ n ])
+          → P u v → u ＝ v
+   decode =
+    ∣∣∣∣-ind-double (λ u v → hlevel-closed-under-→ (succ n) (P u v) (u ＝ v)
+                                                   (∣∣∣∣-h-level (succ n)))
+                    (λ x y → transport (λ T →
+                                        T → ∣ x ∣[ succ n ] ＝ ∣ y ∣[ succ n ])
+                                       (P-computes ⁻¹)
+                                       canonical-id-trunc-map)
+   P-refl : (u : ∣∣ X ∣∣[ succ n ]) → P u u
+   P-refl = ∣∣∣∣-ind (λ - → ∣∣∣∣-h-level (succ n))
+                     (λ x → Idtofun (P-computes ⁻¹) ∣ refl ∣[ n ])
+   encode : (u v : ∣∣ X ∣∣[ succ n ])
+          → u ＝ v → P u v
+   encode u v p = transport (λ v' → P u v') p (P-refl u)
+   H : (u v : ∣∣ X ∣∣[ succ n ]) → encode u v ∘ decode u v ∼ id
+   H u v s = ∣∣∣∣-ind-double (λ - - → ∣∣∣∣-h-level (succ n))
+                             (λ x y → ∣∣∣∣-ind-double-comp) u v
+   G : (u v : ∣∣ X ∣∣[ succ n ]) → decode u v ∘ encode u v ∼ id 
+   G u .u refl = ∣∣∣∣-ind-double (λ - - → ∣∣∣∣-h-level (succ n))
+                                 (λ x y → ∣∣∣∣-ind-double-comp) u u
+
+ trunc-id-type-char : {𝓤 : Universe} {X : 𝓤 ̇} {x y : X} {n : ℕ}
+                    → ∣∣ x ＝ y ∣∣[ n ]
+                    ≃ (∣ x ∣[ succ n ] ＝ ∣ y ∣[ succ n ])
+ trunc-id-type-char {𝓤} {X} {x} {y} {n} =
+  ≃-comp (idtoeq ∣∣ x ＝ y ∣∣[ n ]
+                 (P ∣ x ∣[ succ n ] ∣ y ∣[ succ n ])
+                 (P-computes ⁻¹))
+         (gen-trunc-id-type-char ∣ x ∣[ succ n ] ∣ y ∣[ succ n ])
+
+\end{code}
+
+canonical-id-trunc-map ∘ Idtofun P-computes
+
+We now add some code that allows us to identify the 1-truncation and
+propositional truncation:
+  ∣∣ X ∣∣₁ ≃ ∥ X ∥
+
+\begin{code}
+
+module _ (te : H-level-truncations-exist)
+         (pt : propositional-truncations-exist)
+         (ua : Univalence)
+          where
+
+ open H-level-truncations-exist te
+ open GeneralTruncations te ua
+ open propositional-truncations-exist pt
+
+ 1-trunc-is-prop : {X : 𝓤 ̇} → is-prop (∣∣ X ∣∣[ 1 ])
+ 1-trunc-is-prop = is-prop'-implies-is-prop (∣∣∣∣-h-level 1)
+
+ 1-trunc-≃-prop-trunc : {X : 𝓤 ̇}
+                      → (∣∣ X ∣∣[ 1 ]) ≃ ∥ X ∥
+ 1-trunc-≃-prop-trunc {𝓤} {X} =
+  logically-equivalent-props-are-equivalent 1-trunc-is-prop ∥∥-is-prop ϕ ψ
+  where
+   ϕ : ∣∣ X ∣∣[ 1 ] → ∥ X ∥
+   ϕ = ∣∣∣∣-rec (is-prop-implies-is-prop' ∥∥-is-prop) ∣_∣
+   ψ : ∥ X ∥ → ∣∣ X ∣∣[ 1 ]
+   ψ = ∥∥-rec 1-trunc-is-prop (λ x → ∣ x ∣[ 1 ])
 
 \end{code}
 
 We now add the notion of k-connectedness of type and functions with respect to
-H-levels. We will then see that connectedness as defined elsewhere in the
-library is a special case
+H-levels. TODO: Show that connectedness as defined elsewhere in the
+library is a special case of what follows.
 
 \begin{code}
 
-module k-connectedness (te : H-level-truncations-exist) where
+module k-connectedness
+        (te : H-level-truncations-exist)
+        (ua : Univalence)
+       where
 
  open H-level-truncations-exist te
 
  _is_connected : 𝓤 ̇ → ℕ → 𝓤 ̇
- X is k connected = is-contr (∣∣ X ∣∣ k)
+ X is k connected = is-contr (∣∣ X ∣∣[ k ])
 
  map_is_connected : {X : 𝓤 ̇} {Y : 𝓥 ̇} → (f : X → Y) → ℕ → 𝓤 ⊔ 𝓥 ̇
  map f is k connected = (y : codomain f) → (fiber f y) is k connected
 
 \end{code}
+
+We now add some results about connectedness.
+
+\begin{code}
+
+ open propositional-truncations-exist pt
+ open GeneralTruncations te ua
+
+ connected-characterization : {X : 𝓤 ̇} {n : ℕ}
+                            → X is (succ n) connected
+                            ↔ ∥ X ∥ × ((x y : X) → (x ＝ y) is n connected)
+ connected-characterization {𝓤} {X} {zero} = (left-to-right , {!!})
+  where
+   left-to-right : X is 1 connected
+                 → ∥ X ∥ × ((x y : X) → (x ＝ y) is zero connected)
+   left-to-right X-is-conn =
+    (center (equiv-to-singleton' (1-trunc-≃-prop-trunc te pt ua) X-is-conn)
+     , {!!})
+ connected-characterization {𝓤} {X} {succ n} = ({!!} , {!!})
+
+
+ ap-is-less-connected : {X : 𝓤 ̇} {Y : 𝓥 ̇} → (f : X → Y)
+                      → (n : ℕ)
+                      → map f is (succ n) connected
+                      → map (ap f) is n connected
+ ap-is-less-connected = {!!}
+
+\end{code}

source/UF/Size.lagda

@@ -1045,3 +1045,20 @@ module _ (pt : propositional-truncations-exist) where
                  → is-set Y
                  → image f is (𝓤 ⊔ 𝓥) small
 \end{code}
+
+Ian Ray; 27/06/2024:
+
+If X is 𝓥-small then it is locally 𝓥-small.
+
+\begin{code}
+
+open import MLTT.Spartan
+
+small-implies-locally-small : (X : 𝓤 ̇) → (𝓥 : Universe)
+                            → X is 𝓥 small
+                            → X is-locally 𝓥 small
+small-implies-locally-small X 𝓥 (Y , e) x x' =
+ ((⌜ e ⌝⁻¹ x ＝ ⌜ e ⌝⁻¹ x')
+  , ≃-sym (ap ⌜ e ⌝⁻¹ , ap-is-equiv ⌜ e ⌝⁻¹ (⌜⌝⁻¹-is-equiv e)))
+
+\end{code}