Formalizing Christensen's result on small types and truncations

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
@@ -33,9 +34,15 @@ open import UF.Subsingletons-FunExt
 open import UF.Subsingletons-Properties
 open import UF.Univalence
 open import UF.UA-FunExt
+open import Naturals.Addition renaming (_+_ to _+'_)
 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
+
+open import UF.ImageAndSurjection pt
 
 _is-of-hlevel_ : 𝓤 ̇ → ℕ → 𝓤 ̇
 X is-of-hlevel zero = is-contr X
@@ -48,27 +55,39 @@ hlevel-relation-is-prop {𝓤} (succ n) X =
   Π₂-is-prop fe'
              (λ x x' → hlevel-relation-is-prop n (x ＝ x'))
 
+map_is-of-hlevel_ : {X : 𝓤 ̇} {Y : 𝓥 ̇} → (f : X → Y) → ℕ → 𝓤 ⊔ 𝓥 ̇
+map f is-of-hlevel n = (y : codomain f) → (fiber f y) is-of-hlevel n
+
 \end{code}
 
 H-Levels are cumulative.
 
+TODO: Move the following contractibility lemma to a more apropriate location.
+
 \begin{code}
 
+contr-lemma : {X : 𝓤 ̇} → is-contr X → (x x' : X) → is-contr (x ＝ x')
+contr-lemma (c , C) x x' = (((C x)⁻¹ ∙ C x') , D)
+ where
+  D : is-central (x ＝ x') (C x ⁻¹ ∙ C x')
+  D refl = left-inverse (C x)
+
 hlevels-are-upper-closed : (n : ℕ) (X : 𝓤 ̇)
                          → (X is-of-hlevel n)
                          → (X is-of-hlevel succ n)
-hlevels-are-upper-closed zero X h-level = base h-level
- where
-  base : is-contr X → (x x' : X) → is-contr (x ＝ x')
-  base (c , C) x x' = (((C x)⁻¹ ∙ C x') , D)
-   where
-    D : is-central (x ＝ x') (C x ⁻¹ ∙ C x')
-    D refl = left-inverse (C x)
+hlevels-are-upper-closed zero X h-level = contr-lemma h-level
 hlevels-are-upper-closed (succ n) X h-level = step
  where
   step : (x x' : X) (p q : x ＝ x') → (p ＝ q) is-of-hlevel n
   step x x' p q = hlevels-are-upper-closed n (x ＝ x') (h-level x x') p q
 
+id-types-are-same-hlevel : {X : 𝓤 ̇ } (n : ℕ)
+                         → X is-of-hlevel n
+                         → (x x' : X) → (x ＝ x') is-of-hlevel n
+id-types-are-same-hlevel zero X-hlev x x' = contr-lemma X-hlev x x'
+id-types-are-same-hlevel (succ n) X-hlev x x' =
+  hlevels-are-upper-closed n (x ＝ x') (X-hlev x x')
+
 \end{code}
 
 We will now give some closure results about H-levels.
@@ -237,34 +256,252 @@ From Univalence we can show that (ℍ n) is of level (n + 1), for all n : ℕ.
 
 We now define the notion of a k-truncation using record types.
 
+TODO: Show 1 truncation and propositional truncation are equivalent.
+
 \begin{code}
 
 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} → 𝓤 ̇ → ℕ → 𝓤 ̇
+  ∣∣∣∣-is-hlevel : {𝓤 : Universe} {X : 𝓤 ̇ } {n : ℕ}
+                 → (∣∣ X ∣∣⌞ n ⌟) is-of-hlevel n
+  ∣_∣⌞_⌟ :  {𝓤 : Universe} {X : 𝓤 ̇ } → X → (n : ℕ) → ∣∣ X ∣∣⌞ n ⌟ 
+  ∣∣∣∣-induction : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {n : ℕ}
+                 → (P : ∣∣ X ∣∣⌞ n ⌟ → 𝓥 ̇ )
+                 → ((s : ∣∣ X ∣∣⌞ n ⌟) → (P s) is-of-hlevel n)
+                 → ((x : X) → P (∣ x ∣⌞ n ⌟))
+                 → (s : ∣∣ X ∣∣⌞ n ⌟) → P s
+  ∣∣∣∣-comp-ind : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {n : ℕ}
+                → (P : ∣∣ X ∣∣⌞ n ⌟ → 𝓥 ̇ )
+                → (h-lev : (s : ∣∣ X ∣∣⌞ n ⌟) → (P s) is-of-hlevel n)
+                → (f : (x : X) → P (∣ x ∣⌞ n ⌟))
+                → (x : X)
+                → ∣∣∣∣-induction P h-lev f (∣ x ∣⌞ n ⌟) ＝ f x
+ infix 0 ∣∣_∣∣⌞_⌟
+ infix 0 ∣_∣⌞_⌟
+
+module truncation-properties (te : H-level-truncations-exist) 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} H-lev f s =
+   ∣∣∣∣-induction (λ _ → Y) (λ _ → H-lev) f s
+
+ ∣∣∣∣-uniqueness : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+                 → Y is-of-hlevel n
+                 → (f g : ∣∣ X ∣∣⌞ n ⌟ → Y)
+                 → ((x : X) → f (∣ x ∣⌞ n ⌟) ＝ g (∣ x ∣⌞ n ⌟))
+                 → (s : ∣∣ X ∣∣⌞ n ⌟) → f s ＝ g s
+ ∣∣∣∣-uniqueness {𝓤} {𝓥} {X} {Y} {n} Y-h-lev f g H =
+   ∣∣∣∣-induction (λ s → f s ＝ g s)
+                  (λ s → id-types-are-same-hlevel n Y-h-lev (f s) (g s)) H
+
+ ∣∣∣∣-comp-rec : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {n : ℕ}
+               → (Y-h-lev : Y is-of-hlevel n)
+               → (f : (X → Y))
+               → (x : X)
+               → ∣∣∣∣-rec Y-h-lev f (∣ x ∣⌞ n ⌟) ＝ f x
+ ∣∣∣∣-comp-rec {𝓤} {𝓥} {X} {Y} {n} Y-h-lev f x =
+   ∣∣∣∣-comp-ind (λ _ → Y) (λ _ → Y-h-lev) f x 
+
+ zero-hlevel-is-contr : {X : 𝓤 ̇ } → is-contr (∣∣ X ∣∣⌞ zero ⌟)
+ zero-hlevel-is-contr = ∣∣∣∣-is-hlevel
+
+ one-hlevel-is-prop : {X : 𝓤 ̇ } → is-prop (∣∣ X ∣∣⌞ succ zero ⌟)
+ one-hlevel-is-prop = is-prop'-implies-is-prop ∣∣∣∣-is-hlevel
+
+ two-hlevel-is-set : {X : 𝓤 ̇ } → is-set (∣∣ X ∣∣⌞ succ (succ zero) ⌟)
+ two-hlevel-is-set {𝓤} {X} {x} {y} =
+   is-prop'-implies-is-prop (∣∣∣∣-is-hlevel x y)
+
+ canonical-pred-map : {X : 𝓤 ̇} {n : ℕ}
+                    → ∣∣ X ∣∣⌞ succ n ⌟ → ∣∣ X ∣∣⌞ n ⌟
+ canonical-pred-map {𝓤} {X} {n} x =
+        ∣∣∣∣-rec (hlevels-are-upper-closed n (∣∣ X ∣∣⌞ n ⌟) ∣∣∣∣-is-hlevel)
+                 (λ x → ∣ x ∣⌞ n ⌟) x
+
+ canonical-pred-map-comp : {X : 𝓤 ̇} {n : ℕ} (x : X)
+                         → canonical-pred-map (∣ x ∣⌞ succ n ⌟) ＝ (∣ x ∣⌞ n ⌟)
+ canonical-pred-map-comp {𝓤} {X} {n} x =
+   ∣∣∣∣-comp-rec (hlevels-are-upper-closed n (∣∣ X ∣∣⌞ n ⌟) ∣∣∣∣-is-hlevel)
+                 (λ _ → ∣ _ ∣⌞ n ⌟) x
+
+ truncation-closed-under-equiv : {𝓤 𝓥 : Universe}
+                               → (n : ℕ)
+                               → (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
+                               → X ≃ Y
+                               → (∣∣ X ∣∣⌞ n ⌟) ≃ (∣∣ Y ∣∣⌞ n ⌟)
+ truncation-closed-under-equiv n X Y e = (f , (b , G) , (b , H))
+  where
+   f : ∣∣ X ∣∣⌞ n ⌟ → ∣∣ Y ∣∣⌞ n ⌟
+   f = ∣∣∣∣-rec ∣∣∣∣-is-hlevel (λ x → ∣ (⌜ e ⌝ x) ∣⌞ n ⌟)
+   b : ∣∣ Y ∣∣⌞ n ⌟ → ∣∣ X ∣∣⌞ n ⌟
+   b = ∣∣∣∣-rec ∣∣∣∣-is-hlevel (λ y → ∣ (⌜ e ⌝⁻¹ y) ∣⌞ n ⌟)
+   H : b ∘ f ∼ id
+   H = ∣∣∣∣-induction (λ s → b (f s) ＝ s)
+                      (λ s → id-types-are-same-hlevel n ∣∣∣∣-is-hlevel
+                                                      (b (f s)) s)
+                      H'
+    where
+     H' : (x : X) → b (f (∣ x ∣⌞ n ⌟)) ＝ (∣ x ∣⌞ n ⌟)
+     H' x = b (f (∣ x ∣⌞ n ⌟))         ＝⟨ ap b (∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                                (λ x → ∣ (⌜ e ⌝ x) ∣⌞ n ⌟) x) ⟩
+            b (∣ ⌜ e ⌝ x ∣⌞ n ⌟)       ＝⟨ ∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                                (λ y → ∣ (⌜ e ⌝⁻¹ y) ∣⌞ n ⌟)
+                                                (⌜ e ⌝ x) ⟩
+            (∣ ⌜ e ⌝⁻¹ (⌜ e ⌝ x) ∣⌞ n ⌟) ＝⟨ ap (λ x → ∣ x ∣⌞ n ⌟)
+                                             (inverses-are-retractions' e x) ⟩
+            (∣ x ∣⌞ n ⌟)                ∎ 
+   G : f ∘ b ∼ id
+   G = ∣∣∣∣-induction (λ s → f (b s) ＝ s)
+                      (λ s → id-types-are-same-hlevel n ∣∣∣∣-is-hlevel
+                                                      (f (b s)) s)
+                      G'
+    where
+     G' : (y : Y) → f (b (∣ y ∣⌞ n ⌟)) ＝ (∣ y ∣⌞ n ⌟)
+     G' y = f (b (∣ y ∣⌞ n ⌟))         ＝⟨ ap f (∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                               (λ y → ∣ (⌜ e ⌝⁻¹ y) ∣⌞ n ⌟) y) ⟩
+            f (∣ (⌜ e ⌝⁻¹ y) ∣⌞ n ⌟)   ＝⟨ ∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                          (λ x → ∣ ⌜ e ⌝ x ∣⌞ n ⌟) (⌜ e ⌝⁻¹ y) ⟩
+            (∣ ⌜ e ⌝ (⌜ e ⌝⁻¹ y) ∣⌞ n ⌟) ＝⟨ ap (λ y → ∣ y ∣⌞ n ⌟)
+                                                (inverses-are-sections' e y) ⟩
+            (∣ y ∣⌞ n ⌟)               ∎ 
+
+ succesive-truncations-equiv : (X : 𝓤 ̇) (n : ℕ)
+                             → (∣∣ X ∣∣⌞ n ⌟) ≃ (∣∣ (∣∣ X ∣∣⌞ succ n ⌟) ∣∣⌞ n ⌟)
+ succesive-truncations-equiv X n = (f , (b , G) , (b , H))
+  where
+   f : (∣∣ X ∣∣⌞ n ⌟) → (∣∣ (∣∣ X ∣∣⌞ succ n ⌟) ∣∣⌞ n ⌟)
+   f = ∣∣∣∣-rec ∣∣∣∣-is-hlevel (λ x → ∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟)
+   b : (∣∣ (∣∣ X ∣∣⌞ succ n ⌟) ∣∣⌞ n ⌟) → (∣∣ X ∣∣⌞ n ⌟)
+   b = ∣∣∣∣-rec ∣∣∣∣-is-hlevel (canonical-pred-map)
+   G : f ∘ b ∼ id
+   G = ∣∣∣∣-induction (λ s → f ( b s) ＝ s)
+                      (λ s → id-types-are-same-hlevel n ∣∣∣∣-is-hlevel
+                                                      (f (b s)) s)
+                      (∣∣∣∣-induction (λ t → f (b (∣ t ∣⌞ n ⌟)) ＝ (∣ t ∣⌞ n ⌟))
+                                      (λ t → id-types-are-same-hlevel n
+                                             (id-types-are-same-hlevel n
+                                             ∣∣∣∣-is-hlevel (f (b (∣ t ∣⌞ n ⌟)))
+                                                               ((∣ t ∣⌞ n ⌟))))
+                                      G')
+    where
+     G' : (x : X)
+        → f (b (∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟)) ＝ (∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟)
+     G' x = f (b (∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟))     ＝⟨ ap f (∣∣∣∣-comp-rec
+                                                         ∣∣∣∣-is-hlevel
+                                                         canonical-pred-map
+                                                         (∣ x ∣⌞ succ n ⌟)) ⟩
+            f (canonical-pred-map (∣ x ∣⌞ succ n ⌟)) ＝⟨ ap f
+                                                   (canonical-pred-map-comp x) ⟩
+            f (∣ x ∣⌞ n ⌟)             ＝⟨ ∣∣∣∣-comp-rec
+                                           ∣∣∣∣-is-hlevel
+                                           (λ x → ∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟)
+                                            x ⟩
+            (∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟)   ∎
+   H : b ∘ f ∼ id
+   H = ∣∣∣∣-induction (λ s → b (f s) ＝ s)
+                      (λ s → id-types-are-same-hlevel n ∣∣∣∣-is-hlevel
+                                                      (b (f s)) s)
+                      H'
+    where
+     H' : (x : X) → b (f (∣ x ∣⌞ n ⌟)) ＝ (∣ x ∣⌞ n ⌟)
+     H' x = b (f (∣ x ∣⌞ n ⌟))       ＝⟨ ap b (∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                           (λ x → ∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟) x) ⟩
+            b (∣ ∣ x ∣⌞ succ n ⌟ ∣⌞ n ⌟) ＝⟨ ∣∣∣∣-comp-rec ∣∣∣∣-is-hlevel
+                                          canonical-pred-map (∣ x ∣⌞ succ n ⌟) ⟩
+            canonical-pred-map (∣ x ∣⌞ succ n ⌟) ＝⟨ canonical-pred-map-comp x ⟩
+            (∣ x ∣⌞ n ⌟)                    ∎
+
 
 \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
+We now define the notion of k-connectedness for types and functions with respect
+to H-levels. We will then see that connectedness as defined elsewhere is a
+special case:
+Connectedness typically means set connectedness. In terms of H-levels defined
+here it will mean 2-connectedness.
 
 \begin{code}
 
 module k-connectedness (te : H-level-truncations-exist) where
 
  open H-level-truncations-exist te
+ open truncation-properties 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
 
+ open PropositionalTruncation pt
+
+ 1-connected-map-is-surj : {X : 𝓤 ̇} {Y : 𝓥 ̇} {f : X → Y}
+                         → map f is 1 connected
+                         → is-surjection f
+ 1-connected-map-is-surj {𝓤} {𝓥} {X} {Y} {f} f-1-con y =
+   g y (center (f-1-con y))
+  where
+   g : (y : Y) → ∣∣ fiber f y ∣∣⌞ 1 ⌟ → y ∈image f
+   g y = ∣∣∣∣-rec (is-prop-implies-is-prop' ∃-is-prop) λ (x , e) → ∣ (x , e) ∣
+
+ connectedness-closed-under-equiv : {𝓤 𝓥 : Universe}
+                                  → (k : ℕ)
+                                  → (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
+                                  → X ≃ Y
+                                  → Y is k connected
+                                  → X is k connected
+ connectedness-closed-under-equiv k X Y e Y-con =
+   equiv-to-singleton (truncation-closed-under-equiv k X Y e) Y-con
+
+ contractible-types-are-connected : {𝓤 : Universe}
+                                  → (X : 𝓤 ̇ )
+                                  → is-contr X
+                                  → (n : ℕ)
+                                  → X is n connected
+ contractible-types-are-connected X (c , C) n = ((∣ c ∣⌞ n ⌟) , C')
+  where
+   C' : (s : ∣∣ X ∣∣⌞ n ⌟) → (∣ c ∣⌞ n ⌟) ＝ s
+   C' = ∣∣∣∣-induction (λ s → (∣ c ∣⌞ n ⌟) ＝ s)
+                       (id-types-are-same-hlevel n ∣∣∣∣-is-hlevel (∣ c ∣⌞ n ⌟))
+                       (λ x → ap (λ x → ∣ x ∣⌞ n ⌟) (C x))
+
+ connectedness-is-lower-closed : {X : 𝓤 ̇} {k : ℕ}
+                               → X is (succ k) connected
+                               → X is k connected
+ connectedness-is-lower-closed {𝓤} {X} {k} X-succ-con =
+   equiv-to-singleton (succesive-truncations-equiv X k)
+                      (contractible-types-are-connected (∣∣ X ∣∣⌞ succ k ⌟)
+                                                        X-succ-con k)
+
+ connectedness-extends-to-zero : {X : 𝓤 ̇} (k : ℕ)
+                               → X is k connected
+                               → X is zero connected
+ connectedness-extends-to-zero zero X-con = X-con
+ connectedness-extends-to-zero (succ k) X-con =
+   connectedness-extends-to-zero k (connectedness-is-lower-closed X-con)
+
+ connectedness-step-down : {X : 𝓤 ̇} (k l : ℕ)
+                         → X is (l +' k) connected
+                         → X is l connected
+ connectedness-step-down zero l X-con = X-con
+ connectedness-step-down (succ k) l X-con =
+   connectedness-step-down k l (connectedness-is-lower-closed X-con)
+
+ connectedness-extends-below : {X : 𝓤 ̇} (k l : ℕ)
+                             → (l ≤ℕ k)
+                             → X is k connected
+                             → X is l connected
+ connectedness-extends-below {𝓤} {X} k l o X-con =
+   connectedness-step-down m l (transport (λ z → X is z connected) p X-con)
+  where
+   m : ℕ
+   m = pr₁ (subtraction l k o)
+   p = k        ＝⟨ pr₂ (subtraction l k o) ⁻¹ ⟩
+       m +' l   ＝⟨ addition-commutativity m l ⟩
+       l +' m   ∎
+
 \end{code}