Reflective global subuniverses

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

@@ -92,8 +92,8 @@ module _
       is-contr-retract-of B (f , retraction-is-equiv is-equiv-f)
 
   abstract
-    is-contr-equiv : (e : A ≃ B) → is-contr B → is-contr A
-    is-contr-equiv (pair e is-equiv-e) is-contr-B =
+    is-contr-equiv : A ≃ B → is-contr B → is-contr A
+    is-contr-equiv (e , is-equiv-e) is-contr-B =
       is-contr-is-equiv e is-equiv-e is-contr-B
 
 module _
@@ -133,24 +133,6 @@ 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:
@@ -248,6 +230,24 @@ normalize the extracted information (in this case the first projection of the
 proof of contractibility), but it will normalize the entire proof of
 contractibility first, and then apply the projection.
 
+### 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 and 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)
+```
+
 ### Contractible types are propositions
 
 ```agda

src/foundation-core/fibers-of-maps.lagda.md

@@ -229,9 +229,7 @@ module _
   map-fiber-pr1 ((x , y) , p) = tr B p y
 
   map-inv-fiber-pr1 : B a → fiber (pr1 {B = B}) a
-  pr1 (pr1 (map-inv-fiber-pr1 b)) = a
-  pr2 (pr1 (map-inv-fiber-pr1 b)) = b
-  pr2 (map-inv-fiber-pr1 b) = refl
+  map-inv-fiber-pr1 b = (a , b) , refl
 
   is-section-map-inv-fiber-pr1 :
     is-section map-fiber-pr1 map-inv-fiber-pr1

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

@@ -24,6 +24,9 @@ Functions are primitive in Agda. Here we construct some basic functions
 id : {l : Level} {A : UU l} → A → A
 id a = a
 
+id' : {l : Level} (A : UU l) → A → A
+id' A = id
+
 idω : {A : UUω} → A → A
 idω a = a
 ```

src/foundation.lagda.md

@@ -177,6 +177,8 @@ open import foundation.exclusive-sum public
 open import foundation.existential-quantification public
 open import foundation.exponents-set-quotients public
 open import foundation.extensions-types public
+open import foundation.extensions-types-global-subuniverses public
+open import foundation.extensions-types-subuniverses public
 open import foundation.faithful-maps public
 open import foundation.families-of-equivalences public
 open import foundation.families-of-maps public

src/foundation/commuting-squares-of-maps.lagda.md

@@ -720,7 +720,7 @@ module _
         ap-binary
           ( λ L q → eq-htpy L ∙ q)
           ( eq-htpy (preserves-comp-left-whisker-comp h bottom-right H))
-          ( inv (compute-eq-htpy-ap-precomp top-left (h ·l K)))
+          ( inv (coherence-eq-htpy-ap-precomp top-left (h ·l K)))
 
   distributive-precomp-pasting-vertical-coherence-square-maps :
     ( top : A → X) (left-top : A → B) (right-top : X → Y) (middle : B → Y) →
@@ -805,7 +805,7 @@ module _
         by
         ap-binary
           ( λ p L → p ∙ eq-htpy L)
-          ( inv (compute-eq-htpy-ap-precomp left-top (h ·l K)))
+          ( inv (coherence-eq-htpy-ap-precomp left-top (h ·l K)))
           ( eq-htpy (preserves-comp-left-whisker-comp h right-bottom H))
 ```
 
@@ -856,7 +856,7 @@ module _
     ( ( precomp f W) ·l
       ( precomp-coherence-square-maps top left right bottom H W))
   distributive-precomp-right-whisker-comp-coherence-square-maps f g =
-    inv (compute-eq-htpy-ap-precomp f (g ·l H))
+    inv (coherence-eq-htpy-ap-precomp f (g ·l H))
 ```
 
 Similarly, we can calculate transpositions of left-whiskered squares with the

src/foundation/composition-algebra.lagda.md

@@ -78,7 +78,7 @@ module _
     (h : C → A) (H : f ~ g) (S : UU l4) →
     precomp h S ·l htpy-precomp H S ~ htpy-precomp (H ·r h) S
   inv-distributive-htpy-precomp-right-whisker h H S i =
-    compute-eq-htpy-ap-precomp h (i ·l H)
+    coherence-eq-htpy-ap-precomp h (i ·l H)
 
   distributive-htpy-precomp-right-whisker :
     (h : C → A) (H : f ~ g) (S : UU l4) →

src/foundation/continuations.lagda.md

@@ -34,7 +34,7 @@ open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.transport-along-identifications
 
-open import orthogonal-factorization-systems.extensions-of-maps
+open import orthogonal-factorization-systems.extensions-maps
 open import orthogonal-factorization-systems.modal-operators
 open import orthogonal-factorization-systems.types-local-at-maps
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
@@ -82,8 +82,8 @@ unit-continuation = ev
 ### Maps into `continuation R A` extend along the unit
 
 Every `f` as in the following diagram
-[extends](orthogonal-factorization-systems.extensions-of-maps.md) along the unit
-of its domain
+[extends](orthogonal-factorization-systems.extensions-maps.md) along the unit of
+its domain
 
 ```text
                f

src/foundation/equality-fibers-of-maps.lagda.md

@@ -121,7 +121,7 @@ module _
 
   abstract
     is-equiv-eq-fiber-fiber-ap :
-      (q : (f x) ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
+      (q : f x ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
     is-equiv-eq-fiber-fiber-ap q =
       is-equiv-comp
         ( tr (fiber (ap f)) right-unit)

src/foundation/extensions-types-global-subuniverses.lagda.md

@@ -0,0 +1,231 @@
+# Extensions of types in a global subuniverse
+
+```agda
+module foundation.extensions-types-global-subuniverses where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.extensions-types
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.global-subuniverses
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.propositional-maps
+open import foundation.propositions
+open import foundation.torsorial-type-families
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.univalence
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a type `X`. An
+{{#concept "extension" Disambiguation="type in global subuniverse" Agda=extension-type-global-subuniverse}}
+of `X` in a [global subuniverse](foundation.global-subuniverses.md) `𝒫` is an
+object in the [coslice](foundation.coslice.md) under `X` in `𝒫`, i.e., it
+consists of a type `Y` in `𝒫` and a map `f : X → Y`.
+
+In the above definition of extensions of types in a global subuniverse our aim
+is to capture the most general concept of what it means to be an extension of a
+type in a subuniverse.
+
+Our notion of extensions of types are not to be confused with extension types of
+cubical type theory or
+[extension types of simplicial type theory](https://arxiv.org/abs/1705.07442).
+
+## Definitions
+
+### The predicate on an extension of types of being in a global subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level}
+  (𝒫 : global-subuniverse α) {X : UU l1}
+  (E : extension-type l2 X)
+  where
+
+  is-in-global-subuniverse-extension-type-Prop : Prop (α l2)
+  is-in-global-subuniverse-extension-type-Prop =
+    is-in-global-subuniverse-Prop 𝒫 (type-extension-type E)
+
+  is-in-global-subuniverse-extension-type : UU (α l2)
+  is-in-global-subuniverse-extension-type =
+    is-in-global-subuniverse 𝒫 (type-extension-type E)
+
+  is-prop-is-in-global-subuniverse-extension-type :
+    is-prop is-in-global-subuniverse-extension-type
+  is-prop-is-in-global-subuniverse-extension-type =
+    is-prop-is-in-global-subuniverse 𝒫 (type-extension-type E)
+```
+
+### Extensions of types in a subuniverse
+
+```agda
+extension-type-global-subuniverse :
+  {α : Level → Level} {l1 : Level}
+  (𝒫 : global-subuniverse α) (l2 : Level) (X : UU l1) →
+  UU (α l2 ⊔ l1 ⊔ lsuc l2)
+extension-type-global-subuniverse 𝒫 l2 X =
+  Σ (type-global-subuniverse 𝒫 l2) (λ Y → X → inclusion-global-subuniverse 𝒫 Y)
+
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  (Y : extension-type-global-subuniverse 𝒫 l2 X)
+  where
+
+  type-global-subuniverse-extension-type-global-subuniverse :
+    type-global-subuniverse 𝒫 l2
+  type-global-subuniverse-extension-type-global-subuniverse = pr1 Y
+
+  type-extension-type-global-subuniverse : UU l2
+  type-extension-type-global-subuniverse =
+    inclusion-global-subuniverse 𝒫
+      type-global-subuniverse-extension-type-global-subuniverse
+
+  is-in-global-subuniverse-type-extension-type-global-subuniverse :
+    is-in-global-subuniverse 𝒫 type-extension-type-global-subuniverse
+  is-in-global-subuniverse-type-extension-type-global-subuniverse =
+    is-in-global-subuniverse-inclusion-global-subuniverse 𝒫
+      type-global-subuniverse-extension-type-global-subuniverse
+
+  inclusion-extension-type-global-subuniverse :
+    X → type-extension-type-global-subuniverse
+  inclusion-extension-type-global-subuniverse = pr2 Y
+
+  extension-type-extension-type-global-subuniverse : extension-type l2 X
+  extension-type-extension-type-global-subuniverse =
+    type-extension-type-global-subuniverse ,
+    inclusion-extension-type-global-subuniverse
+```
+
+## Properties
+
+### Extensions of types in a subuniverse are extensions of types by types in the subuniverse
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  compute-extension-type-global-subuniverse :
+    extension-type-global-subuniverse 𝒫 l2 X ≃
+    Σ (extension-type l2 X) (is-in-global-subuniverse-extension-type 𝒫)
+  compute-extension-type-global-subuniverse = equiv-right-swap-Σ
+```
+
+### The inclusion of extensions of types in a subuniverse into extensions of types is an embedding
+
+```agda
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  compute-fiber-extension-type-extension-type-global-subuniverse :
+    (Y : extension-type l2 X) →
+    fiber (extension-type-extension-type-global-subuniverse 𝒫) Y ≃
+    is-in-global-subuniverse 𝒫 (type-extension-type Y)
+  compute-fiber-extension-type-extension-type-global-subuniverse Y =
+    equivalence-reasoning
+    Σ ( Σ (Σ (UU l2) (λ Z → is-in-global-subuniverse 𝒫 Z)) (λ Z → X → pr1 Z))
+      ( λ E → extension-type-extension-type-global-subuniverse 𝒫 E ＝ Y)
+    ≃ Σ ( Σ (extension-type l2 X) (is-in-global-subuniverse-extension-type 𝒫))
+        ( λ E → pr1 E ＝ Y)
+    by
+      equiv-Σ-equiv-base
+        ( λ E → pr1 E ＝ Y)
+        ( compute-extension-type-global-subuniverse 𝒫)
+    ≃ Σ ( Σ (extension-type l2 X) (λ E → E ＝ Y))
+        ( is-in-global-subuniverse-extension-type 𝒫 ∘ pr1)
+      by equiv-right-swap-Σ
+    ≃ is-in-global-subuniverse-extension-type 𝒫 Y
+    by left-unit-law-Σ-is-contr (is-torsorial-Id' Y) (Y , refl)
+
+  is-prop-map-extension-type-extension-type-global-subuniverse :
+    is-prop-map (extension-type-extension-type-global-subuniverse 𝒫)
+  is-prop-map-extension-type-extension-type-global-subuniverse Y =
+    is-prop-equiv
+      ( compute-fiber-extension-type-extension-type-global-subuniverse Y)
+      ( is-prop-is-in-global-subuniverse 𝒫 (type-extension-type Y))
+
+  is-emb-extension-type-extension-type-global-subuniverse :
+    is-emb (extension-type-extension-type-global-subuniverse 𝒫)
+  is-emb-extension-type-extension-type-global-subuniverse =
+    is-emb-is-prop-map
+      is-prop-map-extension-type-extension-type-global-subuniverse
+```
+
+### Characterization of identifications of extensions of types in a subuniverse
+
+```agda
+equiv-extension-type-global-subuniverse :
+  {α : Level → Level} {l1 l2 l3 : Level}
+  (𝒫 : global-subuniverse α) {X : UU l1} →
+  extension-type-global-subuniverse 𝒫 l2 X →
+  extension-type-global-subuniverse 𝒫 l3 X → UU (l1 ⊔ l2 ⊔ l3)
+equiv-extension-type-global-subuniverse 𝒫 U V =
+  equiv-extension-type
+    ( extension-type-extension-type-global-subuniverse 𝒫 U)
+    ( extension-type-extension-type-global-subuniverse 𝒫 V)
+
+module _
+  {α : Level → Level} {l1 l2 : Level} (𝒫 : global-subuniverse α) {X : UU l1}
+  where
+
+  id-equiv-extension-type-global-subuniverse :
+    (U : extension-type-global-subuniverse 𝒫 l2 X) →
+    equiv-extension-type-global-subuniverse 𝒫 U U
+  id-equiv-extension-type-global-subuniverse U =
+    id-equiv-extension-type
+      ( extension-type-extension-type-global-subuniverse 𝒫 U)
+
+  equiv-eq-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    U ＝ V → equiv-extension-type-global-subuniverse 𝒫 U V
+  equiv-eq-extension-type-global-subuniverse U V p =
+    equiv-eq-extension-type
+      ( extension-type-extension-type-global-subuniverse 𝒫 U)
+      ( extension-type-extension-type-global-subuniverse 𝒫 V)
+      ( ap (extension-type-extension-type-global-subuniverse 𝒫) p)
+
+  is-equiv-equiv-eq-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    is-equiv (equiv-eq-extension-type-global-subuniverse U V)
+  is-equiv-equiv-eq-extension-type-global-subuniverse U V =
+    is-equiv-comp
+      ( equiv-eq-extension-type
+        ( extension-type-extension-type-global-subuniverse 𝒫 U)
+        ( extension-type-extension-type-global-subuniverse 𝒫 V))
+      ( ap (extension-type-extension-type-global-subuniverse 𝒫))
+      ( is-emb-extension-type-extension-type-global-subuniverse 𝒫 U V)
+      ( is-equiv-equiv-eq-extension-type
+        ( extension-type-extension-type-global-subuniverse 𝒫 U)
+        ( extension-type-extension-type-global-subuniverse 𝒫 V))
+
+  extensionality-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    (U ＝ V) ≃ equiv-extension-type-global-subuniverse 𝒫 U V
+  extensionality-extension-type-global-subuniverse U V =
+    equiv-eq-extension-type-global-subuniverse U V ,
+    is-equiv-equiv-eq-extension-type-global-subuniverse U V
+
+  eq-equiv-extension-type-global-subuniverse :
+    (U V : extension-type-global-subuniverse 𝒫 l2 X) →
+    equiv-extension-type-global-subuniverse 𝒫 U V → U ＝ V
+  eq-equiv-extension-type-global-subuniverse U V =
+    map-inv-equiv (extensionality-extension-type-global-subuniverse U V)
+```