Subuniverse equivalences and connected maps

src/foundation/contractible-types.lagda.md

@@ -23,6 +23,7 @@ open import foundation-core.contractible-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.propositions
 open import foundation-core.subtypes
@@ -197,12 +198,34 @@ module _
       is-equiv-is-invertible
         ( ev-point' (center H))
         ( λ f → eq-htpy (λ x → ap f (contraction H x)))
-        ( λ x → refl)
+        ( refl-htpy)
 
   equiv-diagonal-exponential-is-contr :
     {l : Level} (X : UU l) → is-contr A → X ≃ (A → X)
   pr1 (equiv-diagonal-exponential-is-contr X H) =
     diagonal-exponential X A
   pr2 (equiv-diagonal-exponential-is-contr X H) =
     is-equiv-diagonal-exponential-is-contr H X
+
+  abstract
+    is-equiv-diagonal-exponential-is-contr' :
+      is-contr A →
+      {l : Level} (X : UU l) → is-equiv (diagonal-exponential A X)
+    is-equiv-diagonal-exponential-is-contr' H X =
+      is-equiv-is-invertible
+        ( λ _ → center H)
+        ( λ x → eq-htpy (contraction H ∘ x))
+        ( contraction H)
+
+  equiv-diagonal-exponential-is-contr' :
+    {l : Level} (X : UU l) → is-contr A → A ≃ (X → A)
+  equiv-diagonal-exponential-is-contr' X H =
+    ( diagonal-exponential A X , is-equiv-diagonal-exponential-is-contr' H X)
+
+  abstract
+    is-contr-is-equiv-diagonal-exponential' :
+      ({l : Level} (X : UU l) → is-equiv (diagonal-exponential A X)) →
+      is-contr A
+    is-contr-is-equiv-diagonal-exponential' H =
+      is-contr-is-equiv-self-diagonal-exponential (H A)
 ```

src/foundation/diagonal-maps-of-types.lagda.md

@@ -20,6 +20,7 @@ open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.constant-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
@@ -70,7 +71,7 @@ module _
     inv-htpy htpy-diagonal-exponential-Id-ap-diagonal-exponential-htpy-eq
 ```
 
-### Given an element of the exponent the diagonal map is injective
+### If the exponent has an element then the diagonal map is injective
 
 ```agda
 module _
@@ -86,7 +87,7 @@ module _
   pr2 diagonal-exponential-injection = is-injective-diagonal-exponential
 ```
 
-### The action on identifications of an (exponential) diagonal is a diagonal
+### The action on identifications of a diagonal is a diagonal
 
 ```agda
 module _

src/group-theory/invertible-elements-monoids.lagda.md

@@ -33,7 +33,7 @@ An element `x : M` in a [monoid](group-theory.monoids.md) `M` is said to be
 is said to be **right invertible** if there is an element `y : M` such that
 `xy ＝ e`. The element `x` is said to be
 {{#concept "invertible" WD="invertible element" WDID=Q67474638 Agda=is-invertible-element-Monoid}}
-if it has a two-sided inverse, i.e., if if there is an element `y : M` such that
+if it has a two-sided inverse, i.e., if there is an element `y : M` such that
 `xy = e` and `yx = e`. Left inverses of elements are also called **retractions**
 and right inverses are also called **sections**.
 

src/orthogonal-factorization-systems.lagda.md

@@ -67,6 +67,10 @@ open import orthogonal-factorization-systems.sigma-closed-modalities public
 open import orthogonal-factorization-systems.sigma-closed-reflective-modalities public
 open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses public
 open import orthogonal-factorization-systems.stable-orthogonal-factorization-systems public
+open import orthogonal-factorization-systems.subuniverse-connected-maps public
+open import orthogonal-factorization-systems.subuniverse-connected-maps-over-type public
+open import orthogonal-factorization-systems.subuniverse-connected-types public
+open import orthogonal-factorization-systems.subuniverse-equivalences public
 open import orthogonal-factorization-systems.types-colocal-at-maps public
 open import orthogonal-factorization-systems.types-local-at-maps public
 open import orthogonal-factorization-systems.types-separated-at-maps public

src/orthogonal-factorization-systems/localizations-at-maps.lagda.md

@@ -21,7 +21,7 @@ open import orthogonal-factorization-systems.types-local-at-maps
 
 Let `f` be a map of type `A → B` and let `X` be a type. The **localization** of
 `X` at `f`, or **`f`-localization**, is an
-`f`[-local](orthogonal-factorization-systems.types-local-at-maps.md) type `Y`
+`f`-[local](orthogonal-factorization-systems.types-local-at-maps.md) type `Y`
 together with a map `η : X → Y` with the property that every type that is
 `f`-local is also `η`-local.
 
@@ -81,8 +81,8 @@ module _
     pr1 is-localization-Y
   pr1 (pr2 (is-subuniverse-localization-is-localization is-localization-Y)) = η
   pr2 (pr2 (is-subuniverse-localization-is-localization is-localization-Y))
-    Z is-local-Z =
-      pr2 is-localization-Y Z is-local-Z
+    (Z , is-local-Z) =
+    pr2 is-localization-Y Z is-local-Z
 ```
 
 It remains to construct a converse.

src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md

@@ -12,6 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.subuniverses
 open import foundation.universe-levels
 
+open import orthogonal-factorization-systems.subuniverse-equivalences
 open import orthogonal-factorization-systems.types-local-at-maps
 ```
 
@@ -20,29 +21,38 @@ open import orthogonal-factorization-systems.types-local-at-maps
 ## Idea
 
 Let `P` be a [subuniverse](foundation.subuniverses.md). Given a type `X`, its
-**localization** at `P`, or **`P`-localization**, is a type `Y` in `P` and a map
-`η : X → Y` such that every type in `P` is
-`η`[-local](orthogonal-factorization-systems.types-local-at-maps.md). I.e., for
-every `Z` in `P`, the [precomposition map](foundation-core.function-types.md)
+{{#concept "localization" Disambiguation="of a type at a subuniverse" Agda=subuniverse-localization}}
+at `P`, or **`P`-localization**, is a type `Y` in `P` and a `P`-equivalence
+`η : X → Y`, i.e., a map such that for every `Z` in `P` the
+[precomposition map](foundation-core.function-types.md)
 
 ```text
   - ∘ η : (Y → Z) → (X → Z)
 ```
 
-is an [equivalence](foundation-core.equivalences.md).
+is an [equivalence](foundation-core.equivalences.md). In other words, every type
+in `P` is `η`-[local](orthogonal-factorization-systems.types-local-at-maps.md).
 
 ## Definition
 
+### The predicate on a map of being a localization at a subuniverse
+
+```agda
+is-subuniverse-localization-map :
+  {l1 l2 lP : Level} (P : subuniverse l1 lP) {A : UU l2} {PA : UU l1}
+  (η : A → PA) → UU (lsuc l1 ⊔ l2 ⊔ lP)
+is-subuniverse-localization-map P {A} {PA} η =
+  is-in-subuniverse P PA × is-subuniverse-equiv P η
+```
+
 ### The predicate of being a localization at a subuniverse
 
 ```agda
 is-subuniverse-localization :
   {l1 l2 lP : Level} (P : subuniverse l1 lP) →
   UU l2 → UU l1 → UU (lsuc l1 ⊔ l2 ⊔ lP)
 is-subuniverse-localization {l1} {l2} P X Y =
-  ( is-in-subuniverse P Y) ×
-  ( Σ ( X → Y)
-      ( λ η → (Z : UU l1) → is-in-subuniverse P Z → is-local η Z))
+  (is-in-subuniverse P Y) × (subuniverse-equiv P X Y)
 ```
 
 ```agda
@@ -58,8 +68,7 @@ module _
   unit-is-subuniverse-localization = pr1 (pr2 is-localization-Y)
 
   is-local-at-unit-is-in-subuniverse-is-subuniverse-localization :
-    (Z : UU l1) → is-in-subuniverse P Z →
-    is-local unit-is-subuniverse-localization Z
+    (Z : type-subuniverse P) → is-local unit-is-subuniverse-localization (pr1 Z)
   is-local-at-unit-is-in-subuniverse-is-subuniverse-localization =
     pr2 (pr2 is-localization-Y)
 ```
@@ -91,15 +100,19 @@ module _
     is-in-subuniverse-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 
+  type-subuniverse-subuniverse-localization : type-subuniverse P
+  type-subuniverse-subuniverse-localization =
+    ( type-subuniverse-localization ,
+      is-in-subuniverse-subuniverse-localization)
+
   unit-subuniverse-localization : X → type-subuniverse-localization
   unit-subuniverse-localization =
     unit-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 
-  is-local-at-unit-is-in-subuniverse-subuniverse-localization :
-    (Z : UU l1) →
-    is-in-subuniverse P Z → is-local unit-subuniverse-localization Z
-  is-local-at-unit-is-in-subuniverse-subuniverse-localization =
+  is-subuniverse-equiv-unit-subuniverse-localization :
+    is-subuniverse-equiv P unit-subuniverse-localization
+  is-subuniverse-equiv-unit-subuniverse-localization =
     is-local-at-unit-is-in-subuniverse-is-subuniverse-localization P
       ( is-subuniverse-localization-subuniverse-localization)
 ```

src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md

@@ -167,7 +167,7 @@ module _
   pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) =
     unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫
   pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A)))
-    X is-in-subuniverse-X =
+    ( X , is-in-subuniverse-X) =
       is-local-is-in-subuniverse-is-reflective-subuniverse
         𝒫 is-reflective-𝒫 X A is-in-subuniverse-X
 
@@ -186,8 +186,9 @@ module _
     is-in-subuniverse-subuniverse-localization 𝒫 (L A)
   pr2 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse))
     A B is-in-subuniverse-A =
-    is-local-at-unit-is-in-subuniverse-subuniverse-localization
-      𝒫 (L B) A is-in-subuniverse-A
+    is-subuniverse-equiv-unit-subuniverse-localization 𝒫
+      ( L B)
+      ( A , is-in-subuniverse-A)
 ```
 
 ## Recursion for reflective subuniverses

src/orthogonal-factorization-systems/subuniverse-connected-maps-over-type.lagda.md

@@ -0,0 +1,124 @@
+# `K`-connected maps over a type with respect to a subuniverse
+
+```agda
+module orthogonal-factorization-systems.subuniverse-connected-maps-over-type where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.structure-identity-principle
+open import foundation.subuniverses
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.torsorial-type-families
+
+open import orthogonal-factorization-systems.subuniverse-connected-maps
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K` we consider the type of
+`K`-connected maps over a type `X`.
+
+## Definitions
+
+### The type of `K`-connected maps over a type
+
+```agda
+Subuniverse-Connected-Map :
+  {l1 l2 l3 : Level} (l4 : Level) (K : subuniverse l1 l2) (A : UU l3) →
+  UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
+Subuniverse-Connected-Map l4 K A = Σ (UU l4) (subuniverse-connected-map K A)
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2)
+  {A : UU l3} (f : Subuniverse-Connected-Map l4 K A)
+  where
+
+  type-Subuniverse-Connected-Map : UU l4
+  type-Subuniverse-Connected-Map = pr1 f
+
+  subuniverse-connected-map-Subuniverse-Connected-Map :
+    subuniverse-connected-map K A type-Subuniverse-Connected-Map
+  subuniverse-connected-map-Subuniverse-Connected-Map = pr2 f
+
+  map-Subuniverse-Connected-Map : A → type-Subuniverse-Connected-Map
+  map-Subuniverse-Connected-Map =
+    map-subuniverse-connected-map K
+      ( subuniverse-connected-map-Subuniverse-Connected-Map)
+
+  is-subuniverse-connected-map-Subuniverse-Connected-Map :
+    is-subuniverse-connected-map K map-Subuniverse-Connected-Map
+  is-subuniverse-connected-map-Subuniverse-Connected-Map =
+    is-subuniverse-connected-map-subuniverse-connected-map K
+      ( subuniverse-connected-map-Subuniverse-Connected-Map)
+```
+
+## Properties
+
+### Characterization of equality
+
+```agda
+equiv-Subuniverse-Connected-Map :
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3} →
+  (f g : Subuniverse-Connected-Map l4 K A) → UU (l3 ⊔ l4)
+equiv-Subuniverse-Connected-Map K f g =
+  Σ ( type-Subuniverse-Connected-Map K f ≃ type-Subuniverse-Connected-Map K g)
+    ( λ e →
+      map-equiv e ∘ map-Subuniverse-Connected-Map K f ~
+      map-Subuniverse-Connected-Map K g)
+
+module _
+  {l1 l2 l3 l4 : Level} (K : subuniverse l1 l2) {A : UU l3}
+  (f : Subuniverse-Connected-Map l4 K A)
+  where
+
+  id-equiv-Subuniverse-Connected-Map : equiv-Subuniverse-Connected-Map K f f
+  id-equiv-Subuniverse-Connected-Map = (id-equiv , refl-htpy)
+
+  is-torsorial-equiv-Subuniverse-Connected-Map :
+    is-torsorial (equiv-Subuniverse-Connected-Map K f)
+  is-torsorial-equiv-Subuniverse-Connected-Map =
+    is-torsorial-Eq-structure
+      ( is-torsorial-equiv (type-Subuniverse-Connected-Map K f))
+      ( type-Subuniverse-Connected-Map K f , id-equiv)
+      ( is-torsorial-htpy-subuniverse-connected-map K
+        ( subuniverse-connected-map-Subuniverse-Connected-Map K f))
+
+  equiv-eq-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    f ＝ g → equiv-Subuniverse-Connected-Map K f g
+  equiv-eq-Subuniverse-Connected-Map .f refl =
+    id-equiv-Subuniverse-Connected-Map
+
+  is-equiv-equiv-eq-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    is-equiv (equiv-eq-Subuniverse-Connected-Map g)
+  is-equiv-equiv-eq-Subuniverse-Connected-Map =
+    fundamental-theorem-id
+      ( is-torsorial-equiv-Subuniverse-Connected-Map)
+      ( equiv-eq-Subuniverse-Connected-Map)
+
+  extensionality-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    (f ＝ g) ≃ equiv-Subuniverse-Connected-Map K f g
+  extensionality-Subuniverse-Connected-Map g =
+    ( equiv-eq-Subuniverse-Connected-Map g ,
+      is-equiv-equiv-eq-Subuniverse-Connected-Map g)
+
+  eq-equiv-Subuniverse-Connected-Map :
+    (g : Subuniverse-Connected-Map l4 K A) →
+    equiv-Subuniverse-Connected-Map K f g → f ＝ g
+  eq-equiv-Subuniverse-Connected-Map g =
+    map-inv-equiv (extensionality-Subuniverse-Connected-Map g)
+```