Define suspension prespectra and maps of prespectra (#833)

src/foundation-core/subtypes.lagda.md

@@ -274,7 +274,7 @@ equiv-subtype-equiv :
   ((x : A) → type-Prop (C x) ↔ type-Prop (D (map-equiv e x))) →
   type-subtype C ≃ type-subtype D
 equiv-subtype-equiv e C D H =
-  equiv-Σ (type-Prop ∘ D) (e) (λ x → equiv-iff' (C x) (D (map-equiv e x)) (H x))
+  equiv-Σ (type-Prop ∘ D) e (λ x → equiv-iff' (C x) (D (map-equiv e x)) (H x))
 ```
 
 ```agda

src/foundation.lagda.md

@@ -83,6 +83,7 @@ open import foundation.dependent-binomial-theorem public
 open import foundation.dependent-epimorphisms public
 open import foundation.dependent-identifications public
 open import foundation.dependent-pair-types public
+open import foundation.dependent-sequences public
 open import foundation.descent-coproduct-types public
 open import foundation.descent-dependent-pair-types public
 open import foundation.descent-empty-types public

src/foundation/dependent-sequences.lagda.md

@@ -0,0 +1,40 @@
+# Dependent sequences
+
+```agda
+module foundation.dependent-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+A **dependent sequence** of elements in a family of types `A : ℕ → UU` is a
+dependent map `(n : ℕ) → A n`.
+
+## Definition
+
+### Dependent sequences of elements in a family of types
+
+```agda
+dependent-sequence : {l : Level} → (ℕ → UU l) → UU l
+dependent-sequence B = (n : ℕ) → B n
+```
+
+### Functorial action on maps of dependent sequences
+
+```agda
+map-dependent-sequence :
+  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} →
+  ((n : ℕ) → A n → B n) → dependent-sequence A → dependent-sequence B
+map-dependent-sequence f a = map-Π f a
+```

src/foundation/sequences.lagda.md

@@ -9,6 +9,7 @@ module foundation.sequences where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-sequences
 open import foundation.universe-levels
 
 open import foundation-core.function-types
@@ -18,18 +19,18 @@ open import foundation-core.function-types
 
 ## Idea
 
-A sequence of elements in a type `A` is a map `ℕ → A`.
+A **sequence** of elements in a type `A` is a map `ℕ → A`.
 
 ## Definition
 
 ### Sequences of elements of a type
 
 ```agda
 sequence : {l : Level} → UU l → UU l
-sequence A = ℕ → A
+sequence A = dependent-sequence (λ _ → A)
 ```
 
-### Functoriality of sequences
+### Functorial action on maps of sequences
 
 ```agda
 map-sequence :

src/foundation/type-arithmetic-dependent-function-types.lagda.md

@@ -33,12 +33,11 @@ module _
 
   left-unit-law-Π-is-contr : ((a : A) → (B a)) ≃ B a
   left-unit-law-Π-is-contr =
-    ( ( left-unit-law-Π ( λ _ → B a)) ∘e
-      ( equiv-Π
-        ( λ _ → B a)
-        ( terminal-map , is-equiv-terminal-map-is-contr C)
-        ( λ a →
-          equiv-eq (ap B ( eq-is-contr C)))))
+    ( left-unit-law-Π ( λ _ → B a)) ∘e
+    ( equiv-Π
+      ( λ _ → B a)
+      ( terminal-map , is-equiv-terminal-map-is-contr C)
+      ( λ a → equiv-eq (ap B ( eq-is-contr C))))
 ```
 
 ### The swap function `((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)` is an equivalence

src/structured-types/pointed-equivalences.lagda.md

@@ -34,9 +34,10 @@ open import structured-types.pointed-types
 
 ## Idea
 
-A pointed equivalence is an equivalence in the category of pointed spaces.
-Equivalently, a pointed equivalence is a pointed map of which the underlying
-function is an equivalence.
+A **pointed equivalence** is an equivalence in the category of pointed spaces.
+Equivalently, a pointed equivalence is a
+[pointed map](structured-types.pointed-maps.md) of which the underlying function
+is an [equivalence](foundation-core.equivalences.md).
 
 ## Definitions
 
@@ -50,6 +51,12 @@ module _
   is-equiv-pointed-map : (A →∗ B) → UU (l1 ⊔ l2)
   is-equiv-pointed-map f = is-equiv (map-pointed-map f)
 
+  is-prop-is-equiv-pointed-map : (f : A →∗ B) → is-prop (is-equiv-pointed-map f)
+  is-prop-is-equiv-pointed-map = is-property-is-equiv ∘ map-pointed-map
+
+  is-equiv-pointed-map-Prop : (A →∗ B) → Prop (l1 ⊔ l2)
+  is-equiv-pointed-map-Prop = is-equiv-Prop ∘ map-pointed-map
+
 pointed-equiv :
   {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) → UU (l1 ⊔ l2)
 pointed-equiv A B =
@@ -64,6 +71,11 @@ compute-pointed-equiv :
   (A ≃∗ B) ≃ Σ (A →∗ B) (is-equiv-pointed-map {A = A} {B})
 compute-pointed-equiv A B = equiv-right-swap-Σ
 
+inv-compute-pointed-equiv :
+  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
+  Σ (A →∗ B) (is-equiv-pointed-map {A = A} {B}) ≃ (A ≃∗ B)
+inv-compute-pointed-equiv A B = equiv-right-swap-Σ
+
 module _
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B)
   where
@@ -199,14 +211,14 @@ module _
             ( inv (preserves-point-pointed-map f))))
         ( equiv-tot
           ( λ p →
-            ( ( equiv-right-transpose-eq-concat
-                ( ap (map-pointed-map f) p)
-                ( preserves-point-pointed-map f)
-                ( is-section-map-inv-is-equiv H (point-Pointed-Type B))) ∘e
-              ( equiv-inv
-                ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
-                ( ( ap (map-pointed-map f) p) ∙
-                  ( preserves-point-pointed-map f)))) ∘e
+            ( equiv-right-transpose-eq-concat
+              ( ap (map-pointed-map f) p)
+              ( preserves-point-pointed-map f)
+              ( is-section-map-inv-is-equiv H (point-Pointed-Type B))) ∘e
+            ( equiv-inv
+              ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
+              ( ( ap (map-pointed-map f) p) ∙
+                ( preserves-point-pointed-map f))) ∘e
             ( equiv-concat'
               ( is-section-map-inv-is-equiv H (point-Pointed-Type B))
               ( right-unit))))
@@ -221,37 +233,22 @@ module _
     is-equiv-pointed-map f → is-contr (retraction-pointed-map f)
   is-contr-retraction-is-equiv-pointed-map H =
     is-contr-total-Eq-structure
-      ( λ g p (G : (g ∘ map-pointed-map f) ~ id) →
+      ( λ g p (G : g ∘ map-pointed-map f ~ id) →
         Id
-          { A =
-            Id
-              { A = type-Pointed-Type A}
-              ( g (map-pointed-map f (point-Pointed-Type A)))
-              ( point-Pointed-Type A)}
           ( G (point-Pointed-Type A))
-          ( ( ( ap g (preserves-point-pointed-map f)) ∙
-              ( p)) ∙
-            ( refl)))
+          ( ( ap g (preserves-point-pointed-map f) ∙ p) ∙ refl))
       ( is-contr-retraction-is-equiv H)
       ( pair (map-inv-is-equiv H) (is-retraction-map-inv-is-equiv H))
       ( is-contr-equiv
         ( fiber
           ( λ p →
-            ( ( ap
-                ( map-inv-is-equiv H)
-                ( preserves-point-pointed-map f)) ∙
-              ( p)) ∙
-            ( refl))
+            ap (map-inv-is-equiv H) (preserves-point-pointed-map f) ∙ p ∙ refl)
           ( is-retraction-map-inv-is-equiv H (point-Pointed-Type A)))
         ( equiv-tot (λ p → equiv-inv _ _))
         ( is-contr-map-is-equiv
           ( is-equiv-comp
-            ( λ q → q ∙ refl)
-            ( λ p →
-              ( ap
-                ( map-inv-is-equiv H)
-                ( preserves-point-pointed-map f)) ∙
-              ( p))
+            ( _∙ refl)
+            ( ap (map-inv-is-equiv H) (preserves-point-pointed-map f) ∙_)
             ( is-equiv-concat
               ( ap
                 ( map-inv-is-equiv H)
@@ -307,8 +304,7 @@ module _
   where
 
   is-equiv-is-equiv-precomp-pointed-map :
-    ( {l : Level} (C : Pointed-Type l) →
-      is-equiv (precomp-pointed-map C f)) →
+    ( {l : Level} (C : Pointed-Type l) → is-equiv (precomp-pointed-map C f)) →
     is-equiv-pointed-map f
   is-equiv-is-equiv-precomp-pointed-map H =
     is-equiv-is-invertible
@@ -431,8 +427,8 @@ module _
   where
 
   is-equiv-is-equiv-comp-pointed-map :
-    ({l : Level} (X : Pointed-Type l) →
-    is-equiv (comp-pointed-map {A = X} f)) → is-equiv-pointed-map f
+    ({l : Level} (X : Pointed-Type l) → is-equiv (comp-pointed-map {A = X} f)) →
+    is-equiv-pointed-map f
   is-equiv-is-equiv-comp-pointed-map H =
     is-equiv-is-invertible
       ( map-pointed-map g)

src/synthetic-homotopy-theory.lagda.md

@@ -48,9 +48,11 @@ open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public
 open import synthetic-homotopy-theory.interval-type public
 open import synthetic-homotopy-theory.iterated-loop-spaces public
+open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-types public
 open import synthetic-homotopy-theory.loop-spaces public
+open import synthetic-homotopy-theory.maps-of-prespectra public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.plus-principle public
@@ -62,7 +64,9 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
+open import synthetic-homotopy-theory.sphere-prespectrum public
 open import synthetic-homotopy-theory.spheres public
+open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.suspensions-of-types public

src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md

@@ -99,10 +99,12 @@ dependent-cocone-map :
   { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
   ( (x : X) → P x) → dependent-cocone f g c P
-dependent-cocone-map f g c P h =
-  ( λ a → h (horizontal-map-cocone f g c a)) ,
-  ( λ b → h (vertical-map-cocone f g c b)) ,
-  ( λ s → apd h (coherence-square-cocone f g c s))
+pr1 (dependent-cocone-map f g c P h) a =
+  h (horizontal-map-cocone f g c a)
+pr1 (pr2 (dependent-cocone-map f g c P h)) b =
+  h (vertical-map-cocone f g c b)
+pr2 (pr2 (dependent-cocone-map f g c P h)) s =
+  apd h (coherence-square-cocone f g c s)
 ```
 
 ## Properties

src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md

@@ -179,7 +179,7 @@ module _
               ( s))))
       ( equiv-dependent-universal-property-unit
         ( λ x → B (north-suspension-structure c)))
-      ( λ N-susp-c →
+      ( λ north-suspension-c →
         ( equiv-Σ
           ( λ s →
             (x : X) →
@@ -189,11 +189,11 @@ module _
               ( map-equiv
                 ( equiv-dependent-universal-property-unit
                   ( λ _ → B (north-suspension-structure c)))
-                ( N-susp-c))
+                ( north-suspension-c))
               ( s)))
           ( equiv-dependent-universal-property-unit
             ( const unit (UU l3) (B (south-suspension-structure c))))
-          ( λ S-susp-c → id-equiv))))
+          ( λ south-suspension-c → id-equiv))))
 
   htpy-map-inv-equiv-dependent-suspension-structure-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure :
     map-inv-equiv equiv-dependent-suspension-structure-suspension-cocone ~

src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md

@@ -27,8 +27,10 @@ open import synthetic-homotopy-theory.loop-spaces
 
 ## Idea
 
-Any pointed map `f : A →∗ B` induces a map `map-Ω f : Ω A →∗ Ω B`. Furthermore,
-this operation respects the groupoidal operations on loop spaces.
+Any [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` induces a
+pointed map `pointed-map-Ω f : Ω A →∗ Ω B`. Furthermore, this operation respects
+the groupoidal operations on
+[loop spaces](synthetic-homotopy-theory.loop-spaces.md).
 
 ## Definition
 
@@ -43,14 +45,15 @@ module _
       ( preserves-point-pointed-map f)
       ( ap (map-pointed-map f) p)
 
-  preserves-refl-map-Ω : Id (map-Ω refl) refl
+  preserves-refl-map-Ω : map-Ω refl ＝ refl
   preserves-refl-map-Ω = preserves-refl-tr-Ω (pr2 f)
 
   pointed-map-Ω : Ω A →∗ Ω B
-  pointed-map-Ω = pair map-Ω preserves-refl-map-Ω
+  pr1 pointed-map-Ω = map-Ω
+  pr2 pointed-map-Ω = preserves-refl-map-Ω
 
   preserves-mul-map-Ω :
-    (x y : type-Ω A) → Id (map-Ω (mul-Ω A x y)) (mul-Ω B (map-Ω x) (map-Ω y))
+    (x y : type-Ω A) → map-Ω (mul-Ω A x y) ＝ mul-Ω B (map-Ω x) (map-Ω y)
   preserves-mul-map-Ω x y =
     ( ap
       ( tr-type-Ω (preserves-point-pointed-map f))
@@ -61,7 +64,7 @@ module _
       ( ap (map-pointed-map f) y))
 
   preserves-inv-map-Ω :
-    (x : type-Ω A) → Id (map-Ω (inv-Ω A x)) (inv-Ω B (map-Ω x))
+    (x : type-Ω A) → map-Ω (inv-Ω A x) ＝ inv-Ω B (map-Ω x)
   preserves-inv-map-Ω x =
     ( ap
       ( tr-type-Ω (preserves-point-pointed-map f))
@@ -84,8 +87,7 @@ module _
     is-emb-comp
       ( tr-type-Ω (preserves-point-pointed-map f))
       ( ap (map-pointed-map f))
-      ( is-emb-is-equiv
-        ( is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
+      ( is-emb-is-equiv (is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
       ( H (point-Pointed-Type A) (point-Pointed-Type A))
 
   emb-Ω :
@@ -102,27 +104,24 @@ module _
 ```agda
 module _
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
-  (f : A →∗ B) (t : is-emb (map-pointed-map f))
+  (f : A →∗ B) (is-emb-f : is-emb (map-pointed-map f))
   where
 
-  is-equiv-map-Ω-emb :
-    is-equiv (map-Ω f)
-  is-equiv-map-Ω-emb =
+  is-equiv-map-Ω-is-emb : is-equiv (map-Ω f)
+  is-equiv-map-Ω-is-emb =
     is-equiv-comp
       ( tr-type-Ω (preserves-point-pointed-map f))
       ( ap (map-pointed-map f))
-      ( t (point-Pointed-Type A) (point-Pointed-Type A))
+      ( is-emb-f (point-Pointed-Type A) (point-Pointed-Type A))
       ( is-equiv-tr-type-Ω (preserves-point-pointed-map f))
 
-  equiv-map-Ω-emb :
-    type-Ω A ≃ type-Ω B
-  pr1 equiv-map-Ω-emb = map-Ω f
-  pr2 equiv-map-Ω-emb = is-equiv-map-Ω-emb
+  equiv-map-Ω-is-emb : type-Ω A ≃ type-Ω B
+  pr1 equiv-map-Ω-is-emb = map-Ω f
+  pr2 equiv-map-Ω-is-emb = is-equiv-map-Ω-is-emb
 
-  pointed-equiv-pointed-map-Ω-emb :
-    Ω A ≃∗ Ω B
-  pr1 pointed-equiv-pointed-map-Ω-emb = equiv-map-Ω-emb
-  pr2 pointed-equiv-pointed-map-Ω-emb = preserves-refl-map-Ω f
+  pointed-equiv-pointed-map-Ω-is-emb : Ω A ≃∗ Ω B
+  pr1 pointed-equiv-pointed-map-Ω-is-emb = equiv-map-Ω-is-emb
+  pr2 pointed-equiv-pointed-map-Ω-is-emb = preserves-refl-map-Ω f
 ```
 
 ### The operator `pointed-map-Ω` preserves equivalences
@@ -136,7 +135,7 @@ module _
   equiv-map-Ω-pointed-equiv :
     type-Ω A ≃ type-Ω B
   equiv-map-Ω-pointed-equiv =
-    equiv-map-Ω-emb
+    equiv-map-Ω-is-emb
       ( pointed-map-pointed-equiv e)
       ( is-emb-is-equiv (is-equiv-map-equiv-pointed-equiv e))
 ```