Subuniverse equivalences and connected maps (#1669)

Formalizes `K`-equivalences and `K`-connected maps with respect to an
arbitrary subuniverse `K`.

Builds on #1547.

Author: fredrik-bakke

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

@@ -13,11 +13,15 @@ open import orthogonal-factorization-systems.anodyne-maps public
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
+open import orthogonal-factorization-systems.connected-maps-at-subuniverses public
+open import orthogonal-factorization-systems.connected-maps-at-subuniverses-over-type public
+open import orthogonal-factorization-systems.connected-types-at-subuniverses public
 open import orthogonal-factorization-systems.continuation-modalities public
 open import orthogonal-factorization-systems.double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.double-negation-sheaves public
 open import orthogonal-factorization-systems.equality-extensions-dependent-maps public
 open import orthogonal-factorization-systems.equality-extensions-maps public
+open import orthogonal-factorization-systems.equivalences-at-subuniverses public
 open import orthogonal-factorization-systems.extensions-dependent-maps public
 open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public

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

@@ -0,0 +1,128 @@
+# `K`-connected maps over a type, with respect to a subuniverse `K`
+
+```agda
+module orthogonal-factorization-systems.connected-maps-at-subuniverses-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.connected-maps-at-subuniverses
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `K` we consider the type of
+`K`-[connected maps](orthogonal-factorization-systems.connected-maps-at-subuniverses.md)
+into a type `X`. I.e., the collection of types `A`
+[equipped](foundation.structure.md) with `K`-connected maps from `A` into `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)
+
+  abstract
+    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
+
+  abstract
+    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)
+```