Renamings and rewordings OFS

src/foundation-core/contractible-types.lagda.md

@@ -133,6 +133,24 @@ module _
     is-equiv-is-contr _ is-contr-A is-contr-B
 ```
 
+### Contractibility of the base of a contractible dependent sum
+
+Given a type `A` and a type family over it `B`, then if the dependent sum
+`Σ A B` is contractible, it follows that if there is a section `(x : A) → B x`
+then `A` is contractible.
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2)
+  where
+
+  abstract
+    is-contr-base-is-contr-Σ' :
+      ((x : A) → B x) → is-contr (Σ A B) → is-contr A
+    is-contr-base-is-contr-Σ' s =
+      is-contr-retract-of (Σ A B) ((λ a → a , s a) , pr1 , refl-htpy)
+```
+
 ### Contractibility of cartesian product types
 
 Given two types `A` and `B`, the following are equivalent:

src/foundation-core/functoriality-dependent-pair-types.lagda.md

@@ -7,7 +7,10 @@ module foundation-core.functoriality-dependent-pair-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -21,7 +24,7 @@ open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.retractions
 open import foundation-core.retracts-of-types
-open import foundation-core.transport-along-identifications
+open import foundation-core.sections
 ```
 
 </details>
@@ -305,6 +308,78 @@ module _
     is-equiv-fiber-map-Σ-map-base-fiber t
 ```
 
+### The fibers of `map-Σ`
+
+We compute the fibers of `map-Σ` first in terms of `fiber'` and then in terms of
+`fiber`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4)
+  (f : A → B) (g : (x : A) → C x → D (f x)) (t : Σ B D)
+  where
+
+  fiber-map-Σ' : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  fiber-map-Σ' =
+    Σ (fiber' f (pr1 t)) (λ s → fiber' (g (pr1 s)) (tr D (pr2 s) (pr2 t)))
+
+  map-fiber-map-Σ' : fiber' (map-Σ D f g) t → fiber-map-Σ'
+  map-fiber-map-Σ' ((a , c) , refl) = (a , refl) , (c , refl)
+
+  map-inv-fiber-map-Σ' : fiber-map-Σ' → fiber' (map-Σ D f g) t
+  map-inv-fiber-map-Σ' ((a , p) , (c , q)) = ((a , c) , eq-pair-Σ p q)
+
+  abstract
+    is-section-map-inv-fiber-map-Σ' :
+      is-section map-fiber-map-Σ' map-inv-fiber-map-Σ'
+    is-section-map-inv-fiber-map-Σ' ((a , refl) , (c , refl)) = refl
+
+  abstract
+    is-retraction-map-inv-fiber-map-Σ' :
+      is-retraction map-fiber-map-Σ' map-inv-fiber-map-Σ'
+    is-retraction-map-inv-fiber-map-Σ' ((a , c) , refl) = refl
+
+  is-equiv-map-fiber-map-Σ' : is-equiv map-fiber-map-Σ'
+  is-equiv-map-fiber-map-Σ' =
+    is-equiv-is-invertible
+      map-inv-fiber-map-Σ'
+      is-section-map-inv-fiber-map-Σ'
+      is-retraction-map-inv-fiber-map-Σ'
+
+  compute-fiber-map-Σ' : fiber' (map-Σ D f g) t ≃ fiber-map-Σ'
+  compute-fiber-map-Σ' = (map-fiber-map-Σ' , is-equiv-map-fiber-map-Σ')
+
+  fiber-map-Σ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  fiber-map-Σ =
+    Σ (fiber f (pr1 t)) (λ s → fiber (g (pr1 s)) (inv-tr D (pr2 s) (pr2 t)))
+
+  map-fiber-map-Σ : fiber (map-Σ D f g) t → fiber-map-Σ
+  map-fiber-map-Σ ((a , c) , refl) = (a , refl) , (c , refl)
+
+  map-inv-fiber-map-Σ : fiber-map-Σ → fiber (map-Σ D f g) t
+  map-inv-fiber-map-Σ ((a , refl) , c , refl) = ((a , c) , refl)
+
+  abstract
+    is-section-map-inv-fiber-map-Σ :
+      is-section map-fiber-map-Σ map-inv-fiber-map-Σ
+    is-section-map-inv-fiber-map-Σ ((a , refl) , (c , refl)) = refl
+
+  abstract
+    is-retraction-map-inv-fiber-map-Σ :
+      is-retraction map-fiber-map-Σ map-inv-fiber-map-Σ
+    is-retraction-map-inv-fiber-map-Σ ((a , c) , refl) = refl
+
+  is-equiv-map-fiber-map-Σ : is-equiv map-fiber-map-Σ
+  is-equiv-map-fiber-map-Σ =
+    is-equiv-is-invertible
+      map-inv-fiber-map-Σ
+      is-section-map-inv-fiber-map-Σ
+      is-retraction-map-inv-fiber-map-Σ
+
+  compute-fiber-map-Σ : fiber (map-Σ D f g) t ≃ fiber-map-Σ
+  compute-fiber-map-Σ = (map-fiber-map-Σ , is-equiv-map-fiber-map-Σ)
+```
+
 ### If `f : A → B` is a contractible map, then so is `map-Σ-map-base f C`
 
 ```agda
@@ -455,10 +530,27 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
   where
 
-  compute-map-Σ-id : map-Σ B id (λ x → id) ~ id
+  compute-map-Σ-id : map-Σ B id (λ _ → id) ~ id
   compute-map-Σ-id = refl-htpy
 ```
 
+### `map-Σ` preserves composition of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  {A' : A → UU l4} {B' : B → UU l5} {C' : C → UU l6}
+  {f : A → B} {f' : (x : A) → A' x → B' (f x)}
+  {g : B → C} {g' : (y : B) → B' y → C' (g y)}
+  where
+
+  preserves-comp-map-Σ :
+    map-Σ C' (g ∘ f) (λ x x' → g' (f x) (f' x x')) ~
+    map-Σ C' g g' ∘ map-Σ B' f f'
+  preserves-comp-map-Σ = refl-htpy
+```
+
 ## See also
 
 - Arithmetical laws involving dependent pair types are recorded in

src/foundation-core/propositions.lagda.md

@@ -183,6 +183,25 @@ pr2 (Σ-Prop P Q) =
     ( λ p → is-prop-type-Prop (Q p))
 ```
 
+### If `Σ A B` is a proposition and there is a section `(x : A) → B x` then `A` is a proposition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (s : (x : A) → B x)
+  where
+
+  is-proof-irrelevant-base-is-proof-irrelevant-Σ' :
+    is-proof-irrelevant (Σ A B) → is-proof-irrelevant A
+  is-proof-irrelevant-base-is-proof-irrelevant-Σ' H a =
+    is-contr-base-is-contr-Σ' A B s (H (a , s a))
+
+  is-prop-base-is-prop-Σ' : is-prop (Σ A B) → is-prop A
+  is-prop-base-is-prop-Σ' H =
+    is-prop-is-proof-irrelevant
+      ( is-proof-irrelevant-base-is-proof-irrelevant-Σ'
+          ( is-proof-irrelevant-is-prop H))
+```
+
 ### Propositions are closed under cartesian product types
 
 ```agda

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

@@ -7,6 +7,7 @@ module foundation-core.truncated-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
@@ -217,6 +218,24 @@ fiber-Truncated-Type A B f b =
   Σ-Truncated-Type A (λ a → Id-Truncated-Type' B (f a) b)
 ```
 
+### Truncatedness of the base of a truncated dependent sum
+
+```agda
+abstract
+  is-trunc-base-is-trunc-Σ' :
+    {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : A → UU l2} →
+    ((x : A) → B x) → is-trunc k (Σ A B) → is-trunc k A
+  is-trunc-base-is-trunc-Σ' {k = neg-two-𝕋} {A} {B} =
+    is-contr-base-is-contr-Σ' A B
+  is-trunc-base-is-trunc-Σ' {k = succ-𝕋 k} s is-trunc-ΣAB x y =
+    is-trunc-base-is-trunc-Σ'
+      ( apd s)
+      ( is-trunc-equiv' k
+        ( (x , s x) ＝ (y , s y))
+        ( equiv-pair-eq-Σ (x , s x) (y , s y))
+        ( is-trunc-ΣAB (x , s x) (y , s y)))
+```
+
 ### Products of truncated types are truncated
 
 ```agda

src/foundation.lagda.md

@@ -342,7 +342,7 @@ open import foundation.retracts-of-maps public
 open import foundation.retracts-of-types public
 open import foundation.russells-paradox public
 open import foundation.sections public
-open import foundation.separated-types public
+open import foundation.separated-types-subuniverses public
 open import foundation.sequences public
 open import foundation.sequential-limits public
 open import foundation.set-presented-types public

src/foundation/contractible-types.lagda.md

@@ -157,11 +157,9 @@ module _
 
   is-contr-Σ-is-prop :
     ((x : A) → is-prop (B x)) → ((x : A) → B x → a ＝ x) → is-contr (Σ A B)
-  pr1 (is-contr-Σ-is-prop p f) = pair a b
-  pr2 (is-contr-Σ-is-prop p f) (pair x y) =
-    eq-type-subtype
-      ( λ x' → pair (B x') (p x'))
-      ( f x y)
+  pr1 (is-contr-Σ-is-prop p f) = a , b
+  pr2 (is-contr-Σ-is-prop p f) (x , y) =
+    eq-type-subtype (λ x' → B x' , p x') (f x y)
 ```
 
 ### The diagonal of contractible types

src/foundation/double-negation-modality.lagda.md

@@ -14,8 +14,8 @@ open import foundation-core.function-types
 open import foundation-core.propositions
 open import foundation-core.transport-along-identifications
 
-open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
 

src/foundation/functoriality-cartesian-product-types.lagda.md

@@ -32,7 +32,7 @@ The **functorial action** of the
 `f : A → B` and `g : C → D` and returns a map
 
 ```text
-  f × g : A × B → C × D`
+  f × g : A × B → C × D
 ```
 
 between the cartesian product types. This functorial action is _bifunctorial_ in

src/foundation/global-subuniverses.lagda.md

@@ -116,7 +116,7 @@ module _
 
 ## Properties
 
-### Global subuniverses are closed under homogenous equivalences
+### Global subuniverses are closed under equivalences between types in a single universe
 
 This is true for any family of subuniverses indexed by universe levels.
 
@@ -126,14 +126,14 @@ module _
   {l : Level} {X Y : UU l}
   where
 
-  is-in-global-subuniverse-homogenous-equiv :
+  is-in-global-subuniverse-equiv-Level :
     X ≃ Y → is-in-global-subuniverse P X → is-in-global-subuniverse P Y
-  is-in-global-subuniverse-homogenous-equiv =
+  is-in-global-subuniverse-equiv-Level =
     is-in-subuniverse-equiv (subuniverse-global-subuniverse P l)
 
-  is-in-global-subuniverse-homogenous-equiv' :
+  is-in-global-subuniverse-equiv-Level' :
     X ≃ Y → is-in-global-subuniverse P Y → is-in-global-subuniverse P X
-  is-in-global-subuniverse-homogenous-equiv' =
+  is-in-global-subuniverse-equiv-Level' =
     is-in-subuniverse-equiv' (subuniverse-global-subuniverse P l)
 ```
 

src/foundation/inhabited-types.lagda.md

@@ -7,9 +7,11 @@ module foundation.inhabited-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
+open import foundation.function-extensionality
 open import foundation.functoriality-propositional-truncation
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.propositional-truncations
@@ -18,6 +20,7 @@ open import foundation.univalence
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.torsorial-type-families
@@ -220,6 +223,27 @@ is-contr-is-inhabited-is-prop {A = A} p h =
     ( λ a → a , eq-is-prop' p a)
 ```
 
+### Contractibility of the base of a dependent sum
+
+Given a type `A` and a type family over it `B`, then if the dependent sum
+`Σ A B` is contractible, it follows that if there merely exists a section
+`(x : A) → B x`, then `A` is contractible.
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2)
+  where
+
+  abstract
+    is-contr-base-is-contr-Σ :
+      is-inhabited ((x : A) → B x) → is-contr (Σ A B) → is-contr A
+    is-contr-base-is-contr-Σ s is-contr-ΣAB =
+      rec-trunc-Prop
+        ( is-contr-Prop A)
+        ( λ s → is-contr-base-is-contr-Σ' A B s is-contr-ΣAB)
+        ( s)
+```
+
 ## See also
 
 - The notion of _nonempty types_ is treated in

src/foundation/precomposition-dependent-functions.lagda.md

@@ -10,17 +10,20 @@ open import foundation-core.precomposition-dependent-functions public
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.dependent-universal-property-equivalences
 open import foundation.function-extensionality
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.equivalences
 open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.truncated-maps
 open import foundation-core.truncation-levels
+open import foundation-core.type-theoretic-principle-of-choice
 ```
 
 </details>
@@ -120,3 +123,37 @@ is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H =
         ( funext (g ∘ f) (h ∘ f))
         ( H g h))
 ```
+
+### The dependent precomposition map at a dependent pair type
+
+Given a map `f : X → Y` and a family `B : (y : Y) → A y → 𝒰` we have an
+equivalence of maps
+
+```text
+                                     precomp-Π f (λ y → Σ (A y) (B y))
+            ((y : Y) → Σ (A y) (B y)) -----------------------------> ((x : X) → Σ (A (f x)) (B (f x)))
+                       |                                                          |
+                     ~ |                                                          | ~
+                       ∨                                                          ∨
+  Σ (a : (y : Y) → A y) ((y : Y) → B y (a y)) --------> Σ (a : (x : X) → A (f x)) ((x : X) → B (f x) (a x)).
+                       map-Σ (precomp-Π f A) (λ a → precomp-Π f (λ y → B y (a y)))
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {X : UU l1} {Y : UU l2} {A : Y → UU l3} {B : (y : Y) → A y → UU l4}
+  {f : X → Y}
+  where
+
+  coherence-precomp-Π-Σ :
+    coherence-square-maps
+      ( precomp-Π f (λ y → Σ (A y) (B y)))
+      ( map-distributive-Π-Σ)
+      ( map-distributive-Π-Σ)
+      ( map-Σ
+        ( λ a → (x : X) → B (f x) (a x))
+        ( precomp-Π f A)
+        ( λ a → precomp-Π f (λ y → B y (a y))))
+  coherence-precomp-Π-Σ = refl-htpy
+```