From 3e9f15a655a4beecf33ac0fbbbcc3fdaac1524e0 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 17:02:59 +0200
Subject: [PATCH 01/11] =?UTF-8?q?define=20infinitely=20deloopable=20types?=
 =?UTF-8?q?=20and=20abelian=20=E2=88=9E-groups?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/higher-group-theory.lagda.md              |  6 ++
 .../abelian-higher-groups.lagda.md            | 55 +++++++++++
 .../infinitely-deloopable-types.lagda.md      | 96 +++++++++++++++++++
 3 files changed, 157 insertions(+)
 create mode 100644 src/higher-group-theory/abelian-higher-groups.lagda.md
 create mode 100644 src/higher-group-theory/infinitely-deloopable-types.lagda.md

diff --git a/src/higher-group-theory.lagda.md b/src/higher-group-theory.lagda.md
index 13e68733d8..1a123c491b 100644
--- a/src/higher-group-theory.lagda.md
+++ b/src/higher-group-theory.lagda.md
@@ -1,10 +1,15 @@
 # Higher group theory
 
+```agda
+{-# OPTIONS --guardedness #-}
+```
+
 ## Files in the higher group theory folder
 
 ```agda
 module higher-group-theory where
 
+open import higher-group-theory.abelian-higher-groups public
 open import higher-group-theory.cartesian-products-higher-groups public
 open import higher-group-theory.conjugation public
 open import higher-group-theory.cyclic-higher-groups public
@@ -19,6 +24,7 @@ open import higher-group-theory.higher-group-actions public
 open import higher-group-theory.higher-groups public
 open import higher-group-theory.homomorphisms-higher-group-actions public
 open import higher-group-theory.homomorphisms-higher-groups public
+open import higher-group-theory.infinitely-deloopable-types public
 open import higher-group-theory.integers-higher-group public
 open import higher-group-theory.iterated-cartesian-products-higher-groups public
 open import higher-group-theory.iterated-deloopings-of-pointed-types public
diff --git a/src/higher-group-theory/abelian-higher-groups.lagda.md b/src/higher-group-theory/abelian-higher-groups.lagda.md
new file mode 100644
index 0000000000..d7ff455e4c
--- /dev/null
+++ b/src/higher-group-theory/abelian-higher-groups.lagda.md
@@ -0,0 +1,55 @@
+# Abelian higher groups
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module higher-group-theory.abelian-higher-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.small-types
+open import foundation.universe-levels
+
+open import higher-group-theory.equivalences-higher-groups
+open import higher-group-theory.higher-groups
+open import higher-group-theory.infinitely-deloopable-types
+open import higher-group-theory.small-higher-groups
+
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-types
+open import structured-types.small-pointed-types
+```
+
+</details>
+
+## Idea
+
+An {{#concept "abelian" Disambiguation="∞-group"}}, or
+{{#concept "commutative" Disambiguation="∞-group"}} ∞-group is a
+[higher group](higher-group-theory.higher-groups.md) that is commutative in a
+fully coherent way. This may be expressed by saying that the underlying
+[pointed type](structured-types.pointed-types.md) is
+[infinitely deloopable](higher-group-theory.infinitely-deloopable-types.md).
+
+Abelian ∞-groups thus give an example of another infinitely coherent structure
+that is definable in Homotopy Type Theory.
+
+## Definitions
+
+### The predicate of being abelian
+
+```agda
+is-abelian-∞-Group : {l : Level} → ∞-Group l → UU (lsuc l)
+is-abelian-∞-Group G = infinite-delooping (pointed-type-∞-Group G)
+```
+
+## Properties
+
+## External links
+
+- [abelian infinity-group](https://ncatlab.org/nlab/show/abelian+infinity-group)
+  at $n$Lab
diff --git a/src/higher-group-theory/infinitely-deloopable-types.lagda.md b/src/higher-group-theory/infinitely-deloopable-types.lagda.md
new file mode 100644
index 0000000000..9198c2cfc6
--- /dev/null
+++ b/src/higher-group-theory/infinitely-deloopable-types.lagda.md
@@ -0,0 +1,96 @@
+# Infinitely deloopable types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module higher-group-theory.infinitely-deloopable-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.small-types
+open import foundation.universe-levels
+
+open import higher-group-theory.deloopable-types
+open import higher-group-theory.equivalences-higher-groups
+open import higher-group-theory.higher-groups
+open import higher-group-theory.small-higher-groups
+
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-types
+open import structured-types.small-pointed-types
+```
+
+</details>
+
+## Idea
+
+A [pointed type](structured-types.pointed-types.md) `X` is said to be
+{{#concept "infinitely deloopable" Disambiguation="pointed type" Agda=infinite-delooping}}
+if it is
+[$n$-deloopable](higher-group-theory.iterated-deloopings-of-pointed-types.md)
+for all $n$, or equivalently, if it is
+[deloopable](higher-group-theory.deloopable-types.md) and coinductively its
+delooping is also infinitely deloopable.
+
+### Relation to commutative higher group structures
+
+An infinite delooping of a pointed type `X` is, in a specific sense, a
+{{#concept "commutative ∞-group structure" Agda=infinite-delooping}} on `X`. In
+other words, the type `infinite-delooping X` is the type of commutative ∞-group
+structures on `X`.
+
+Being infinitely deloopable is therefore a [structure](foundation.structure.md),
+and usually not a [property](foundation-core.propositions.md). If there are
+multiple distinct ways to equip a pointed type `X` with the structure of a
+commutative ∞-group, or even with the structure of an
+[abelian group](group-theory.abelian-groups.md), then the type of infinite
+deloopings of `X` will not be a proposition. For instance, the
+[standard `4`-element type](univalent-combinatorics.standard-finite-types.md)
+`Fin 4` is infinitely deloopable in multiple distinct ways, by equipping it with
+the [cyclic group structure](group-theory.cyclic-groups.md) of `ℤ₄` or by
+equipping it with the group structure of `ℤ₂ × ℤ₂`.
+
+## Definitions
+
+### The type of infinite deloopings of a pointed type
+
+```agda
+record
+  infinite-delooping
+  {l : Level} (X : Pointed-Type l) : UU (lsuc l)
+  where
+  coinductive
+  field
+    ∞-group-infinite-delooping : ∞-Group l
+
+    is-delooping-infinite-delooping :
+      is-delooping X ∞-group-infinite-delooping
+
+  classifying-pointed-type-infinite-delooping : Pointed-Type l
+  classifying-pointed-type-infinite-delooping =
+    classifying-pointed-type-∞-Group ∞-group-infinite-delooping
+
+  classifying-type-infinite-delooping : UU l
+  classifying-type-infinite-delooping =
+    classifying-type-∞-Group ∞-group-infinite-delooping
+
+  equiv-is-delooping-infinite-delooping :
+    type-Pointed-Type X ≃ type-∞-Group ∞-group-infinite-delooping
+  equiv-is-delooping-infinite-delooping =
+    equiv-pointed-equiv is-delooping-infinite-delooping
+
+  field
+    infinite-delooping-∞-group-infinite-delooping :
+      infinite-delooping classifying-pointed-type-infinite-delooping
+
+open infinite-delooping public
+```
+
+## External links
+
+- [infinite loop space](https://ncatlab.org/nlab/show/infinite+loop+space) at
+  $n$Lab

From 8035fdbfc34d4cb15912275099a042b0d623e004 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 21:21:15 +0200
Subject: [PATCH 02/11] connective spectra

---
 src/synthetic-homotopy-theory.lagda.md        |   2 +
 .../connective-prespectra.lagda.md            | 142 +++++++++++++++
 .../connective-spectra.lagda.md               | 164 ++++++++++++++++++
 3 files changed, 308 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/connective-prespectra.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/connective-spectra.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 6a4d8548fa..6b4ee10ea0 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -28,6 +28,8 @@ open import synthetic-homotopy-theory.coforks public
 open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.conjugation-loops public
 open import synthetic-homotopy-theory.connected-set-bundles-circle public
+open import synthetic-homotopy-theory.connective-prespectra public
+open import synthetic-homotopy-theory.connective-spectra public
 open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.dependent-cocones-under-spans public
 open import synthetic-homotopy-theory.dependent-coforks public
diff --git a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
new file mode 100644
index 0000000000..15dbbc4559
--- /dev/null
+++ b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
@@ -0,0 +1,142 @@
+# Connective prespectra
+
+```agda
+module synthetic-homotopy-theory.connective-prespectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.connected-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.truncation-levels
+open import foundation.universe-levels
+
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+open import synthetic-homotopy-theory.suspensions-of-types
+```
+
+</details>
+
+## Idea
+
+A [prespectrum] is {{#concept "connective" Agda=is-connective-Prespectrum}} if
+the $n$th type in the [sequence](foundation.sequences.md) is
+$n$-[connected](foundation.connected-types.md).
+
+### The predicate on prespectra of being connective
+
+```agda
+module _
+  {l : Level} (A : Prespectrum l)
+  where
+
+  is-connective-Prespectrum : UU l
+  is-connective-Prespectrum =
+    (n : ℕ) → is-connected (truncation-level-ℕ n) (type-Prespectrum A n)
+
+  is-prop-is-connective-Prespectrum : is-prop is-connective-Prespectrum
+  is-prop-is-connective-Prespectrum =
+    is-prop-Π
+      ( λ n →
+        is-prop-is-connected (truncation-level-ℕ n) (type-Prespectrum A n))
+
+  is-connective-prop-Prespectrum : Prop l
+  is-connective-prop-Prespectrum =
+    is-connective-Prespectrum , is-prop-is-connective-Prespectrum
+```
+
+### The type of connective prespectra
+
+```agda
+Connective-Prespectrum : (l : Level) → UU (lsuc l)
+Connective-Prespectrum l = Σ (Prespectrum l) (is-connective-Prespectrum)
+
+module _
+  {l : Level} (A : Connective-Prespectrum l)
+  where
+
+  prespectrum-Connective-Prespectrum : Prespectrum l
+  prespectrum-Connective-Prespectrum = pr1 A
+
+  pointed-type-Connective-Prespectrum : ℕ → Pointed-Type l
+  pointed-type-Connective-Prespectrum =
+    pointed-type-Prespectrum prespectrum-Connective-Prespectrum
+
+  type-Connective-Prespectrum : ℕ → UU l
+  type-Connective-Prespectrum =
+    type-Prespectrum prespectrum-Connective-Prespectrum
+
+  point-Connective-Prespectrum : (n : ℕ) → type-Connective-Prespectrum n
+  point-Connective-Prespectrum =
+    point-Prespectrum prespectrum-Connective-Prespectrum
+
+  pointed-adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    pointed-type-Connective-Prespectrum n →∗
+    Ω (pointed-type-Connective-Prespectrum (succ-ℕ n))
+  pointed-adjoint-structure-map-Connective-Prespectrum =
+    pointed-adjoint-structure-map-Prespectrum prespectrum-Connective-Prespectrum
+
+  adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    type-Connective-Prespectrum n →
+    type-Ω (pointed-type-Connective-Prespectrum (succ-ℕ n))
+  adjoint-structure-map-Connective-Prespectrum =
+    adjoint-structure-map-Prespectrum prespectrum-Connective-Prespectrum
+
+  preserves-point-adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    adjoint-structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
+    refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))
+  preserves-point-adjoint-structure-map-Connective-Prespectrum =
+    preserves-point-adjoint-structure-map-Prespectrum
+      prespectrum-Connective-Prespectrum
+
+  is-connective-Connective-Prespectrum :
+    is-connective-Prespectrum prespectrum-Connective-Prespectrum
+  is-connective-Connective-Prespectrum = pr2 A
+```
+
+### The structure maps of a connective prespectrum
+
+```agda
+module _
+  {l : Level} (A : Connective-Prespectrum l) (n : ℕ)
+  where
+
+  pointed-structure-map-Connective-Prespectrum :
+    suspension-Pointed-Type (pointed-type-Connective-Prespectrum A n) →∗
+    pointed-type-Connective-Prespectrum A (succ-ℕ n)
+  pointed-structure-map-Connective-Prespectrum =
+    pointed-structure-map-Prespectrum (prespectrum-Connective-Prespectrum A) n
+
+  structure-map-Connective-Prespectrum :
+    suspension (type-Connective-Prespectrum A n) →
+    type-Connective-Prespectrum A (succ-ℕ n)
+  structure-map-Connective-Prespectrum =
+    map-pointed-map pointed-structure-map-Connective-Prespectrum
+
+  preserves-point-structure-map-Connective-Prespectrum :
+    structure-map-Connective-Prespectrum north-suspension ＝
+    point-Connective-Prespectrum A (succ-ℕ n)
+  preserves-point-structure-map-Connective-Prespectrum =
+    preserves-point-pointed-map pointed-structure-map-Connective-Prespectrum
+```
+
+## External links
+
+- [connective spectrum](https://ncatlab.org/nlab/show/connective+spectrum) at
+  $n$Lab
diff --git a/src/synthetic-homotopy-theory/connective-spectra.lagda.md b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
new file mode 100644
index 0000000000..6c7cf46160
--- /dev/null
+++ b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
@@ -0,0 +1,164 @@
+# Connective spectra
+
+```agda
+module synthetic-homotopy-theory.connective-spectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.connected-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.truncation-levels
+open import foundation.universe-levels
+
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.connective-prespectra
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.spectra
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+open import synthetic-homotopy-theory.suspensions-of-types
+```
+
+</details>
+
+## Idea
+
+A [spectrum] is {{#concept "connective" Agda=is-connective-Spectrum}} if the
+underlying [prespectrum](synthetic-homotopy-theory.prespectra.md) is
+[connective](synthetic-homotopy-theory.connective-prespectra.md). I.e., if the
+$n$th type in the [sequence](foundation.sequences.md) is
+$n$-[connected](foundation.connected-types.md) for all $n$.
+
+### The predicate on spectra of being connective
+
+```agda
+module _
+  {l : Level} (A : Spectrum l)
+  where
+
+  is-connective-Spectrum : UU l
+  is-connective-Spectrum = is-connective-Prespectrum (prespectrum-Spectrum A)
+
+  is-prop-is-connective-Spectrum : is-prop is-connective-Spectrum
+  is-prop-is-connective-Spectrum =
+    is-prop-is-connective-Prespectrum (prespectrum-Spectrum A)
+
+  is-connective-prop-Spectrum : Prop l
+  is-connective-prop-Spectrum =
+    is-connective-Spectrum , is-prop-is-connective-Spectrum
+```
+
+### The type of connective spectra
+
+```agda
+Connective-Spectrum : (l : Level) → UU (lsuc l)
+Connective-Spectrum l = Σ (Spectrum l) (is-connective-Spectrum)
+
+module _
+  {l : Level} (A : Connective-Spectrum l)
+  where
+
+  spectrum-Connective-Spectrum : Spectrum l
+  spectrum-Connective-Spectrum = pr1 A
+
+  pointed-type-Connective-Spectrum : ℕ → Pointed-Type l
+  pointed-type-Connective-Spectrum =
+    pointed-type-Spectrum spectrum-Connective-Spectrum
+
+  type-Connective-Spectrum : ℕ → UU l
+  type-Connective-Spectrum =
+    type-Spectrum spectrum-Connective-Spectrum
+
+  point-Connective-Spectrum : (n : ℕ) → type-Connective-Spectrum n
+  point-Connective-Spectrum =
+    point-Spectrum spectrum-Connective-Spectrum
+
+  pointed-adjoint-structure-map-Connective-Spectrum :
+    (n : ℕ) →
+    pointed-type-Connective-Spectrum n →∗
+    Ω (pointed-type-Connective-Spectrum (succ-ℕ n))
+  pointed-adjoint-structure-map-Connective-Spectrum =
+    pointed-adjoint-structure-map-Spectrum spectrum-Connective-Spectrum
+
+  adjoint-structure-map-Connective-Spectrum :
+    (n : ℕ) →
+    type-Connective-Spectrum n →
+    type-Ω (pointed-type-Connective-Spectrum (succ-ℕ n))
+  adjoint-structure-map-Connective-Spectrum =
+    adjoint-structure-map-Spectrum spectrum-Connective-Spectrum
+
+  preserves-point-adjoint-structure-map-Connective-Spectrum :
+    (n : ℕ) →
+    adjoint-structure-map-Spectrum (pr1 A) n (point-Spectrum (pr1 A) n) ＝
+    refl-Ω (pointed-type-Spectrum (pr1 A) (succ-ℕ n))
+  preserves-point-adjoint-structure-map-Connective-Spectrum =
+    preserves-point-adjoint-structure-map-Spectrum
+      spectrum-Connective-Spectrum
+
+  is-equiv-pointed-adjoint-structure-map-Connective-Spectrum :
+    (n : ℕ) → is-pointed-equiv (pointed-adjoint-structure-map-Connective-Spectrum n)
+  is-equiv-pointed-adjoint-structure-map-Connective-Spectrum =
+    is-equiv-pointed-adjoint-structure-map-Spectrum spectrum-Connective-Spectrum
+
+  structure-equiv-Connective-Spectrum :
+    (n : ℕ) →
+    type-Connective-Spectrum n ≃
+    type-Ω (pointed-type-Connective-Spectrum (succ-ℕ n))
+  structure-equiv-Connective-Spectrum n =
+    adjoint-structure-map-Connective-Spectrum n ,
+    is-equiv-pointed-adjoint-structure-map-Connective-Spectrum n
+
+  pointed-structure-equiv-Connective-Spectrum :
+    (n : ℕ) →
+    pointed-type-Connective-Spectrum n ≃∗
+    Ω (pointed-type-Connective-Spectrum (succ-ℕ n))
+  pointed-structure-equiv-Connective-Spectrum n =
+    structure-equiv-Connective-Spectrum n ,
+    preserves-point-adjoint-structure-map-Connective-Spectrum n
+
+  is-connective-Connective-Spectrum :
+    is-connective-Spectrum spectrum-Connective-Spectrum
+  is-connective-Connective-Spectrum = pr2 A
+```
+
+### The structure maps of a connective spectrum
+
+```agda
+module _
+  {l : Level} (A : Connective-Spectrum l) (n : ℕ)
+  where
+
+  pointed-structure-map-Connective-Spectrum :
+    suspension-Pointed-Type (pointed-type-Connective-Spectrum A n) →∗
+    pointed-type-Connective-Spectrum A (succ-ℕ n)
+  pointed-structure-map-Connective-Spectrum =
+    pointed-structure-map-Spectrum (spectrum-Connective-Spectrum A) n
+
+  structure-map-Connective-Spectrum :
+    suspension (type-Connective-Spectrum A n) →
+    type-Connective-Spectrum A (succ-ℕ n)
+  structure-map-Connective-Spectrum =
+    map-pointed-map pointed-structure-map-Connective-Spectrum
+
+  preserves-point-structure-map-Connective-Spectrum :
+    structure-map-Connective-Spectrum north-suspension ＝
+    point-Connective-Spectrum A (succ-ℕ n)
+  preserves-point-structure-map-Connective-Spectrum =
+    preserves-point-pointed-map pointed-structure-map-Connective-Spectrum
+```
+
+## External links
+
+- [connective spectrum](https://ncatlab.org/nlab/show/connective+spectrum) at
+  $n$Lab

From 57ad8b00f83e60e308040f14ea678d8d72eee631 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 21:22:48 +0200
Subject: [PATCH 03/11] fix definition abelian higher group

---
 src/foundation/connected-types.lagda.md       |  4 +-
 .../abelian-higher-groups.lagda.md            | 38 +++++++---
 .../infinitely-deloopable-types.lagda.md      | 75 ++++++++++++++++++-
 3 files changed, 103 insertions(+), 14 deletions(-)

diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md
index 193097e706..1200702f88 100644
--- a/src/foundation/connected-types.lagda.md
+++ b/src/foundation/connected-types.lagda.md
@@ -220,6 +220,6 @@ module _
     A retract-of B →
     is-connected k B →
     is-connected k A
-  is-connected-retract-of R c =
-    is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R) c
+  is-connected-retract-of R =
+    is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R)
 ```
diff --git a/src/higher-group-theory/abelian-higher-groups.lagda.md b/src/higher-group-theory/abelian-higher-groups.lagda.md
index d7ff455e4c..af62b76b62 100644
--- a/src/higher-group-theory/abelian-higher-groups.lagda.md
+++ b/src/higher-group-theory/abelian-higher-groups.lagda.md
@@ -1,8 +1,6 @@
 # Abelian higher groups
 
 ```agda
-{-# OPTIONS --guardedness #-}
-
 module higher-group-theory.abelian-higher-groups where
 ```
 
@@ -16,12 +14,13 @@ open import foundation.universe-levels
 
 open import higher-group-theory.equivalences-higher-groups
 open import higher-group-theory.higher-groups
-open import higher-group-theory.infinitely-deloopable-types
 open import higher-group-theory.small-higher-groups
 
 open import structured-types.pointed-equivalences
 open import structured-types.pointed-types
 open import structured-types.small-pointed-types
+
+open import synthetic-homotopy-theory.connective-spectra
 ```
 
 </details>
@@ -30,25 +29,44 @@ open import structured-types.small-pointed-types
 
 An {{#concept "abelian" Disambiguation="∞-group"}}, or
 {{#concept "commutative" Disambiguation="∞-group"}} ∞-group is a
-[higher group](higher-group-theory.higher-groups.md) that is commutative in a
-fully coherent way. This may be expressed by saying that the underlying
-[pointed type](structured-types.pointed-types.md) is
-[infinitely deloopable](higher-group-theory.infinitely-deloopable-types.md).
+[higher group](higher-group-theory.higher-groups.md) `A₀` that is commutative in
+a fully coherent way. This may be expressed by saying that there exists a
+[connective spectrum](synthetic-homotopy-theory.connective-spectra.md) such that
+the ∞-group is the first type in the sequence. I.e., there exists a sequence of
+increasingly [connected](foundation.connected-types.md) ∞-groups
+
+```text
+  A₀   A₁   A₂   A₃   ⋯   Aᵢ   ⋯
+```
+
+such that
+
+```text
+  Aᵢ ≃∗ Ω Aᵢ₊₁
+```
 
 Abelian ∞-groups thus give an example of another infinitely coherent structure
 that is definable in Homotopy Type Theory.
 
 ## Definitions
 
+### The predicate of being abelian with respect to a universe level
+
+```agda
+is-abelian-level-∞-Group :
+  {l : Level} (l1 : Level) → ∞-Group l → UU (l ⊔ lsuc l1)
+is-abelian-level-∞-Group l1 G =
+  Σ ( Connective-Spectrum l1)
+    ( λ A → pointed-type-∞-Group G ≃∗ pointed-type-Connective-Spectrum A 0)
+```
+
 ### The predicate of being abelian
 
 ```agda
 is-abelian-∞-Group : {l : Level} → ∞-Group l → UU (lsuc l)
-is-abelian-∞-Group G = infinite-delooping (pointed-type-∞-Group G)
+is-abelian-∞-Group {l} G = is-abelian-level-∞-Group l G
 ```
 
-## Properties
-
 ## External links
 
 - [abelian infinity-group](https://ncatlab.org/nlab/show/abelian+infinity-group)
diff --git a/src/higher-group-theory/infinitely-deloopable-types.lagda.md b/src/higher-group-theory/infinitely-deloopable-types.lagda.md
index 9198c2cfc6..a4dce748c3 100644
--- a/src/higher-group-theory/infinitely-deloopable-types.lagda.md
+++ b/src/higher-group-theory/infinitely-deloopable-types.lagda.md
@@ -9,9 +9,15 @@ module higher-group-theory.infinitely-deloopable-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.0-connected-types
+open import foundation.connected-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.function-types
 open import foundation.small-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import higher-group-theory.deloopable-types
@@ -20,8 +26,13 @@ open import higher-group-theory.higher-groups
 open import higher-group-theory.small-higher-groups
 
 open import structured-types.pointed-equivalences
+open import structured-types.pointed-maps
 open import structured-types.pointed-types
 open import structured-types.small-pointed-types
+
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.spectra
 ```
 
 </details>
@@ -32,7 +43,7 @@ A [pointed type](structured-types.pointed-types.md) `X` is said to be
 {{#concept "infinitely deloopable" Disambiguation="pointed type" Agda=infinite-delooping}}
 if it is
 [$n$-deloopable](higher-group-theory.iterated-deloopings-of-pointed-types.md)
-for all $n$, or equivalently, if it is
+for all $n$ such that the deloopings agree, or equivalently, if it is
 [deloopable](higher-group-theory.deloopable-types.md) and coinductively its
 delooping is also infinitely deloopable.
 
@@ -84,12 +95,72 @@ record
     equiv-pointed-equiv is-delooping-infinite-delooping
 
   field
-    infinite-delooping-∞-group-infinite-delooping :
+    infinite-delooping-classifying-pointed-type-infinite-delooping :
       infinite-delooping classifying-pointed-type-infinite-delooping
 
 open infinite-delooping public
 ```
 
+## Properties
+
+### The underlying spectrum associated to an infinitely deloopable type
+
+```agda
+module _
+  {l : Level}
+  where
+
+  pointed-type-family-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) → ℕ → Pointed-Type l
+  pointed-type-family-infinite-delooping X D zero-ℕ = X
+  pointed-type-family-infinite-delooping X D (succ-ℕ n) =
+    pointed-type-family-infinite-delooping
+      ( classifying-pointed-type-infinite-delooping D)
+      ( infinite-delooping-classifying-pointed-type-infinite-delooping D)
+      ( n)
+
+  type-family-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) → ℕ → UU l
+  type-family-infinite-delooping X D =
+    type-Pointed-Type ∘ pointed-type-family-infinite-delooping X D
+
+  pointed-equiv-family-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) (n : ℕ) →
+    pointed-type-family-infinite-delooping X D n ≃∗
+    Ω (pointed-type-family-infinite-delooping X D (succ-ℕ n))
+  pointed-equiv-family-infinite-delooping X D zero-ℕ =
+    is-delooping-infinite-delooping D
+  pointed-equiv-family-infinite-delooping X D (succ-ℕ n) =
+    pointed-equiv-family-infinite-delooping
+      ( classifying-pointed-type-infinite-delooping D)
+      ( infinite-delooping-classifying-pointed-type-infinite-delooping D)
+      ( n)
+
+  pointed-map-family-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) (n : ℕ) →
+    pointed-type-family-infinite-delooping X D n →∗
+    Ω (pointed-type-family-infinite-delooping X D (succ-ℕ n))
+  pointed-map-family-infinite-delooping X D =
+    pointed-map-pointed-equiv ∘ pointed-equiv-family-infinite-delooping X D
+
+  prespectrum-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) → Prespectrum l
+  prespectrum-infinite-delooping X D =
+    pointed-type-family-infinite-delooping X D ,
+    pointed-map-family-infinite-delooping X D
+
+  is-spectrum-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) →
+    is-spectrum (prespectrum-infinite-delooping X D)
+  is-spectrum-infinite-delooping X D =
+    is-equiv-map-pointed-equiv ∘ pointed-equiv-family-infinite-delooping X D
+
+  spectrum-infinite-delooping :
+    (X : Pointed-Type l) (D : infinite-delooping X) → Spectrum l
+  spectrum-infinite-delooping X D =
+    prespectrum-infinite-delooping X D , is-spectrum-infinite-delooping X D
+```
+
 ## External links
 
 - [infinite loop space](https://ncatlab.org/nlab/show/infinite+loop+space) at

From ad641f5f7b2d8defa835b0a5863cd755550bd2c7 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 21:25:58 +0200
Subject: [PATCH 04/11] delete infinitely deloopable types

---
 src/higher-group-theory.lagda.md              |   1 -
 .../infinitely-deloopable-types.lagda.md      | 167 ------------------
 2 files changed, 168 deletions(-)
 delete mode 100644 src/higher-group-theory/infinitely-deloopable-types.lagda.md

diff --git a/src/higher-group-theory.lagda.md b/src/higher-group-theory.lagda.md
index 1a123c491b..5301e15401 100644
--- a/src/higher-group-theory.lagda.md
+++ b/src/higher-group-theory.lagda.md
@@ -24,7 +24,6 @@ open import higher-group-theory.higher-group-actions public
 open import higher-group-theory.higher-groups public
 open import higher-group-theory.homomorphisms-higher-group-actions public
 open import higher-group-theory.homomorphisms-higher-groups public
-open import higher-group-theory.infinitely-deloopable-types public
 open import higher-group-theory.integers-higher-group public
 open import higher-group-theory.iterated-cartesian-products-higher-groups public
 open import higher-group-theory.iterated-deloopings-of-pointed-types public
diff --git a/src/higher-group-theory/infinitely-deloopable-types.lagda.md b/src/higher-group-theory/infinitely-deloopable-types.lagda.md
deleted file mode 100644
index a4dce748c3..0000000000
--- a/src/higher-group-theory/infinitely-deloopable-types.lagda.md
+++ /dev/null
@@ -1,167 +0,0 @@
-# Infinitely deloopable types
-
-```agda
-{-# OPTIONS --guardedness #-}
-
-module higher-group-theory.infinitely-deloopable-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.0-connected-types
-open import foundation.connected-types
-open import foundation.dependent-pair-types
-open import foundation.equivalences
-open import foundation.function-types
-open import foundation.small-types
-open import foundation.truncation-levels
-open import foundation.universe-levels
-
-open import higher-group-theory.deloopable-types
-open import higher-group-theory.equivalences-higher-groups
-open import higher-group-theory.higher-groups
-open import higher-group-theory.small-higher-groups
-
-open import structured-types.pointed-equivalences
-open import structured-types.pointed-maps
-open import structured-types.pointed-types
-open import structured-types.small-pointed-types
-
-open import synthetic-homotopy-theory.loop-spaces
-open import synthetic-homotopy-theory.prespectra
-open import synthetic-homotopy-theory.spectra
-```
-
-</details>
-
-## Idea
-
-A [pointed type](structured-types.pointed-types.md) `X` is said to be
-{{#concept "infinitely deloopable" Disambiguation="pointed type" Agda=infinite-delooping}}
-if it is
-[$n$-deloopable](higher-group-theory.iterated-deloopings-of-pointed-types.md)
-for all $n$ such that the deloopings agree, or equivalently, if it is
-[deloopable](higher-group-theory.deloopable-types.md) and coinductively its
-delooping is also infinitely deloopable.
-
-### Relation to commutative higher group structures
-
-An infinite delooping of a pointed type `X` is, in a specific sense, a
-{{#concept "commutative ∞-group structure" Agda=infinite-delooping}} on `X`. In
-other words, the type `infinite-delooping X` is the type of commutative ∞-group
-structures on `X`.
-
-Being infinitely deloopable is therefore a [structure](foundation.structure.md),
-and usually not a [property](foundation-core.propositions.md). If there are
-multiple distinct ways to equip a pointed type `X` with the structure of a
-commutative ∞-group, or even with the structure of an
-[abelian group](group-theory.abelian-groups.md), then the type of infinite
-deloopings of `X` will not be a proposition. For instance, the
-[standard `4`-element type](univalent-combinatorics.standard-finite-types.md)
-`Fin 4` is infinitely deloopable in multiple distinct ways, by equipping it with
-the [cyclic group structure](group-theory.cyclic-groups.md) of `ℤ₄` or by
-equipping it with the group structure of `ℤ₂ × ℤ₂`.
-
-## Definitions
-
-### The type of infinite deloopings of a pointed type
-
-```agda
-record
-  infinite-delooping
-  {l : Level} (X : Pointed-Type l) : UU (lsuc l)
-  where
-  coinductive
-  field
-    ∞-group-infinite-delooping : ∞-Group l
-
-    is-delooping-infinite-delooping :
-      is-delooping X ∞-group-infinite-delooping
-
-  classifying-pointed-type-infinite-delooping : Pointed-Type l
-  classifying-pointed-type-infinite-delooping =
-    classifying-pointed-type-∞-Group ∞-group-infinite-delooping
-
-  classifying-type-infinite-delooping : UU l
-  classifying-type-infinite-delooping =
-    classifying-type-∞-Group ∞-group-infinite-delooping
-
-  equiv-is-delooping-infinite-delooping :
-    type-Pointed-Type X ≃ type-∞-Group ∞-group-infinite-delooping
-  equiv-is-delooping-infinite-delooping =
-    equiv-pointed-equiv is-delooping-infinite-delooping
-
-  field
-    infinite-delooping-classifying-pointed-type-infinite-delooping :
-      infinite-delooping classifying-pointed-type-infinite-delooping
-
-open infinite-delooping public
-```
-
-## Properties
-
-### The underlying spectrum associated to an infinitely deloopable type
-
-```agda
-module _
-  {l : Level}
-  where
-
-  pointed-type-family-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) → ℕ → Pointed-Type l
-  pointed-type-family-infinite-delooping X D zero-ℕ = X
-  pointed-type-family-infinite-delooping X D (succ-ℕ n) =
-    pointed-type-family-infinite-delooping
-      ( classifying-pointed-type-infinite-delooping D)
-      ( infinite-delooping-classifying-pointed-type-infinite-delooping D)
-      ( n)
-
-  type-family-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) → ℕ → UU l
-  type-family-infinite-delooping X D =
-    type-Pointed-Type ∘ pointed-type-family-infinite-delooping X D
-
-  pointed-equiv-family-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) (n : ℕ) →
-    pointed-type-family-infinite-delooping X D n ≃∗
-    Ω (pointed-type-family-infinite-delooping X D (succ-ℕ n))
-  pointed-equiv-family-infinite-delooping X D zero-ℕ =
-    is-delooping-infinite-delooping D
-  pointed-equiv-family-infinite-delooping X D (succ-ℕ n) =
-    pointed-equiv-family-infinite-delooping
-      ( classifying-pointed-type-infinite-delooping D)
-      ( infinite-delooping-classifying-pointed-type-infinite-delooping D)
-      ( n)
-
-  pointed-map-family-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) (n : ℕ) →
-    pointed-type-family-infinite-delooping X D n →∗
-    Ω (pointed-type-family-infinite-delooping X D (succ-ℕ n))
-  pointed-map-family-infinite-delooping X D =
-    pointed-map-pointed-equiv ∘ pointed-equiv-family-infinite-delooping X D
-
-  prespectrum-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) → Prespectrum l
-  prespectrum-infinite-delooping X D =
-    pointed-type-family-infinite-delooping X D ,
-    pointed-map-family-infinite-delooping X D
-
-  is-spectrum-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) →
-    is-spectrum (prespectrum-infinite-delooping X D)
-  is-spectrum-infinite-delooping X D =
-    is-equiv-map-pointed-equiv ∘ pointed-equiv-family-infinite-delooping X D
-
-  spectrum-infinite-delooping :
-    (X : Pointed-Type l) (D : infinite-delooping X) → Spectrum l
-  spectrum-infinite-delooping X D =
-    prespectrum-infinite-delooping X D , is-spectrum-infinite-delooping X D
-```
-
-## External links
-
-- [infinite loop space](https://ncatlab.org/nlab/show/infinite+loop+space) at
-  $n$Lab

From 8d1fcdff6b95812e6245523eec5cbb98a84d7ce0 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 21:26:52 +0200
Subject: [PATCH 05/11] linewrap

---
 src/synthetic-homotopy-theory/connective-spectra.lagda.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/connective-spectra.lagda.md b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
index 6c7cf46160..0d7d01bd35 100644
--- a/src/synthetic-homotopy-theory/connective-spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
@@ -107,7 +107,8 @@ module _
       spectrum-Connective-Spectrum
 
   is-equiv-pointed-adjoint-structure-map-Connective-Spectrum :
-    (n : ℕ) → is-pointed-equiv (pointed-adjoint-structure-map-Connective-Spectrum n)
+    (n : ℕ) →
+    is-pointed-equiv (pointed-adjoint-structure-map-Connective-Spectrum n)
   is-equiv-pointed-adjoint-structure-map-Connective-Spectrum =
     is-equiv-pointed-adjoint-structure-map-Spectrum spectrum-Connective-Spectrum
 

From 1f98efce8171f2a5a0a3785bcd648fd37bc332ee Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 4 Sep 2024 21:27:06 +0200
Subject: [PATCH 06/11] remove guardedness

---
 src/higher-group-theory.lagda.md | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/higher-group-theory.lagda.md b/src/higher-group-theory.lagda.md
index 5301e15401..e8b3202aab 100644
--- a/src/higher-group-theory.lagda.md
+++ b/src/higher-group-theory.lagda.md
@@ -1,9 +1,5 @@
 # Higher group theory
 
-```agda
-{-# OPTIONS --guardedness #-}
-```
-
 ## Files in the higher group theory folder
 
 ```agda

From 44461c20f787cacda2e03e26568f321acb7c541b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 5 Sep 2024 16:31:37 +0200
Subject: [PATCH 07/11] additions reference `BvDR18`

---
 references.bib | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/references.bib b/references.bib
index 7d87266a6f..60335786fe 100644
--- a/references.bib
+++ b/references.bib
@@ -61,7 +61,7 @@ @book{BSCS05
   langid    = {hungarian}
 }
 
-@online{BvDR18,
+@inproceedings{BvDR18,
   title       = {Higher {{Groups}} in {{Homotopy Type Theory}}},
   author      = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
   date        = {2018-02-12},
@@ -71,8 +71,15 @@ @online{BvDR18
   eprinttype  = {arxiv},
   eprintclass = {cs, math},
   abstract    = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
-  pubstate    = {preprint},
-  keywords    = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
+  isbn        = {9781450355834},
+  doi         = {10.1145/3209108.3209150},
+  pages       = {205--214},
+  numpages    = {10},
+  location    = {Oxford, United Kingdom},
+  booktitle   = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+  address     = {New York, NY, USA},
+  publisher   = {Association for Computing Machinery},
+  series      = {LICS '18}
 }
 
 @article{BW23,

From 7ea6abee89a3720d374babd676596c7317fd722e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 17 Oct 2024 12:30:12 +0200
Subject: [PATCH 08/11] wrap up

---
 .../abelian-higher-groups.lagda.md            | 28 ++++++++++++-------
 .../connective-prespectra.lagda.md            |  5 ++--
 .../connective-spectra.lagda.md               |  7 +++--
 3 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/higher-group-theory/abelian-higher-groups.lagda.md b/src/higher-group-theory/abelian-higher-groups.lagda.md
index af62b76b62..cdfe3e08ba 100644
--- a/src/higher-group-theory/abelian-higher-groups.lagda.md
+++ b/src/higher-group-theory/abelian-higher-groups.lagda.md
@@ -30,10 +30,12 @@ open import synthetic-homotopy-theory.connective-spectra
 An {{#concept "abelian" Disambiguation="∞-group"}}, or
 {{#concept "commutative" Disambiguation="∞-group"}} ∞-group is a
 [higher group](higher-group-theory.higher-groups.md) `A₀` that is commutative in
-a fully coherent way. This may be expressed by saying that there exists a
-[connective spectrum](synthetic-homotopy-theory.connective-spectra.md) such that
-the ∞-group is the first type in the sequence. I.e., there exists a sequence of
-increasingly [connected](foundation.connected-types.md) ∞-groups
+a fully coherent way. There are multiple ways to express this in Homotopy Type
+Theory. One way is to say there is a
+[connective spectrum](synthetic-homotopy-theory.connective-spectra.md) `𝒜` such
+that the ∞-group appears as the first type in the sequence. {{#cite BvDR18}}
+I.e., there exists a sequence of increasingly
+[connected](foundation.connected-types.md) ∞-groups
 
 ```text
   A₀   A₁   A₂   A₃   ⋯   Aᵢ   ⋯
@@ -50,23 +52,29 @@ that is definable in Homotopy Type Theory.
 
 ## Definitions
 
-### The predicate of being abelian with respect to a universe level
+### The connective spectrum condition of being abelian with respect to a universe level
 
 ```agda
-is-abelian-level-∞-Group :
+is-abelian-level-connective-spectrum-condition-∞-Group :
   {l : Level} (l1 : Level) → ∞-Group l → UU (l ⊔ lsuc l1)
-is-abelian-level-∞-Group l1 G =
+is-abelian-level-connective-spectrum-condition-∞-Group l1 G =
   Σ ( Connective-Spectrum l1)
     ( λ A → pointed-type-∞-Group G ≃∗ pointed-type-Connective-Spectrum A 0)
 ```
 
-### The predicate of being abelian
+### The connective spectrum condition of being abelian
 
 ```agda
-is-abelian-∞-Group : {l : Level} → ∞-Group l → UU (lsuc l)
-is-abelian-∞-Group {l} G = is-abelian-level-∞-Group l G
+is-abelian-connective-spectrum-condition-∞-Group :
+  {l : Level} → ∞-Group l → UU (lsuc l)
+is-abelian-connective-spectrum-condition-∞-Group {l} G =
+  is-abelian-level-connective-spectrum-condition-∞-Group l G
 ```
 
+## References
+
+{{#bibliography}}
+
 ## External links
 
 - [abelian infinity-group](https://ncatlab.org/nlab/show/abelian+infinity-group)
diff --git a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
index 15dbbc4559..8fd0f60ca1 100644
--- a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
@@ -32,8 +32,9 @@ open import synthetic-homotopy-theory.suspensions-of-types
 
 ## Idea
 
-A [prespectrum] is {{#concept "connective" Agda=is-connective-Prespectrum}} if
-the $n$th type in the [sequence](foundation.sequences.md) is
+A [prespectrum](synthetic-homotopy-theory.prespecra.md) is
+{{#concept "connective" Disambiguation="prespectrum" Agda=is-connective-Prespectrum}}
+if the $n$'th type in the [sequence](foundation.sequences.md) is
 $n$-[connected](foundation.connected-types.md).
 
 ### The predicate on prespectra of being connective
diff --git a/src/synthetic-homotopy-theory/connective-spectra.lagda.md b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
index 0d7d01bd35..79594a02de 100644
--- a/src/synthetic-homotopy-theory/connective-spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
@@ -34,10 +34,11 @@ open import synthetic-homotopy-theory.suspensions-of-types
 
 ## Idea
 
-A [spectrum] is {{#concept "connective" Agda=is-connective-Spectrum}} if the
-underlying [prespectrum](synthetic-homotopy-theory.prespectra.md) is
+A [spectrum](synthetic-homotopy-theory.spectra.md) is
+{{#concept "connective" Disambiguation="spectrum" Agda=is-connective-Spectrum}}
+if the underlying [prespectrum](synthetic-homotopy-theory.prespectra.md) is
 [connective](synthetic-homotopy-theory.connective-prespectra.md). I.e., if the
-$n$th type in the [sequence](foundation.sequences.md) is
+$n$'th type in the [sequence](foundation.sequences.md) is
 $n$-[connected](foundation.connected-types.md) for all $n$.
 
 ### The predicate on spectra of being connective

From 42373f4c2750b2d84d69230a3a45349bc69117ac Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 17 Oct 2024 13:43:07 +0200
Subject: [PATCH 09/11] fix link

---
 src/synthetic-homotopy-theory/connective-prespectra.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
index 8fd0f60ca1..7a3bfa2bd3 100644
--- a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
@@ -32,7 +32,7 @@ open import synthetic-homotopy-theory.suspensions-of-types
 
 ## Idea
 
-A [prespectrum](synthetic-homotopy-theory.prespecra.md) is
+A [prespectrum](synthetic-homotopy-theory.prespectra.md) is
 {{#concept "connective" Disambiguation="prespectrum" Agda=is-connective-Prespectrum}}
 if the $n$'th type in the [sequence](foundation.sequences.md) is
 $n$-[connected](foundation.connected-types.md).

From ff2fa2629f9baf2159da8d6b7e8963e6fa31c213 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 18 Oct 2024 19:37:40 +0200
Subject: [PATCH 10/11] Update
 src/synthetic-homotopy-theory/connective-prespectra.lagda.md

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
---
 src/synthetic-homotopy-theory/connective-prespectra.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
index 7a3bfa2bd3..db0ebe5577 100644
--- a/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-prespectra.lagda.md
@@ -34,7 +34,7 @@ open import synthetic-homotopy-theory.suspensions-of-types
 
 A [prespectrum](synthetic-homotopy-theory.prespectra.md) is
 {{#concept "connective" Disambiguation="prespectrum" Agda=is-connective-Prespectrum}}
-if the $n$'th type in the [sequence](foundation.sequences.md) is
+if the $n$th type in the [sequence](foundation.sequences.md) is
 $n$-[connected](foundation.connected-types.md).
 
 ### The predicate on prespectra of being connective

From c3846453c64307bc7daf7591ebd503339400e980 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 18 Oct 2024 19:37:47 +0200
Subject: [PATCH 11/11] Update
 src/synthetic-homotopy-theory/connective-spectra.lagda.md

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
---
 src/synthetic-homotopy-theory/connective-spectra.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/connective-spectra.lagda.md b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
index 79594a02de..939ec9243c 100644
--- a/src/synthetic-homotopy-theory/connective-spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/connective-spectra.lagda.md
@@ -38,7 +38,7 @@ A [spectrum](synthetic-homotopy-theory.spectra.md) is
 {{#concept "connective" Disambiguation="spectrum" Agda=is-connective-Spectrum}}
 if the underlying [prespectrum](synthetic-homotopy-theory.prespectra.md) is
 [connective](synthetic-homotopy-theory.connective-prespectra.md). I.e., if the
-$n$'th type in the [sequence](foundation.sequences.md) is
+$n$th type in the [sequence](foundation.sequences.md) is
 $n$-[connected](foundation.connected-types.md) for all $n$.
 
 ### The predicate on spectra of being connective