Maps in subuniverses (UniMath#1163)

A simple PR that moves "maps in subuniverses" to their own file and
formalizes that they are closed under base change.

src/foundation.lagda.md

@@ -249,6 +249,8 @@ open import foundation.lifts-types public
 open import foundation.limited-principle-of-omniscience public
 open import foundation.locally-small-types public
 open import foundation.logical-equivalences public
+open import foundation.maps-in-global-subuniverses public
+open import foundation.maps-in-subuniverses public
 open import foundation.maybe public
 open import foundation.mere-embeddings public
 open import foundation.mere-equality public

src/foundation/cartesian-morphisms-arrows.lagda.md

@@ -22,6 +22,7 @@ open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies-morphisms-arrows
 open import foundation.identity-types
 open import foundation.morphisms-arrows
@@ -174,6 +175,30 @@ module _
       ( is-pullback-cone-fiber f y)
 ```
 
+### The induced family of equivalences of fibers of cartesian morphisms of arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (h : cartesian-hom-arrow f g)
+  where
+
+  equiv-fibers-cartesian-hom-arrow :
+    (b : B) → fiber f b ≃ fiber g (map-codomain-cartesian-hom-arrow f g h b)
+  equiv-fibers-cartesian-hom-arrow b =
+    ( map-fiber-vertical-map-cone
+      ( map-codomain-cartesian-hom-arrow f g h)
+      ( g)
+      ( cone-cartesian-hom-arrow f g h)
+      ( b)) ,
+    ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+      ( map-codomain-cartesian-hom-arrow f g h)
+      ( g)
+      ( cone-cartesian-hom-arrow f g h)
+      ( is-cartesian-cartesian-hom-arrow f g h)
+      ( b))
+```
+
 ### Transposing cartesian morphisms of arrows
 
 The {{#concept "transposition" Disambiguation="cartesian morphism of arrows"}}

src/foundation/global-subuniverses.lagda.md

@@ -67,41 +67,25 @@ record global-subuniverse (α : Level → Level) : UUω where
       (l1 l2 : Level) →
       is-closed-under-equiv-subuniverses α subuniverse-global-subuniverse l1 l2
 
-open global-subuniverse public
-
-module _
-  {α : Level → Level} (P : global-subuniverse α)
-  where
-
   is-in-global-subuniverse : {l : Level} → UU l → UU (α l)
   is-in-global-subuniverse {l} X =
-    is-in-subuniverse (subuniverse-global-subuniverse P l) X
+    is-in-subuniverse (subuniverse-global-subuniverse l) X
+
+  is-prop-is-in-global-subuniverse :
+    {l : Level} (X : UU l) → is-prop (is-in-global-subuniverse X)
+  is-prop-is-in-global-subuniverse {l} X =
+    is-prop-type-Prop (subuniverse-global-subuniverse l X)
 
   type-global-subuniverse : (l : Level) → UU (α l ⊔ lsuc l)
   type-global-subuniverse l =
-    type-subuniverse (subuniverse-global-subuniverse P l)
+    type-subuniverse (subuniverse-global-subuniverse l)
 
   inclusion-global-subuniverse :
     {l : Level} → type-global-subuniverse l → UU l
   inclusion-global-subuniverse {l} =
-    inclusion-subuniverse (subuniverse-global-subuniverse P l)
-```
+    inclusion-subuniverse (subuniverse-global-subuniverse l)
 
-### Maps in a subuniverse
-
-We say a map is _in_ a global subuniverse if each of its
-[fibers](foundation-core.fibers-of-maps.md) is.
-
-```agda
-module _
-  {α : Level → Level} (P : global-subuniverse α)
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  where
-
-  is-in-map-global-subuniverse : (A → B) → UU (α (l1 ⊔ l2) ⊔ l2)
-  is-in-map-global-subuniverse f =
-    (y : B) →
-    is-in-subuniverse (subuniverse-global-subuniverse P (l1 ⊔ l2)) (fiber f y)
+open global-subuniverse public
 ```
 
 ### The predicate of essentially being in a subuniverse

src/foundation/maps-in-global-subuniverses.lagda.md

@@ -0,0 +1,106 @@
+# Maps in global subuniverses
+
+```agda
+module foundation.maps-in-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-morphisms-arrows
+open import foundation.dependent-pair-types
+open import foundation.fibers-of-maps
+open import foundation.functoriality-fibers-of-maps
+open import foundation.global-subuniverses
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+Given a [global subuniverse](foundation.global-subuniverses.md) `𝒫`, a map
+`f : A → B` is said to be a
+{{#concept "map in `𝒫`" Disambiguation="in a global subuniverse" Agda=is-in-global-subuniverse-map}},
+or a **`𝒫`-map**, if its [fibers](foundation-core.fibers-of-maps.md) are in `𝒫`.
+
+## Definitions
+
+### The predicate on maps of being in a global subuniverse
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-in-global-subuniverse-map : UU (α (l1 ⊔ l2) ⊔ l2)
+  is-in-global-subuniverse-map =
+    (b : B) → is-in-global-subuniverse 𝒫 (fiber f b)
+
+  is-prop-is-in-global-subuniverse-map : is-prop is-in-global-subuniverse-map
+  is-prop-is-in-global-subuniverse-map =
+    is-prop-Π (λ b → is-prop-is-in-global-subuniverse 𝒫 (fiber f b))
+
+  is-in-global-subuniverse-map-Prop : Prop (α (l1 ⊔ l2) ⊔ l2)
+  is-in-global-subuniverse-map-Prop =
+    ( is-in-global-subuniverse-map , is-prop-is-in-global-subuniverse-map)
+```
+
+## Properties
+
+### A type is in `𝒫` if and only if its terminal projection is in `𝒫`
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 : Level} {A : UU l1}
+  where
+
+  is-in-global-subuniverse-is-in-global-subuniverse-terminal-map :
+    is-in-global-subuniverse-map 𝒫 (terminal-map A) →
+    is-in-global-subuniverse 𝒫 A
+  is-in-global-subuniverse-is-in-global-subuniverse-terminal-map H =
+    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
+      ( fiber (terminal-map A) star)
+      ( A)
+      ( equiv-fiber-terminal-map star)
+      ( H star)
+
+  is-in-global-subuniverse-terminal-map-is-in-global-subuniverse :
+    is-in-global-subuniverse 𝒫 A →
+    is-in-global-subuniverse-map 𝒫 (terminal-map A)
+  is-in-global-subuniverse-terminal-map-is-in-global-subuniverse H u =
+    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
+      ( A)
+      ( fiber (terminal-map A) u)
+      ( inv-equiv-fiber-terminal-map u)
+      ( H)
+```
+
+### Closure under base change
+
+Maps in `𝒫` are closed under base change.
+
+```agda
+module _
+  {α : Level → Level} (𝒫 : global-subuniverse α)
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (g : C → D)
+  where
+
+  is-in-global-subuniverse-map-base-change :
+    is-in-global-subuniverse-map 𝒫 f →
+    cartesian-hom-arrow g f →
+    is-in-global-subuniverse-map 𝒫 g
+  is-in-global-subuniverse-map-base-change F α d =
+    is-closed-under-equiv-global-subuniverse 𝒫 (l1 ⊔ l2) (l3 ⊔ l4)
+      ( fiber f (map-codomain-cartesian-hom-arrow g f α d))
+      ( fiber g d)
+      ( inv-equiv (equiv-fibers-cartesian-hom-arrow g f α d))
+      ( F (map-codomain-cartesian-hom-arrow g f α d))
+```

src/foundation/maps-in-subuniverses.lagda.md

@@ -0,0 +1,38 @@
+# Maps in subuniverses
+
+```agda
+module foundation.maps-in-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.subuniverses
+open import foundation.universe-levels
+
+open import foundation-core.fibers-of-maps
+```
+
+</details>
+
+## Idea
+
+Given a [subuniverse](foundation.subuniverses.md) `𝒫`, a map `f : A → B` is said
+to be a
+{{#concept "map in `𝒫`" Disambiguation="in a subuniverse" Agda=is-in-subuniverse-map}},
+or a **`𝒫`-map**, if its [fibers](foundation-core.fibers-of-maps.md) are in `𝒫`.
+
+## Definitions
+
+### The predicate on maps of being in a subuniverse
+
+```agda
+is-in-subuniverse-map :
+  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2} →
+  (A → B) → UU (l2 ⊔ l3)
+is-in-subuniverse-map P {A} {B} f = (b : B) → is-in-subuniverse P (fiber f b)
+```
+
+## See also
+
+- [Maps in global subuniverses](foundation.maps-in-global-subuniverses.md)

src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md

@@ -24,6 +24,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.inhabited-types
 open import foundation.logical-equivalences
+open import foundation.maps-in-subuniverses
 open import foundation.propositional-truncations
 open import foundation.separated-types
 open import foundation.subuniverses
@@ -170,13 +171,14 @@ module _
 ```agda
 module _
   {l1 l2 : Level} (k : 𝕋)
-  {A : UU l1} (a : A) {B : A → UU l2} (H : is-0-connected A)
+  {A : UU l1} (a : A) {B : A → UU l2}
   where
 
   forward-implication-extended-fundamental-theorem-id-connected :
+    is-0-connected A →
     ( (f : (x : A) → (a ＝ x) → B x) → (x : A) → is-connected-map k (f x)) →
     is-inhabited (B a) → is-connected (succ-𝕋 k) (Σ A B)
-  forward-implication-extended-fundamental-theorem-id-connected K L =
+  forward-implication-extended-fundamental-theorem-id-connected H K L =
     is-connected-succ-is-connected-eq
       ( map-trunc-Prop (fiber-inclusion B a) L)
       ( forward-implication-extended-fundamental-theorem-id
@@ -199,7 +201,7 @@ module _
     ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-connected-map k (f x)) ↔
     is-connected (succ-𝕋 k) (Σ A B)
   pr1 (extended-fundamental-theorem-id-connected H K) L =
-    forward-implication-extended-fundamental-theorem-id-connected L K
+    forward-implication-extended-fundamental-theorem-id-connected H L K
   pr2 (extended-fundamental-theorem-id-connected H K) =
     backward-implication-extended-fundamental-theorem-id-connected
 ```

src/foundation/subuniverses.lagda.md

@@ -77,15 +77,6 @@ module _
   emb-inclusion-subuniverse = emb-subtype P
 ```
 
-### Maps in a subuniverse
-
-```agda
-is-in-subuniverse-map :
-  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2} →
-  (A → B) → UU (l2 ⊔ l3)
-is-in-subuniverse-map P {A} {B} f = (b : B) → is-in-subuniverse P (fiber f b)
-```
-
 ### The predicate of essentially being in a subuniverse
 
 ```agda