Improve proofs for truncation equivalences

src/foundation-core/truncated-maps.lagda.md

@@ -10,10 +10,12 @@ module foundation-core.truncated-maps where
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-fibers-of-maps
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -112,23 +114,37 @@ module _
   where
 
   abstract
-    is-trunc-map-is-trunc-map-ap :
+    is-trunc-map-succ-is-trunc-map-ap :
       ((x y : A) → is-trunc-map k (ap f {x} {y})) → is-trunc-map (succ-𝕋 k) f
-    is-trunc-map-is-trunc-map-ap is-trunc-map-ap-f b (pair x p) (pair x' p') =
+    is-trunc-map-succ-is-trunc-map-ap is-trunc-map-ap-f b (x , p) (x' , p') =
       is-trunc-equiv k
-        ( fiber (ap f) (p ∙ (inv p')))
-        ( equiv-fiber-ap-eq-fiber f (pair x p) (pair x' p'))
-        ( is-trunc-map-ap-f x x' (p ∙ (inv p')))
+        ( fiber (ap f) (p ∙ inv p'))
+        ( equiv-fiber-ap-eq-fiber f (x , p) (x' , p'))
+        ( is-trunc-map-ap-f x x' (p ∙ inv p'))
 
   abstract
-    is-trunc-map-ap-is-trunc-map :
+    is-trunc-map-ap-is-trunc-map-succ :
       is-trunc-map (succ-𝕋 k) f → (x y : A) → is-trunc-map k (ap f {x} {y})
-    is-trunc-map-ap-is-trunc-map is-trunc-map-f x y p =
+    is-trunc-map-ap-is-trunc-map-succ is-trunc-map-f x y p =
       is-trunc-is-equiv' k
-        ( pair x p ＝ pair y refl)
+        ( (x , p) ＝ (y , refl))
         ( eq-fiber-fiber-ap f x y p)
         ( is-equiv-eq-fiber-fiber-ap f x y p)
-        ( is-trunc-map-f (f y) (pair x p) (pair y refl))
+        ( is-trunc-map-f (f y) (x , p) (y , refl))
+```
+
+### The action on identifications of a `k`-truncated map is also `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  abstract
+    is-trunc-map-ap-is-trunc-map :
+      is-trunc-map k f → (x y : A) → is-trunc-map k (ap f {x} {y})
+    is-trunc-map-ap-is-trunc-map H =
+      is-trunc-map-ap-is-trunc-map-succ k f (is-trunc-map-succ-is-trunc-map k H)
 ```
 
 ### The domain of any `k`-truncated map into a `k+1`-truncated type is `k+1`-truncated
@@ -146,7 +162,7 @@ is-trunc-is-trunc-map-into-is-trunc
     ( k)
     ( ap f)
     ( is-trunc-B (f a) (f a'))
-    ( is-trunc-map-ap-is-trunc-map k f is-trunc-map-f a a')
+    ( is-trunc-map-ap-is-trunc-map-succ k f is-trunc-map-f a a')
 ```
 
 ### A family of types is a family of `k`-truncated types if and only of the projection map is `k`-truncated
@@ -274,7 +290,7 @@ abstract
         ( map-compute-fiber-comp g h (g b))
         ( is-equiv-map-compute-fiber-comp g h (g b))
         ( is-trunc-map-htpy k (inv-htpy H) is-trunc-f (g b)))
-      ( pair b refl)
+      ( b , refl)
 ```
 
 ### If a composite `g ∘ h` and its left factor `g` are truncated maps, then its right factor `h` is a truncated map
@@ -305,3 +321,21 @@ module _
       ( is-trunc-map-comp k i g M
         ( is-trunc-map-is-equiv k K))
 ```
+
+### If the domain is contractible and the codomain is `k+1`-truncated then the map is `k`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  is-trunc-map-is-trunc-succ-codomain-is-contr-domain :
+    is-contr A →
+    is-trunc (succ-𝕋 k) B →
+    is-trunc-map k f
+  is-trunc-map-is-trunc-succ-codomain-is-contr-domain c tB u =
+    is-trunc-equiv k
+      ( f (center c) ＝ u)
+      ( left-unit-law-Σ-is-contr c (center c))
+      ( tB (f (center c)) u)
+```

src/foundation/0-connected-types.lagda.md

@@ -1,4 +1,4 @@
-# `0`-Connected types
+# 0-Connected types
 
 ```agda
 module foundation.0-connected-types where
@@ -10,12 +10,17 @@ module foundation.0-connected-types where
 open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.contractible-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equality-coproduct-types
+open import foundation.evaluation-functions
 open import foundation.fiber-inclusions
 open import foundation.functoriality-set-truncation
 open import foundation.images
 open import foundation.inhabited-types
 open import foundation.mere-equality
+open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.set-truncations
 open import foundation.sets
@@ -56,7 +61,13 @@ is-0-connected A = type-Prop (is-0-connected-Prop A)
 
 is-prop-is-0-connected : {l : Level} (A : UU l) → is-prop (is-0-connected A)
 is-prop-is-0-connected A = is-prop-type-Prop (is-0-connected-Prop A)
+```
+
+## Properties
+
+### 0-connected types are inhabited
 
+```agda
 abstract
   is-inhabited-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → is-inhabited A
@@ -65,13 +76,21 @@ abstract
       ( center C)
       ( set-Prop (trunc-Prop A))
       ( unit-trunc-Prop)
+```
+
+### Elements of 0-connected types are all merely equal
 
+```agda
 abstract
   mere-eq-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → all-elements-merely-equal A
   mere-eq-is-0-connected {A = A} H x y =
     apply-effectiveness-unit-trunc-Set (eq-is-contr H)
+```
+
+### A type is 0-connected if it is inhabited and all elements are merely equal
 
+```agda
 abstract
   is-0-connected-mere-eq :
     {l : Level} {A : UU l} (a : A) →
@@ -91,17 +110,22 @@ abstract
     apply-universal-property-trunc-Prop H
       ( is-0-connected-Prop _)
       ( λ a → is-0-connected-mere-eq a (K a))
+```
 
-is-0-connected-is-surjective-point :
-  {l1 : Level} {A : UU l1} (a : A) →
-  is-surjective (point a) → is-0-connected A
-is-0-connected-is-surjective-point a H =
-  is-0-connected-mere-eq a
-    ( λ x →
-      apply-universal-property-trunc-Prop
-        ( H x)
-        ( mere-eq-Prop a x)
-        ( λ u → unit-trunc-Prop (pr2 u)))
+### A type is 0-connected iff any point inclusion is surjective
+
+```agda
+abstract
+  is-0-connected-is-surjective-point :
+    {l1 : Level} {A : UU l1} (a : A) →
+    is-surjective (point a) → is-0-connected A
+  is-0-connected-is-surjective-point a H =
+    is-0-connected-mere-eq a
+      ( λ x →
+        apply-universal-property-trunc-Prop
+          ( H x)
+          ( mere-eq-Prop a x)
+          ( λ u → unit-trunc-Prop (pr2 u)))
 
 abstract
   is-surjective-point-is-0-connected :
@@ -112,21 +136,29 @@ abstract
       ( mere-eq-is-0-connected H a x)
       ( trunc-Prop (fiber (point a) x))
       ( λ where refl → unit-trunc-Prop (star , refl))
+```
+
+### If `A` is 0-connected and `B` is `k+1`-truncated then every evaluation map `(A → B) → B` is `k`-truncated
 
-is-trunc-map-ev-point-is-connected :
+```agda
+is-trunc-map-ev-is-connected :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
   is-0-connected A → is-trunc (succ-𝕋 k) B →
-  is-trunc-map k (ev-point' a {B})
-is-trunc-map-ev-point-is-connected k {A} {B} a H K =
+  is-trunc-map k (ev-function B a)
+is-trunc-map-ev-is-connected k {A} {B} a H K =
   is-trunc-map-comp k
-    ( ev-point' star {B})
+    ( ev-function B star)
     ( precomp (point a) B)
     ( is-trunc-map-is-equiv k
       ( universal-property-contr-is-contr star is-contr-unit B))
     ( is-trunc-map-precomp-Π-is-surjective k
       ( is-surjective-point-is-0-connected a H)
       ( λ _ → (B , K)))
+```
+
+### The dependent universal property of 0-connected types
 
+```agda
 equiv-dependent-universal-property-is-0-connected :
   {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
   ( {l : Level} (P : A → Prop l) →
@@ -143,7 +175,11 @@ apply-dependent-universal-property-is-0-connected :
   {l : Level} (P : A → Prop l) → type-Prop (P a) → (x : A) → type-Prop (P x)
 apply-dependent-universal-property-is-0-connected a H P =
   map-inv-equiv (equiv-dependent-universal-property-is-0-connected a H P)
+```
+
+### A type `A` is 0-connected if and only if every fiber inclusion `B a → Σ A B` is surjective
 
+```agda
 abstract
   is-surjective-fiber-inclusion :
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
@@ -172,7 +208,11 @@ abstract
     is-0-connected A
   is-0-connected-is-surjective-fiber-inclusion a H =
     is-0-connected-mere-eq a (mere-eq-is-surjective-fiber-inclusion a H)
+```
+
+### 0-connected types are closed under equivalences
 
+```agda
 is-0-connected-equiv :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} →
   (A ≃ B) → is-0-connected B → is-0-connected A
@@ -184,7 +224,7 @@ is-0-connected-equiv' :
 is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e)
 ```
 
-### `0`-connected types are closed under cartesian products
+### 0-connected types are closed under cartesian products
 
 ```agda
 module _
@@ -200,7 +240,7 @@ module _
       ( is-contr-product p1 p2)
 ```
 
-### The unit type is `0`-connected
+### The unit type is 0-connected
 
 ```agda
 abstract
@@ -209,7 +249,7 @@ abstract
     is-contr-equiv' unit equiv-unit-trunc-unit-Set is-contr-unit
 ```
 
-### A contractible type is `0`-connected
+### Contractible types are 0-connected
 
 ```agda
 is-0-connected-is-contr :
@@ -219,43 +259,87 @@ is-0-connected-is-contr X p =
   is-contr-equiv X (inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p))) p
 ```
 
-### The image of a function with a `0`-connected domain is `0`-connected
+### The image of a function with a 0-connected domain is 0-connected
 
 ```agda
-abstract
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where abstract
+
+  is-contr-im-map-trunc-Set-is-0-connected-domain' :
+    A → all-elements-merely-equal A → is-contr (im (map-trunc-Set f))
+  is-contr-im-map-trunc-Set-is-0-connected-domain' a C =
+    is-contr-im
+      ( trunc-Set B)
+      ( unit-trunc-Set a)
+      ( apply-dependent-universal-property-trunc-Set'
+        ( λ x →
+          set-Prop
+            ( Id-Prop
+              ( trunc-Set B)
+              ( map-trunc-Set f x)
+              ( map-trunc-Set f (unit-trunc-Set a))))
+        ( λ a' →
+          apply-universal-property-trunc-Prop
+            ( C a' a)
+            ( Id-Prop
+              ( trunc-Set B)
+              ( map-trunc-Set f (unit-trunc-Set a'))
+              ( map-trunc-Set f (unit-trunc-Set a)))
+            ( λ where refl → refl)))
+
+  is-0-connected-im-is-0-connected-domain' :
+    A → all-elements-merely-equal A → is-0-connected (im f)
+  is-0-connected-im-is-0-connected-domain' a C =
+    is-contr-equiv'
+      ( im (map-trunc-Set f))
+      ( equiv-trunc-im-Set f)
+      ( is-contr-im-map-trunc-Set-is-0-connected-domain' a C)
+
   is-0-connected-im-is-0-connected-domain :
-    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
     is-0-connected A → is-0-connected (im f)
-  is-0-connected-im-is-0-connected-domain {A = A} {B} f C =
+  is-0-connected-im-is-0-connected-domain C =
     apply-universal-property-trunc-Prop
       ( is-inhabited-is-0-connected C)
       ( is-contr-Prop _)
       ( λ a →
-        is-contr-equiv'
-          ( im (map-trunc-Set f))
-          ( equiv-trunc-im-Set f)
-          ( is-contr-im
-            ( trunc-Set B)
-            ( unit-trunc-Set a)
-            ( apply-dependent-universal-property-trunc-Set'
-              ( λ x →
-                set-Prop
-                  ( Id-Prop
-                    ( trunc-Set B)
-                    ( map-trunc-Set f x)
-                    ( map-trunc-Set f (unit-trunc-Set a))))
-              ( λ a' →
-                apply-universal-property-trunc-Prop
-                  ( mere-eq-is-0-connected C a' a)
-                  ( Id-Prop
-                    ( trunc-Set B)
-                    ( map-trunc-Set f (unit-trunc-Set a'))
-                    ( map-trunc-Set f (unit-trunc-Set a)))
-                  ( λ where refl → refl)))))
+        is-0-connected-im-is-0-connected-domain' a (mere-eq-is-0-connected C))
+```
 
-abstract
-  is-0-connected-im-point' :
-    {l1 : Level} {A : UU l1} (f : unit → A) → is-0-connected (im f)
+### The image of a point is 0-connected
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where abstract
+
+  is-0-connected-im-point' : (f : unit → A) → is-0-connected (im f)
   is-0-connected-im-point' f =
     is-0-connected-im-is-0-connected-domain f is-0-connected-unit
+
+  is-0-connected-im-point : (a : A) → is-0-connected (im (point a))
+  is-0-connected-im-point a = is-0-connected-im-point' (point a)
+```
+
+### Coproducts of inhabited types are not 0-connected
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where abstract
+
+  is-not-0-connected-coproduct-has-element :
+    A → B → ¬ is-0-connected (A + B)
+  is-not-0-connected-coproduct-has-element a b H =
+    apply-universal-property-trunc-Prop
+      ( mere-eq-is-0-connected H (inl a) (inr b))
+      ( empty-Prop)
+      ( is-empty-eq-coproduct-inl-inr a b)
+
+  is-not-0-connected-coproduct-is-inhabited :
+    is-inhabited A → is-inhabited B → ¬ is-0-connected (A + B)
+  is-not-0-connected-coproduct-is-inhabited |a| |b| =
+    apply-twice-universal-property-trunc-Prop |a| |b|
+      ( neg-type-Prop (is-0-connected (A + B)))
+      ( is-not-0-connected-coproduct-has-element)
 ```