diff --git a/config/codespell-dictionary.txt b/config/codespell-dictionary.txt
index 42eb42d013..7ebfe3a5ca 100644
--- a/config/codespell-dictionary.txt
+++ b/config/codespell-dictionary.txt
@@ -31,6 +31,7 @@ conisistsed->consisted
 conisistsing->consisting
 consistsed->consisted
 consistsing->consisting
+diamgram->diagram
 eacy->each,easy
 embeddding->embedding
 embedddings->embeddings
@@ -58,6 +59,7 @@ homomorphsim->homomorphism
 homomorphsims->homomorphisms
 identitification->identification
 identitifications->identifications
+inhanited->inhabited
 isomorhpism->isomorphism
 isomorhpisms->isomorphisms
 isomorhpsim->isomorphism
diff --git a/docs/tables/loop-spaces-concepts.md b/docs/tables/loop-spaces-concepts.md
index 3060bb5827..b08f5be7e4 100644
--- a/docs/tables/loop-spaces-concepts.md
+++ b/docs/tables/loop-spaces-concepts.md
@@ -8,5 +8,6 @@
 | Functoriality of loop spaces | [`synthetic-homotopy-theory.functoriality-loop-spaces`](synthetic-homotopy-theory.functoriality-loop-spaces.md)   |
 | Groups of loops in 1-types   | [`synthetic-homotopy-theory.groups-of-loops-in-1-types`](synthetic-homotopy-theory.groups-of-loops-in-1-types.md) |
 | Iterated loop spaces         | [`synthetic-homotopy-theory.iterated-loop-spaces`](synthetic-homotopy-theory.iterated-loop-spaces.md)             |
+| Multivariable loop spaces    | [`synthetic-homotopy-theory.multivariable-loop-spaces`](synthetic-homotopy-theory.multivariable-loop-spaces.md)   |
 | Powers of loops              | [`synthetic-homotopy-theory.powers-of-loops`](synthetic-homotopy-theory.powers-of-loops.md)                       |
 | Triple loop spaces           | [`synthetic-homotopy-theory.triple-loop-spaces`](synthetic-homotopy-theory.triple-loop-spaces.md)                 |
diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md
index dc561cf951..678b3cb60e 100644
--- a/src/structured-types.lagda.md
+++ b/src/structured-types.lagda.md
@@ -39,6 +39,7 @@ open import structured-types.involutive-type-of-h-space-structures public
 open import structured-types.involutive-types public
 open import structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms public
 open import structured-types.iterated-pointed-cartesian-product-types public
+open import structured-types.left-invertible-magmas public
 open import structured-types.magmas public
 open import structured-types.medial-magmas public
 open import structured-types.mere-equivalences-types-equipped-with-endomorphisms public
diff --git a/src/structured-types/left-invertible-magmas.lagda.md b/src/structured-types/left-invertible-magmas.lagda.md
new file mode 100644
index 0000000000..de0a6427b2
--- /dev/null
+++ b/src/structured-types/left-invertible-magmas.lagda.md
@@ -0,0 +1,52 @@
+# Left-invertible magmas
+
+```agda
+module structured-types.left-invertible-magmas where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import structured-types.magmas
+```
+
+</details>
+
+## Idea
+
+A [magma](structured-types.magmas.md) `A` is
+{{#concept "left-invertible" Disambiguation="magma" Agda=is-left-invertible-Magma}}
+if the multiplication map `μ(a,-) : A → A` is an
+[equivalence](foundation-core.equivalences.md) for every `a : A`. In other
+words, if multiplying by a fixed element on the left is always an equivalence.
+
+Left-invertibility appears as Definition 2.1(4) of {{#cite BCFR23}} in the
+context of [H-spaces](structured-types.h-spaces.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level} (A : Magma l)
+  where
+
+  is-left-invertible-Magma : UU l
+  is-left-invertible-Magma = (a : type-Magma A) → is-equiv (mul-Magma A a)
+
+  is-prop-is-left-invertible-Magma : is-prop is-left-invertible-Magma
+  is-prop-is-left-invertible-Magma =
+    is-prop-Π (λ a → is-property-is-equiv (mul-Magma A a))
+
+  is-left-invertible-prop-Magma : Prop l
+  is-left-invertible-prop-Magma =
+    ( is-left-invertible-Magma , is-prop-is-left-invertible-Magma)
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/structured-types/pointed-maps.lagda.md b/src/structured-types/pointed-maps.lagda.md
index 721206c4bf..15eaa85f3d 100644
--- a/src/structured-types/pointed-maps.lagda.md
+++ b/src/structured-types/pointed-maps.lagda.md
@@ -14,6 +14,8 @@ open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import structured-types.pointed-dependent-functions
@@ -140,6 +142,21 @@ module _
   pr2 id-pointed-map = refl
 ```
 
+### Truncatedness of the type of pointed maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  where abstract
+
+  is-trunc-pointed-function-type :
+    (k : 𝕋) → is-trunc k (type-Pointed-Type B) → is-trunc k (pointed-map A B)
+  is-trunc-pointed-function-type k H =
+    is-trunc-Σ
+      ( is-trunc-function-type k H)
+      ( λ f → is-trunc-Id H (f (point-Pointed-Type A)) (point-Pointed-Type B))
+```
+
 ## See also
 
 - [Constant pointed maps](structured-types.constant-pointed-maps.md)
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 2839f2a816..500f6ef66e 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -102,6 +102,7 @@ open import synthetic-homotopy-theory.morphisms-descent-data-circle public
 open import synthetic-homotopy-theory.morphisms-descent-data-pushouts public
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams public
 open import synthetic-homotopy-theory.multiplication-circle public
+open import synthetic-homotopy-theory.multivariable-loop-spaces public
 open import synthetic-homotopy-theory.null-cocones-under-pointed-span-diagrams public
 open import synthetic-homotopy-theory.plus-principle public
 open import synthetic-homotopy-theory.powers-of-loops public
diff --git a/src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md b/src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md
index 09fde243e6..fbe2b953f5 100644
--- a/src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md
@@ -68,6 +68,12 @@ module _
     universal-property-pushout f (terminal-map A) cocone-cofiber
   universal-property-cofiber = up-pushout f (terminal-map A)
 
+  equiv-up-cofiber :
+    {l : Level} (X : UU l) → (cofiber → X) ≃ cocone f (terminal-map A) X
+  equiv-up-cofiber X =
+    ( cocone-map f (terminal-map A) cocone-cofiber ,
+      universal-property-cofiber X)
+
   dependent-universal-property-cofiber :
     dependent-universal-property-pushout f (terminal-map A) cocone-cofiber
   dependent-universal-property-cofiber = dup-pushout f (terminal-map A)
@@ -76,6 +82,11 @@ module _
     {l : Level} {X : UU l} → cocone f (terminal-map A) X → cofiber → X
   cogap-cofiber = cogap f (terminal-map A)
 
+  equiv-cogap-cofiber :
+    {l : Level} (X : UU l) → cocone f (terminal-map A) X ≃ (cofiber → X)
+  equiv-cogap-cofiber X =
+    ( cogap-cofiber , is-equiv-map-inv-is-equiv (universal-property-cofiber X))
+
   dependent-cogap-cofiber :
     {l : Level} {P : cofiber → UU l}
     (c : dependent-cocone f (terminal-map A) (cocone-cofiber) P)
diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md
new file mode 100644
index 0000000000..f70aa3511f
--- /dev/null
+++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md
@@ -0,0 +1,711 @@
+# Multivariable loop spaces
+
+```agda
+module synthetic-homotopy-theory.multivariable-loop-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.commuting-triangles-of-identifications
+open import foundation.constant-maps
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.path-algebra
+open import foundation.propositional-truncations
+open import foundation.retractions
+open import foundation.sections
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.type-arithmetic-cartesian-product-types
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.unit-type
+open import foundation.universal-property-empty-type
+open import foundation.universal-property-maybe
+open import foundation.universe-levels
+
+open import structured-types.h-spaces
+open import structured-types.left-invertible-magmas
+open import structured-types.magmas
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-homotopies
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.cavallos-trick
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.suspensions-of-types
+```
+
+</details>
+
+## Idea
+
+Given a type `I` and a [pointed type](structured-types.pointed-types.md)
+`a∗ : A`, we can form the {{#concept "`I`-ary loop space" Agda=multivar-Ω}} in
+`A` as the type `Σ (a : A), (I → (a ＝ a∗))`. This type is canonically pointed
+at `(a∗ , refl-htpy)`. We recover the
+[standard loop space](synthetic-homotopy-theory.loop-spaces.md) `ΩA` as the
+`1+1`-ary loops, there is a unique `1`-ary loop, and we recover `A` itself as
+the `∅`-loops. The `𝕊¹`-ary loops correspond to
+[loops of loops](synthetic-homotopy-theory.double-loop-spaces.md). Observe that
+among pointed types `1+1` represents elements, and so we should interpret
+`1+1`-ary as _unary_ loops rather than binary ones, which is consistent with the
+fact that `1+1`-ary loops yields the standard loops.
+
+For every point `x` of `I` there is a coherent, associative, and invertible
+[H-space structure](structured-types.h-spaces.md) on `I`-ary loops, and moreover
+any point `x` of `I` gives a
+[pointed equivalence](structured-types.pointed-equivalences.md) between `I`-ary
+loops of `A` and `(I,x) →∗ ΩA`.
+
+## Table of files directly related to loop spaces
+
+{{#include tables/loop-spaces-concepts.md}}
+
+## Definitions
+
+### The `I`-ary loop space
+
+```agda
+module _
+  {l1 l2 : Level} (I : UU l1) (A∗ : Pointed-Type l2)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  type-multivar-Ω : UU (l1 ⊔ l2)
+  type-multivar-Ω = Σ A (λ a → I → a ＝ a∗)
+
+  refl-multivar-Ω : type-multivar-Ω
+  refl-multivar-Ω = (a∗ , refl-htpy)
+
+  multivar-Ω : Pointed-Type (l1 ⊔ l2)
+  multivar-Ω = (type-multivar-Ω , refl-multivar-Ω)
+```
+
+## Properties
+
+### Characterizing equality in `I`-ary loop spaces
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2}
+  where
+
+  Eq-multivar-Ω : (x y : type-multivar-Ω I A∗) → UU (l1 ⊔ l2)
+  Eq-multivar-Ω (a , p) (b , q) =
+    Σ ( a ＝ b)
+      ( λ r → (i : I) → coherence-triangle-identifications (p i) (q i) r)
+
+  refl-Eq-multivar-Ω : (x : type-multivar-Ω I A∗) → Eq-multivar-Ω x x
+  refl-Eq-multivar-Ω p = (refl , refl-htpy)
+
+  Eq-eq-multivar-Ω :
+    (x y : type-multivar-Ω I A∗) → x ＝ y → Eq-multivar-Ω x y
+  Eq-eq-multivar-Ω x .x refl = refl-Eq-multivar-Ω x
+
+  abstract
+    is-torsorial-Eq-multivar-Ω :
+      (x : type-multivar-Ω I A∗) → is-torsorial (Eq-multivar-Ω x)
+    is-torsorial-Eq-multivar-Ω (a , p) =
+      is-torsorial-Eq-structure
+        ( is-torsorial-Id a)
+        ( a , refl)
+        ( is-torsorial-htpy p)
+
+  is-equiv-Eq-eq-multivar-Ω :
+    (x y : type-multivar-Ω I A∗) → is-equiv (Eq-eq-multivar-Ω x y)
+  is-equiv-Eq-eq-multivar-Ω x =
+    fundamental-theorem-id (is-torsorial-Eq-multivar-Ω x) (Eq-eq-multivar-Ω x)
+
+  extensionality-multivar-Ω :
+    (x y : type-multivar-Ω I A∗) → (x ＝ y) ≃ Eq-multivar-Ω x y
+  extensionality-multivar-Ω x y =
+    ( Eq-eq-multivar-Ω x y , is-equiv-Eq-eq-multivar-Ω x y)
+
+  eq-Eq-multivar-Ω :
+    (x y : type-multivar-Ω I A∗) → Eq-multivar-Ω x y → x ＝ y
+  eq-Eq-multivar-Ω x y =
+    map-inv-equiv (extensionality-multivar-Ω x y)
+```
+
+### Characterizing equality of equality in `I`-ary loop spaces
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2}
+  (x y : type-multivar-Ω I A∗)
+  where
+
+  Eq²-multivar-Ω :
+    (p q : Eq-multivar-Ω x y) → UU (l1 ⊔ l2)
+  Eq²-multivar-Ω (p , H) (q , K) =
+    Σ (p ＝ q) (λ r → (i : I) → H i ∙ ap (_∙ pr2 y i) r ＝ K i)
+
+  refl-Eq²-multivar-Ω :
+    (p : Eq-multivar-Ω x y) → Eq²-multivar-Ω p p
+  refl-Eq²-multivar-Ω p = (refl , right-unit-htpy)
+
+  Eq²-eq-multivar-Ω :
+    (p q : Eq-multivar-Ω x y) → p ＝ q → Eq²-multivar-Ω p q
+  Eq²-eq-multivar-Ω p .p refl = refl-Eq²-multivar-Ω p
+
+  abstract
+    is-torsorial-Eq²-multivar-Ω :
+      (p : Eq-multivar-Ω x y) → is-torsorial (Eq²-multivar-Ω p)
+    is-torsorial-Eq²-multivar-Ω (a , p) =
+      is-torsorial-Eq-structure
+        ( is-torsorial-Id a)
+        ( a , refl)
+        ( is-torsorial-htpy (p ∙h refl-htpy))
+
+  is-equiv-Eq²-eq-multivar-Ω :
+    (p q : Eq-multivar-Ω x y) → is-equiv (Eq²-eq-multivar-Ω p q)
+  is-equiv-Eq²-eq-multivar-Ω p =
+    fundamental-theorem-id
+      ( is-torsorial-Eq²-multivar-Ω p)
+      ( Eq²-eq-multivar-Ω p)
+
+  extensionality²-multivar-Ω :
+    (p q : Eq-multivar-Ω x y) → (p ＝ q) ≃ Eq²-multivar-Ω p q
+  extensionality²-multivar-Ω p q =
+    ( Eq²-eq-multivar-Ω p q , is-equiv-Eq²-eq-multivar-Ω p q)
+
+  eq-Eq²-multivar-Ω :
+    (p q : Eq-multivar-Ω x y) → Eq²-multivar-Ω p q → p ＝ q
+  eq-Eq²-multivar-Ω p q =
+    map-inv-equiv (extensionality²-multivar-Ω p q)
+```
+
+### The `I`-ary loops over a pointed type forms a magma
+
+```agda
+module _
+  {l1 l2 : Level} (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗) (let i∗ = point-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  mul-multivar-Ω :
+    type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗
+  mul-multivar-Ω (a , p) (b , q) = (a , (λ x → p x ∙ inv (q i∗) ∙ q x))
+
+  multivar-Ω-Magma : Magma (l1 ⊔ l2)
+  multivar-Ω-Magma = (type-multivar-Ω I A∗ , mul-multivar-Ω)
+```
+
+### The coherent H-space of `I`-ary loops, for pointed `I`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗) (let i∗ = point-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  Eq-left-unit-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    Eq-multivar-Ω (mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x) x
+  Eq-left-unit-law-mul-multivar-Ω (a , p) = (inv (p i∗) , refl-htpy)
+
+  left-unit-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x ＝ x
+  left-unit-law-mul-multivar-Ω x =
+    eq-Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x)
+      ( x)
+      ( Eq-left-unit-law-mul-multivar-Ω x)
+
+  Eq-right-unit-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    Eq-multivar-Ω (mul-multivar-Ω I∗ A∗ x (refl-multivar-Ω I A∗)) x
+  Eq-right-unit-law-mul-multivar-Ω x =
+    ( refl , right-unit-htpy ∙h right-unit-htpy)
+
+  right-unit-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    mul-multivar-Ω I∗ A∗ x (refl-multivar-Ω I A∗) ＝ x
+  right-unit-law-mul-multivar-Ω x =
+    eq-Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ x (refl-multivar-Ω I A∗))
+      ( x)
+      ( Eq-right-unit-law-mul-multivar-Ω x)
+
+  Eq-coherence-unit-laws-mul-multivar-Ω :
+    Eq²-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) (refl-multivar-Ω I A∗))
+      ( refl-multivar-Ω I A∗)
+      ( Eq-left-unit-law-mul-multivar-Ω (refl-multivar-Ω I A∗))
+      ( Eq-right-unit-law-mul-multivar-Ω (refl-multivar-Ω I A∗))
+  Eq-coherence-unit-laws-mul-multivar-Ω =
+    ( refl , refl-htpy)
+
+  coherence-unit-laws-mul-multivar-Ω :
+    left-unit-law-mul-multivar-Ω (refl-multivar-Ω I A∗) ＝
+    right-unit-law-mul-multivar-Ω (refl-multivar-Ω I A∗)
+  coherence-unit-laws-mul-multivar-Ω = refl
+
+  multivar-Ω-H-Space : H-Space (l1 ⊔ l2)
+  multivar-Ω-H-Space =
+    ( multivar-Ω I A∗ ,
+      mul-multivar-Ω I∗ A∗ ,
+      left-unit-law-mul-multivar-Ω ,
+      right-unit-law-mul-multivar-Ω ,
+      coherence-unit-laws-mul-multivar-Ω)
+```
+
+### Associativity of multiplication
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗) (let i∗ = point-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  Eq-associative-mul-multivar-Ω :
+    (x y z : type-multivar-Ω I A∗) →
+    Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ x y) z)
+      ( mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ y z))
+  pr1 (Eq-associative-mul-multivar-Ω (a , p) (b , q) (c , r)) = refl
+  pr2 (Eq-associative-mul-multivar-Ω (a , p) (b , q) (c , r)) x =
+    equational-reasoning
+      (((p x ∙ inv (q i∗)) ∙ q x) ∙ inv (r i∗)) ∙ r x
+      ＝ (p x ∙ inv (q i∗)) ∙ ((q x ∙ inv (r i∗)) ∙ r x)
+        by
+        assoc²-1 (p x ∙ inv (q i∗)) (q x) (inv (r i∗)) (r x)
+      ＝ (p x ∙ inv ((q i∗ ∙ inv (r i∗)) ∙ r i∗)) ∙ ((q x ∙ inv (r i∗)) ∙ r x)
+        by
+        ap
+          ( λ u → (p x ∙ inv u) ∙ (q x ∙ inv (r i∗) ∙ r x))
+          ( inv (is-section-inv-concat' (r i∗) (q i∗)))
+
+  associative-mul-multivar-Ω :
+    (x y z : type-multivar-Ω I A∗) →
+    mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ x y) z ＝
+    mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ y z)
+  associative-mul-multivar-Ω x y z =
+    eq-Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ x y) z)
+      ( mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ y z))
+      ( Eq-associative-mul-multivar-Ω x y z)
+```
+
+### The multiplicative inverse
+
+Given `i∗ : I` and `a∗ : A`, then any `I`-ary loop `(a , p)` has a
+multiplicative inverse given by `(a∗ , (i ↦ (p i)⁻¹ ∙ p i∗)`.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗) (let i∗ = point-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  inv-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗
+  inv-multivar-Ω (a , p) = (a∗ , (λ i → inv (p i) ∙ p i∗))
+
+  Eq-right-inverse-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x))
+      ( refl-multivar-Ω I A∗)
+  pr1 (Eq-right-inverse-law-mul-multivar-Ω (a , p)) = p i∗
+  pr2 (Eq-right-inverse-law-mul-multivar-Ω (a , p)) x =
+    equational-reasoning
+      (p x ∙ inv (inv (p i∗) ∙ p i∗)) ∙ (inv (p x) ∙ p i∗)
+      ＝ p x ∙ (inv (p x) ∙ p i∗)
+        by
+        ap
+          ( _∙ (inv (p x) ∙ p i∗))
+          ( ap (p x ∙_) (ap inv (left-inv (p i∗))) ∙ right-unit)
+      ＝ p i∗
+        by is-section-inv-concat (p x) (p i∗)
+      ＝ p i∗ ∙ refl
+        by inv right-unit
+
+  right-inverse-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x) ＝
+    refl-multivar-Ω I A∗
+  right-inverse-law-mul-multivar-Ω x =
+    eq-Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x))
+      ( refl-multivar-Ω I A∗)
+      ( Eq-right-inverse-law-mul-multivar-Ω x)
+
+  Eq-left-inverse-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x)
+      ( refl-multivar-Ω I A∗)
+  pr1 (Eq-left-inverse-law-mul-multivar-Ω (a , p)) = refl
+  pr2 (Eq-left-inverse-law-mul-multivar-Ω (a , p)) i =
+    equational-reasoning
+      ((inv (p i) ∙ p i∗) ∙ inv (p i∗)) ∙ p i
+      ＝ inv (p i) ∙ p i
+        by ap (_∙ p i) (is-retraction-inv-concat' (p i∗) (inv (p i)))
+      ＝ refl by left-inv (p i)
+
+  left-inverse-law-mul-multivar-Ω :
+    (x : type-multivar-Ω I A∗) →
+    mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x ＝
+    refl-multivar-Ω I A∗
+  left-inverse-law-mul-multivar-Ω x =
+    eq-Eq-multivar-Ω
+      ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x)
+      ( refl-multivar-Ω I A∗)
+      ( Eq-left-inverse-law-mul-multivar-Ω x)
+```
+
+### Invertibility of left and right multiplication
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗)
+  where
+
+  left-mul-inv-multivar-Ω :
+    type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗
+  left-mul-inv-multivar-Ω a =
+    mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a)
+
+  is-section-left-mul-inv-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    is-section (mul-multivar-Ω I∗ A∗ a) (left-mul-inv-multivar-Ω a)
+  is-section-left-mul-inv-multivar-Ω a x =
+    equational-reasoning
+      mul-multivar-Ω I∗ A∗ a (mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) x)
+      ＝ mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ a (inv-multivar-Ω I∗ A∗ a)) x
+        by inv (associative-mul-multivar-Ω I∗ A∗ a (inv-multivar-Ω I∗ A∗ a) x)
+      ＝ mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x
+        by
+        ap
+          ( λ u → mul-multivar-Ω I∗ A∗ u x)
+          ( right-inverse-law-mul-multivar-Ω I∗ A∗ a)
+      ＝ x
+        by left-unit-law-mul-multivar-Ω I∗ A∗ x
+
+  is-retraction-left-mul-inv-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    is-retraction (mul-multivar-Ω I∗ A∗ a) (left-mul-inv-multivar-Ω a)
+  is-retraction-left-mul-inv-multivar-Ω a x =
+    equational-reasoning
+      mul-multivar-Ω I∗ A∗
+        ( inv-multivar-Ω I∗ A∗ a)
+        ( mul-multivar-Ω I∗ A∗ a x)
+      ＝ mul-multivar-Ω I∗ A∗
+          ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) a)
+          ( x)
+        by
+        inv (associative-mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) a x)
+      ＝ mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x
+        by
+        ap
+          ( λ u → mul-multivar-Ω I∗ A∗ u x)
+          ( left-inverse-law-mul-multivar-Ω I∗ A∗ a)
+      ＝ x by left-unit-law-mul-multivar-Ω I∗ A∗ x
+
+  section-left-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) → section (mul-multivar-Ω I∗ A∗ a)
+  section-left-mul-multivar-Ω a =
+    ( left-mul-inv-multivar-Ω a ,
+      is-section-left-mul-inv-multivar-Ω a)
+
+  retraction-left-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) → retraction (mul-multivar-Ω I∗ A∗ a)
+  retraction-left-mul-multivar-Ω a =
+    ( left-mul-inv-multivar-Ω a ,
+      is-retraction-left-mul-inv-multivar-Ω a)
+
+  is-equiv-left-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) → is-equiv (mul-multivar-Ω I∗ A∗ a)
+  is-equiv-left-mul-multivar-Ω a =
+    is-equiv-is-invertible
+      ( left-mul-inv-multivar-Ω a)
+      ( is-section-left-mul-inv-multivar-Ω a)
+      ( is-retraction-left-mul-inv-multivar-Ω a)
+
+  equiv-left-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) → type-multivar-Ω I A∗ ≃ type-multivar-Ω I A∗
+  equiv-left-mul-multivar-Ω a =
+    ( mul-multivar-Ω I∗ A∗ a , is-equiv-left-mul-multivar-Ω a)
+
+  is-left-invertible-mul-multivar-Ω :
+    is-left-invertible-Magma (multivar-Ω-Magma I∗ A∗)
+  is-left-invertible-mul-multivar-Ω = is-equiv-left-mul-multivar-Ω
+```
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗)
+  where
+
+  right-mul-inv-multivar-Ω :
+    type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗
+  right-mul-inv-multivar-Ω a x =
+    mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a)
+
+  is-section-right-mul-inv-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    is-section
+      ( λ x → mul-multivar-Ω I∗ A∗ x a)
+      ( right-mul-inv-multivar-Ω a)
+  is-section-right-mul-inv-multivar-Ω a x =
+    equational-reasoning
+      mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a)) a
+      ＝ mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) a)
+        by associative-mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a) a
+      ＝ mul-multivar-Ω I∗ A∗ x (refl-multivar-Ω I A∗)
+        by ap (mul-multivar-Ω I∗ A∗ x) (left-inverse-law-mul-multivar-Ω I∗ A∗ a)
+      ＝ x
+        by right-unit-law-mul-multivar-Ω I∗ A∗ x
+
+  is-retraction-right-mul-inv-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    is-retraction
+      ( λ x → mul-multivar-Ω I∗ A∗ x a)
+      ( right-mul-inv-multivar-Ω a)
+  is-retraction-right-mul-inv-multivar-Ω a x =
+    equational-reasoning
+      mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ x a) (inv-multivar-Ω I∗ A∗ a)
+      ＝ mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ a (inv-multivar-Ω I∗ A∗ a))
+        by associative-mul-multivar-Ω I∗ A∗ x a (inv-multivar-Ω I∗ A∗ a)
+      ＝ mul-multivar-Ω I∗ A∗ x (refl-multivar-Ω I A∗)
+        by
+        ap (mul-multivar-Ω I∗ A∗ x) (right-inverse-law-mul-multivar-Ω I∗ A∗ a)
+      ＝ x
+        by right-unit-law-mul-multivar-Ω I∗ A∗ x
+
+  section-right-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    section (λ x → mul-multivar-Ω I∗ A∗ x a)
+  section-right-mul-multivar-Ω a =
+    ( right-mul-inv-multivar-Ω a ,
+      is-section-right-mul-inv-multivar-Ω a)
+
+  retraction-right-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    retraction (λ x → mul-multivar-Ω I∗ A∗ x a)
+  retraction-right-mul-multivar-Ω a =
+    ( right-mul-inv-multivar-Ω a ,
+      is-retraction-right-mul-inv-multivar-Ω a)
+
+  is-equiv-right-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) →
+    is-equiv (λ x → mul-multivar-Ω I∗ A∗ x a)
+  is-equiv-right-mul-multivar-Ω a =
+    is-equiv-is-invertible
+      ( right-mul-inv-multivar-Ω a)
+      ( is-section-right-mul-inv-multivar-Ω a)
+      ( is-retraction-right-mul-inv-multivar-Ω a)
+
+  equiv-right-mul-multivar-Ω :
+    (a : type-multivar-Ω I A∗) → type-multivar-Ω I A∗ ≃ type-multivar-Ω I A∗
+  equiv-right-mul-multivar-Ω a =
+    ((λ x → mul-multivar-Ω I∗ A∗ x a) , is-equiv-right-mul-multivar-Ω a)
+```
+
+### If `I` is pointed then `I`-ary loops are pointed equivalent to pointed maps `I →∗ ΩA`
+
+First we demonstrate the equivalence directly as a composite of simple
+equivalences, then we construct the explicit map and demonstrate that it is also
+pointed.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (I∗ : Pointed-Type l1) (A∗ : Pointed-Type l2)
+  (let I = type-Pointed-Type I∗) (let i∗ = point-Pointed-Type I∗)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  abstract
+    compute-type-multivar-Ω-pointed' :
+      type-multivar-Ω I A∗ ≃ (I∗ →∗ Ω A∗)
+    compute-type-multivar-Ω-pointed' =
+      equivalence-reasoning
+        Σ A (λ a → I → a ＝ a∗)
+        ≃ Σ A (λ a → Σ (I → a ＝ a∗) (λ f → Σ (a ＝ a∗) (f i∗ ＝_)))
+          by
+          equiv-tot
+            ( λ a →
+              inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-Id (f i∗)))
+        ≃ Σ (Σ A (_＝ a∗)) (λ (a , p) → Σ (I → a ＝ a∗) (λ a → a i∗ ＝ p))
+          by inv-associative-Σ ∘e equiv-tot (λ a → equiv-left-swap-Σ)
+        ≃ Σ (I → a∗ ＝ a∗) (λ f → f i∗ ＝ refl)
+          by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl)
+
+  map-compute-multivar-Ω-pointed :
+    type-multivar-Ω I A∗ → (I∗ →∗ Ω A∗)
+  map-compute-multivar-Ω-pointed (a , p) =
+    ( (λ i → inv (p i∗) ∙ p i) , left-inv (p i∗))
+
+  map-inv-compute-multivar-Ω-pointed :
+    (I∗ →∗ Ω A∗) → type-multivar-Ω I A∗
+  map-inv-compute-multivar-Ω-pointed (f , p) = (a∗ , f)
+
+  is-section-map-inv-compute-multivar-Ω-pointed :
+    is-section map-compute-multivar-Ω-pointed map-inv-compute-multivar-Ω-pointed
+  is-section-map-inv-compute-multivar-Ω-pointed (f , p) =
+    eq-pointed-htpy _ _
+      ( cavallos-trick-H-Space' I∗ (Ω-H-Space A∗) _ _
+        ( λ x → ap (λ u → inv u ∙ f x) p))
+
+  is-retraction-map-inv-compute-multivar-Ω-pointed :
+    is-retraction
+      ( map-compute-multivar-Ω-pointed)
+      ( map-inv-compute-multivar-Ω-pointed)
+  is-retraction-map-inv-compute-multivar-Ω-pointed (a , p) =
+    eq-Eq-multivar-Ω _ _ (inv (p i∗) , refl-htpy)
+
+  preserves-point-map-compute-multivar-Ω-pointed :
+    map-compute-multivar-Ω-pointed (refl-multivar-Ω I A∗) ＝
+    ( const I (refl-Ω A∗) , refl)
+  preserves-point-map-compute-multivar-Ω-pointed = refl
+
+  is-equiv-map-compute-multivar-Ω-pointed :
+    is-equiv map-compute-multivar-Ω-pointed
+  is-equiv-map-compute-multivar-Ω-pointed =
+    is-equiv-is-invertible
+      ( map-inv-compute-multivar-Ω-pointed)
+      ( is-section-map-inv-compute-multivar-Ω-pointed)
+      ( is-retraction-map-inv-compute-multivar-Ω-pointed)
+
+  compute-type-multivar-Ω-pointed :
+    type-multivar-Ω I A∗ ≃ (I∗ →∗ Ω A∗)
+  compute-type-multivar-Ω-pointed =
+    ( map-compute-multivar-Ω-pointed ,
+      is-equiv-map-compute-multivar-Ω-pointed)
+
+  compute-multivar-Ω-pointed :
+    multivar-Ω I A∗ ≃∗ (I∗ →∗ Ω A∗ , (const I (refl-Ω A∗) , refl))
+  compute-multivar-Ω-pointed =
+    ( compute-type-multivar-Ω-pointed ,
+      preserves-point-map-compute-multivar-Ω-pointed)
+```
+
+### ∅-ary loops
+
+```agda
+module _
+  {l : Level} (A∗ : Pointed-Type l)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  compute-type-multivar-Ω-empty : type-multivar-Ω empty A∗ ≃ A
+  compute-type-multivar-Ω-empty =
+    right-unit-law-Σ-is-contr (λ a → universal-property-empty' (a ＝ a∗))
+
+  preserves-point-map-compute-multivar-Ω-empty :
+    map-equiv compute-type-multivar-Ω-empty (refl-multivar-Ω empty A∗) ＝ a∗
+  preserves-point-map-compute-multivar-Ω-empty = refl
+
+  compute-multivar-Ω-empty : multivar-Ω empty A∗ ≃∗ A∗
+  pr1 compute-multivar-Ω-empty = compute-type-multivar-Ω-empty
+  pr2 compute-multivar-Ω-empty = preserves-point-map-compute-multivar-Ω-empty
+```
+
+### `I+1`-ary loops
+
+`(I + 1)`-ary loops are equivalent to families of loops `I → ΩA`, where `Ω` is
+the standard loop type.
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} (A∗ : Pointed-Type l2)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  compute-type-multivar-Ω-isolated-point :
+    type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗)
+  compute-type-multivar-Ω-isolated-point =
+    equivalence-reasoning
+      Σ A (λ a → I + unit → a ＝ a∗)
+      ≃ Σ A (λ a → (I → a ＝ a∗) × (a ＝ a∗))
+        by equiv-tot (λ a → equiv-universal-property-Maybe)
+      ≃ Σ A (λ a → (a ＝ a∗) × (I → a ＝ a∗))
+        by equiv-tot (λ a → commutative-product)
+      ≃ Σ (Σ A (λ a → (a ＝ a∗))) (λ u → (I → pr1 u ＝ a∗))
+        by inv-associative-Σ
+      ≃ (I → type-Ω A∗)
+        by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl)
+```
+
+### `ΣI`-ary loops are `I`-ary loops of loops
+
+For every type $I$ we have an equivalence
+
+$$Ω_{ΣI}(A) ≃ Ω_I(Ω(A))$$
+
+where $ΣI$ denotes the
+[suspension](synthetic-homotopy-theory.suspensions-of-types.md) of $I$.
+
+```agda
+module _
+  {l1 l2 : Level} (I : UU l1) (A∗ : Pointed-Type l2)
+  (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗)
+  where
+
+  compute-type-multivar-Ω-suspension :
+    type-multivar-Ω (suspension I) A∗ ≃ type-multivar-Ω I (Ω A∗)
+  compute-type-multivar-Ω-suspension =
+    equivalence-reasoning
+      Σ A (λ a → suspension I → a ＝ a∗)
+      ≃ Σ A (λ a → Σ (a ＝ a∗) (λ S → Σ (a ＝ a∗) (λ N → I → N ＝ S)))
+        by equiv-tot (λ a → equiv-left-swap-Σ ∘e equiv-up-suspension)
+      ≃ Σ (Σ A (λ a → a ＝ a∗)) (λ (a , S) → Σ (a ＝ a∗) (λ N → I → N ＝ S))
+        by inv-associative-Σ
+      ≃ Σ (a∗ ＝ a∗) (λ N → I → N ＝ refl)
+        by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl-Ω A∗)
+```
+
+### Truncatedness of `I`-ary loops
+
+```agda
+module _
+  {l1 l2 : Level} (I : UU l1) (A∗ : Pointed-Type l2)
+  where abstract
+
+  is-trunc-type-multivar-Ω-has-element :
+    (k : 𝕋) → I → is-trunc (succ-𝕋 k) (type-Pointed-Type A∗) →
+    is-trunc k (type-multivar-Ω I A∗)
+  is-trunc-type-multivar-Ω-has-element k i∗ K =
+    is-trunc-equiv k ((I , i∗) →∗ Ω A∗)
+      ( compute-type-multivar-Ω-pointed (I , i∗) A∗)
+      ( is-trunc-pointed-function-type k
+        ( K (point-Pointed-Type A∗) (point-Pointed-Type A∗)))
+
+  is-trunc-type-multivar-Ω-is-inhabited :
+    (k : 𝕋) → is-inhabited I → is-trunc (succ-𝕋 k) (type-Pointed-Type A∗) →
+    is-trunc k (type-multivar-Ω I A∗)
+  is-trunc-type-multivar-Ω-is-inhabited k H K =
+    rec-trunc-Prop
+      ( is-trunc-Prop k (type-multivar-Ω I A∗))
+      ( λ i∗ → is-trunc-type-multivar-Ω-has-element k i∗ K)
+      ( H)
+```