Multivariable loop spaces
Content created by Fredrik Bakke.
Created on 2026-05-05.
Last modified on 2026-05-05.
module synthetic-homotopy-theory.multivariable-loop-spaces where
Imports
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.subuniverse-of-truncated-types 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
Idea
Given a type I and a pointed type
a∗ : A, we can form the I-ary loop space¶
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 Ω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. 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 on I-ary loops, and moreover
any point x of I gives a
pointed equivalence between I-ary
loops of A and (I,x) →∗ ΩA.
Table of files directly related to loop spaces
| Concept | File |
|---|---|
| Higher groups | higher-group-theory.higher-groups |
| Conjugation of loops | synthetic-homotopy-theory.conjugation-loops |
| Double loop spaces | synthetic-homotopy-theory.double-loop-spaces |
| The Eckmann-Hilton argument | synthetic-homotopy-theory.eckmann-hilton-argument |
| Free loops | synthetic-homotopy-theory.free-loops |
| Functoriality of loop spaces | synthetic-homotopy-theory.functoriality-loop-spaces |
| Groups of loops in 1-types | synthetic-homotopy-theory.groups-of-loops-in-1-types |
| Iterated loop spaces | synthetic-homotopy-theory.iterated-loop-spaces |
| Multivariable loop spaces | synthetic-homotopy-theory.multivariable-loop-spaces |
| Powers of loops | synthetic-homotopy-theory.powers-of-loops |
| Triple loop spaces | synthetic-homotopy-theory.triple-loop-spaces |
Definitions
The I-ary loop space
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-multivariable-Ω : UU (l1 ⊔ l2) type-multivariable-Ω = Σ A (λ a → I → a ＝ a∗) refl-multivariable-Ω : type-multivariable-Ω refl-multivariable-Ω = (a∗ , refl-htpy) multivariable-Ω : Pointed-Type (l1 ⊔ l2) multivariable-Ω = (type-multivariable-Ω , refl-multivariable-Ω)
Properties
Characterizing equality in multivariable loop spaces
module _ {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2} where Eq-multivariable-Ω : (x y : type-multivariable-Ω I A∗) → UU (l1 ⊔ l2) Eq-multivariable-Ω (a , p) (b , q) = Σ ( a ＝ b) ( λ r → (i : I) → coherence-triangle-identifications (p i) (q i) r) refl-Eq-multivariable-Ω : (x : type-multivariable-Ω I A∗) → Eq-multivariable-Ω x x refl-Eq-multivariable-Ω p = (refl , refl-htpy) Eq-eq-multivariable-Ω : (x y : type-multivariable-Ω I A∗) → x ＝ y → Eq-multivariable-Ω x y Eq-eq-multivariable-Ω x .x refl = refl-Eq-multivariable-Ω x abstract is-torsorial-Eq-multivariable-Ω : (x : type-multivariable-Ω I A∗) → is-torsorial (Eq-multivariable-Ω x) is-torsorial-Eq-multivariable-Ω (a , p) = is-torsorial-Eq-structure ( is-torsorial-Id a) ( a , refl) ( is-torsorial-htpy p) is-equiv-Eq-eq-multivariable-Ω : (x y : type-multivariable-Ω I A∗) → is-equiv (Eq-eq-multivariable-Ω x y) is-equiv-Eq-eq-multivariable-Ω x = fundamental-theorem-id ( is-torsorial-Eq-multivariable-Ω x) ( Eq-eq-multivariable-Ω x) extensionality-multivariable-Ω : (x y : type-multivariable-Ω I A∗) → (x ＝ y) ≃ Eq-multivariable-Ω x y extensionality-multivariable-Ω x y = ( Eq-eq-multivariable-Ω x y , is-equiv-Eq-eq-multivariable-Ω x y) eq-Eq-multivariable-Ω : (x y : type-multivariable-Ω I A∗) → Eq-multivariable-Ω x y → x ＝ y eq-Eq-multivariable-Ω x y = map-inv-equiv (extensionality-multivariable-Ω x y)
Characterizing equality of equality in multivariable loop spaces
module _ {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2} (x y : type-multivariable-Ω I A∗) where Eq²-multivariable-Ω : (p q : Eq-multivariable-Ω x y) → UU (l1 ⊔ l2) Eq²-multivariable-Ω (p , H) (q , K) = Σ (p ＝ q) (λ r → (i : I) → H i ∙ ap (_∙ pr2 y i) r ＝ K i) refl-Eq²-multivariable-Ω : (p : Eq-multivariable-Ω x y) → Eq²-multivariable-Ω p p refl-Eq²-multivariable-Ω p = (refl , right-unit-htpy) Eq²-eq-multivariable-Ω : (p q : Eq-multivariable-Ω x y) → p ＝ q → Eq²-multivariable-Ω p q Eq²-eq-multivariable-Ω p .p refl = refl-Eq²-multivariable-Ω p abstract is-torsorial-Eq²-multivariable-Ω : (p : Eq-multivariable-Ω x y) → is-torsorial (Eq²-multivariable-Ω p) is-torsorial-Eq²-multivariable-Ω (a , p) = is-torsorial-Eq-structure ( is-torsorial-Id a) ( a , refl) ( is-torsorial-htpy (p ∙h refl-htpy)) is-equiv-Eq²-eq-multivariable-Ω : (p q : Eq-multivariable-Ω x y) → is-equiv (Eq²-eq-multivariable-Ω p q) is-equiv-Eq²-eq-multivariable-Ω p = fundamental-theorem-id ( is-torsorial-Eq²-multivariable-Ω p) ( Eq²-eq-multivariable-Ω p) extensionality²-multivariable-Ω : (p q : Eq-multivariable-Ω x y) → (p ＝ q) ≃ Eq²-multivariable-Ω p q extensionality²-multivariable-Ω p q = ( Eq²-eq-multivariable-Ω p q , is-equiv-Eq²-eq-multivariable-Ω p q) eq-Eq²-multivariable-Ω : (p q : Eq-multivariable-Ω x y) → Eq²-multivariable-Ω p q → p ＝ q eq-Eq²-multivariable-Ω p q = map-inv-equiv (extensionality²-multivariable-Ω p q)
The multivariable loops over a pointed type forms a magma
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-multivariable-Ω : (a b : type-multivariable-Ω I A∗) → type-multivariable-Ω I A∗ mul-multivariable-Ω (a , p) (b , q) = (a , (λ x → p x ∙ inv (q i∗) ∙ q x)) multivariable-Ω-Magma : Magma (l1 ⊔ l2) multivariable-Ω-Magma = (type-multivariable-Ω I A∗ , mul-multivariable-Ω)
The coherent H-space of I-ary loops, for pointed I
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-multivariable-Ω : (x : type-multivariable-Ω I A∗) → Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (refl-multivariable-Ω I A∗) x) ( x) Eq-left-unit-law-mul-multivariable-Ω (a , p) = (inv (p i∗) , refl-htpy) left-unit-law-mul-multivariable-Ω : (x : type-multivariable-Ω I A∗) → mul-multivariable-Ω I∗ A∗ (refl-multivariable-Ω I A∗) x ＝ x left-unit-law-mul-multivariable-Ω x = eq-Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (refl-multivariable-Ω I A∗) x) ( x) ( Eq-left-unit-law-mul-multivariable-Ω x) Eq-right-unit-law-mul-multivariable-Ω : (x : type-multivariable-Ω I A∗) → Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ x (refl-multivariable-Ω I A∗)) ( x) Eq-right-unit-law-mul-multivariable-Ω x = ( refl , right-unit-htpy ∙h right-unit-htpy) right-unit-law-mul-multivariable-Ω : (x : type-multivariable-Ω I A∗) → mul-multivariable-Ω I∗ A∗ x (refl-multivariable-Ω I A∗) ＝ x right-unit-law-mul-multivariable-Ω x = eq-Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ x (refl-multivariable-Ω I A∗)) ( x) ( Eq-right-unit-law-mul-multivariable-Ω x) Eq-coherence-unit-laws-mul-multivariable-Ω : Eq²-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ ( refl-multivariable-Ω I A∗) ( refl-multivariable-Ω I A∗)) ( refl-multivariable-Ω I A∗) ( Eq-left-unit-law-mul-multivariable-Ω (refl-multivariable-Ω I A∗)) ( Eq-right-unit-law-mul-multivariable-Ω (refl-multivariable-Ω I A∗)) Eq-coherence-unit-laws-mul-multivariable-Ω = ( refl , refl-htpy) coherence-unit-laws-mul-multivariable-Ω : left-unit-law-mul-multivariable-Ω (refl-multivariable-Ω I A∗) ＝ right-unit-law-mul-multivariable-Ω (refl-multivariable-Ω I A∗) coherence-unit-laws-mul-multivariable-Ω = refl multivariable-Ω-H-Space : H-Space (l1 ⊔ l2) multivariable-Ω-H-Space = ( multivariable-Ω I A∗ , mul-multivariable-Ω I∗ A∗ , left-unit-law-mul-multivariable-Ω , right-unit-law-mul-multivariable-Ω , coherence-unit-laws-mul-multivariable-Ω)
Associativity of multiplication
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-multivariable-Ω : (x y z : type-multivariable-Ω I A∗) → Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (mul-multivariable-Ω I∗ A∗ x y) z) ( mul-multivariable-Ω I∗ A∗ x (mul-multivariable-Ω I∗ A∗ y z)) pr1 (Eq-associative-mul-multivariable-Ω (a , p) (b , q) (c , r)) = refl pr2 (Eq-associative-mul-multivariable-Ω (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-multivariable-Ω : (x y z : type-multivariable-Ω I A∗) → mul-multivariable-Ω I∗ A∗ (mul-multivariable-Ω I∗ A∗ x y) z ＝ mul-multivariable-Ω I∗ A∗ x (mul-multivariable-Ω I∗ A∗ y z) associative-mul-multivariable-Ω x y z = eq-Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (mul-multivariable-Ω I∗ A∗ x y) z) ( mul-multivariable-Ω I∗ A∗ x (mul-multivariable-Ω I∗ A∗ y z)) ( Eq-associative-mul-multivariable-Ω 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∗).
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-multivariable-Ω : type-multivariable-Ω I A∗ → type-multivariable-Ω I A∗ inv-multivariable-Ω (a , p) = (a∗ , (λ i → inv (p i) ∙ p i∗)) Eq-right-inverse-law-mul-multivariable-Ω : (x : type-multivariable-Ω I A∗) → Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω x)) ( refl-multivariable-Ω I A∗) pr1 (Eq-right-inverse-law-mul-multivariable-Ω (a , p)) = p i∗ pr2 (Eq-right-inverse-law-mul-multivariable-Ω (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-multivariable-Ω : (x : type-multivariable-Ω I A∗) → mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω x) ＝ refl-multivariable-Ω I A∗ right-inverse-law-mul-multivariable-Ω x = eq-Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω x)) ( refl-multivariable-Ω I A∗) ( Eq-right-inverse-law-mul-multivariable-Ω x) Eq-left-inverse-law-mul-multivariable-Ω : (x : type-multivariable-Ω I A∗) → Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω x) x) ( refl-multivariable-Ω I A∗) pr1 (Eq-left-inverse-law-mul-multivariable-Ω (a , p)) = refl pr2 (Eq-left-inverse-law-mul-multivariable-Ω (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-multivariable-Ω : (x : type-multivariable-Ω I A∗) → mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω x) x ＝ refl-multivariable-Ω I A∗ left-inverse-law-mul-multivariable-Ω x = eq-Eq-multivariable-Ω ( mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω x) x) ( refl-multivariable-Ω I A∗) ( Eq-left-inverse-law-mul-multivariable-Ω x)
Invertibility of left and right multiplication
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-multivariable-Ω : (a b : type-multivariable-Ω I A∗) → type-multivariable-Ω I A∗ left-mul-inv-multivariable-Ω a = mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω I∗ A∗ a) is-section-left-mul-inv-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-section (mul-multivariable-Ω I∗ A∗ a) (left-mul-inv-multivariable-Ω a) is-section-left-mul-inv-multivariable-Ω a x = equational-reasoning mul-multivariable-Ω I∗ A∗ a ( mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω I∗ A∗ a) x) ＝ mul-multivariable-Ω I∗ A∗ ( mul-multivariable-Ω I∗ A∗ a (inv-multivariable-Ω I∗ A∗ a)) ( x) by inv ( associative-mul-multivariable-Ω I∗ A∗ a ( inv-multivariable-Ω I∗ A∗ a) ( x)) ＝ mul-multivariable-Ω I∗ A∗ (refl-multivariable-Ω I A∗) x by ap ( λ u → mul-multivariable-Ω I∗ A∗ u x) ( right-inverse-law-mul-multivariable-Ω I∗ A∗ a) ＝ x by left-unit-law-mul-multivariable-Ω I∗ A∗ x is-retraction-left-mul-inv-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-retraction (mul-multivariable-Ω I∗ A∗ a) (left-mul-inv-multivariable-Ω a) is-retraction-left-mul-inv-multivariable-Ω a x = equational-reasoning mul-multivariable-Ω I∗ A∗ ( inv-multivariable-Ω I∗ A∗ a) ( mul-multivariable-Ω I∗ A∗ a x) ＝ mul-multivariable-Ω I∗ A∗ ( mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω I∗ A∗ a) a) ( x) by inv ( associative-mul-multivariable-Ω I∗ A∗ ( inv-multivariable-Ω I∗ A∗ a) ( a) ( x)) ＝ mul-multivariable-Ω I∗ A∗ (refl-multivariable-Ω I A∗) x by ap ( λ u → mul-multivariable-Ω I∗ A∗ u x) ( left-inverse-law-mul-multivariable-Ω I∗ A∗ a) ＝ x by left-unit-law-mul-multivariable-Ω I∗ A∗ x section-left-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → section (mul-multivariable-Ω I∗ A∗ a) section-left-mul-multivariable-Ω a = ( left-mul-inv-multivariable-Ω a , is-section-left-mul-inv-multivariable-Ω a) retraction-left-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → retraction (mul-multivariable-Ω I∗ A∗ a) retraction-left-mul-multivariable-Ω a = ( left-mul-inv-multivariable-Ω a , is-retraction-left-mul-inv-multivariable-Ω a) is-equiv-left-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-equiv (mul-multivariable-Ω I∗ A∗ a) is-equiv-left-mul-multivariable-Ω a = is-equiv-is-invertible ( left-mul-inv-multivariable-Ω a) ( is-section-left-mul-inv-multivariable-Ω a) ( is-retraction-left-mul-inv-multivariable-Ω a) equiv-left-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → type-multivariable-Ω I A∗ ≃ type-multivariable-Ω I A∗ equiv-left-mul-multivariable-Ω a = ( mul-multivariable-Ω I∗ A∗ a , is-equiv-left-mul-multivariable-Ω a) is-left-invertible-mul-multivariable-Ω : is-left-invertible-Magma (multivariable-Ω-Magma I∗ A∗) is-left-invertible-mul-multivariable-Ω = is-equiv-left-mul-multivariable-Ω
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-multivariable-Ω : (a b : type-multivariable-Ω I A∗) → type-multivariable-Ω I A∗ right-mul-inv-multivariable-Ω a x = mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω I∗ A∗ a) is-section-right-mul-inv-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-section ( λ x → mul-multivariable-Ω I∗ A∗ x a) ( right-mul-inv-multivariable-Ω a) is-section-right-mul-inv-multivariable-Ω a x = equational-reasoning mul-multivariable-Ω I∗ A∗ ( mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω I∗ A∗ a)) ( a) ＝ mul-multivariable-Ω I∗ A∗ x ( mul-multivariable-Ω I∗ A∗ (inv-multivariable-Ω I∗ A∗ a) a) by associative-mul-multivariable-Ω I∗ A∗ x (inv-multivariable-Ω I∗ A∗ a) a ＝ mul-multivariable-Ω I∗ A∗ x (refl-multivariable-Ω I A∗) by ap ( mul-multivariable-Ω I∗ A∗ x) ( left-inverse-law-mul-multivariable-Ω I∗ A∗ a) ＝ x by right-unit-law-mul-multivariable-Ω I∗ A∗ x is-retraction-right-mul-inv-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-retraction ( λ x → mul-multivariable-Ω I∗ A∗ x a) ( right-mul-inv-multivariable-Ω a) is-retraction-right-mul-inv-multivariable-Ω a x = equational-reasoning mul-multivariable-Ω I∗ A∗ ( mul-multivariable-Ω I∗ A∗ x a) ( inv-multivariable-Ω I∗ A∗ a) ＝ mul-multivariable-Ω I∗ A∗ x ( mul-multivariable-Ω I∗ A∗ a (inv-multivariable-Ω I∗ A∗ a)) by associative-mul-multivariable-Ω I∗ A∗ x a (inv-multivariable-Ω I∗ A∗ a) ＝ mul-multivariable-Ω I∗ A∗ x (refl-multivariable-Ω I A∗) by ap ( mul-multivariable-Ω I∗ A∗ x) ( right-inverse-law-mul-multivariable-Ω I∗ A∗ a) ＝ x by right-unit-law-mul-multivariable-Ω I∗ A∗ x section-right-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → section (λ x → mul-multivariable-Ω I∗ A∗ x a) section-right-mul-multivariable-Ω a = ( right-mul-inv-multivariable-Ω a , is-section-right-mul-inv-multivariable-Ω a) retraction-right-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → retraction (λ x → mul-multivariable-Ω I∗ A∗ x a) retraction-right-mul-multivariable-Ω a = ( right-mul-inv-multivariable-Ω a , is-retraction-right-mul-inv-multivariable-Ω a) is-equiv-right-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → is-equiv (λ x → mul-multivariable-Ω I∗ A∗ x a) is-equiv-right-mul-multivariable-Ω a = is-equiv-is-invertible ( right-mul-inv-multivariable-Ω a) ( is-section-right-mul-inv-multivariable-Ω a) ( is-retraction-right-mul-inv-multivariable-Ω a) equiv-right-mul-multivariable-Ω : (a : type-multivariable-Ω I A∗) → type-multivariable-Ω I A∗ ≃ type-multivariable-Ω I A∗ equiv-right-mul-multivariable-Ω a = ( ( λ x → mul-multivariable-Ω I∗ A∗ x a) , ( is-equiv-right-mul-multivariable-Ω 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.
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-multivariable-Ω-pointed' : type-multivariable-Ω I A∗ ≃ (I∗ →∗ Ω A∗) compute-type-multivariable-Ω-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-multivariable-Ω-pointed : type-multivariable-Ω I A∗ → (I∗ →∗ Ω A∗) map-compute-multivariable-Ω-pointed (a , p) = ( (λ i → inv (p i∗) ∙ p i) , left-inv (p i∗)) map-inv-compute-multivariable-Ω-pointed : (I∗ →∗ Ω A∗) → type-multivariable-Ω I A∗ map-inv-compute-multivariable-Ω-pointed (f , p) = (a∗ , f) is-section-map-inv-compute-multivariable-Ω-pointed : is-section map-compute-multivariable-Ω-pointed map-inv-compute-multivariable-Ω-pointed is-section-map-inv-compute-multivariable-Ω-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-multivariable-Ω-pointed : is-retraction ( map-compute-multivariable-Ω-pointed) ( map-inv-compute-multivariable-Ω-pointed) is-retraction-map-inv-compute-multivariable-Ω-pointed (a , p) = eq-Eq-multivariable-Ω _ _ (inv (p i∗) , refl-htpy) preserves-point-map-compute-multivariable-Ω-pointed : map-compute-multivariable-Ω-pointed (refl-multivariable-Ω I A∗) ＝ ( const I (refl-Ω A∗) , refl) preserves-point-map-compute-multivariable-Ω-pointed = refl is-equiv-map-compute-multivariable-Ω-pointed : is-equiv map-compute-multivariable-Ω-pointed is-equiv-map-compute-multivariable-Ω-pointed = is-equiv-is-invertible ( map-inv-compute-multivariable-Ω-pointed) ( is-section-map-inv-compute-multivariable-Ω-pointed) ( is-retraction-map-inv-compute-multivariable-Ω-pointed) compute-type-multivariable-Ω-pointed : type-multivariable-Ω I A∗ ≃ (I∗ →∗ Ω A∗) compute-type-multivariable-Ω-pointed = ( map-compute-multivariable-Ω-pointed , is-equiv-map-compute-multivariable-Ω-pointed) compute-multivariable-Ω-pointed : multivariable-Ω I A∗ ≃∗ (I∗ →∗ Ω A∗ , (const I (refl-Ω A∗) , refl)) compute-multivariable-Ω-pointed = ( compute-type-multivariable-Ω-pointed , preserves-point-map-compute-multivariable-Ω-pointed)
∅-ary loops
module _ {l : Level} (A∗ : Pointed-Type l) (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) where compute-type-multivariable-Ω-empty : type-multivariable-Ω empty A∗ ≃ A compute-type-multivariable-Ω-empty = right-unit-law-Σ-is-contr (λ a → universal-property-empty' (a ＝ a∗)) map-compute-type-multivariable-Ω-empty : type-multivariable-Ω empty A∗ → A map-compute-type-multivariable-Ω-empty = map-equiv compute-type-multivariable-Ω-empty preserves-point-map-compute-multivariable-Ω-empty : map-compute-type-multivariable-Ω-empty (refl-multivariable-Ω empty A∗) ＝ a∗ preserves-point-map-compute-multivariable-Ω-empty = refl compute-multivariable-Ω-empty : multivariable-Ω empty A∗ ≃∗ A∗ pr1 compute-multivariable-Ω-empty = compute-type-multivariable-Ω-empty pr2 compute-multivariable-Ω-empty = preserves-point-map-compute-multivariable-Ω-empty
I+1-ary loops
(I + 1)-ary loops are equivalent to families of loops I → ΩA, where Ω is
the standard loop type.
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-multivariable-Ω-isolated-point : type-multivariable-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) compute-type-multivariable-Ω-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 we have an equivalence
where denotes the suspension of .
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-multivariable-Ω-suspension : type-multivariable-Ω (suspension I) A∗ ≃ type-multivariable-Ω I (Ω A∗) compute-type-multivariable-Ω-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
module _ {l1 l2 : Level} (I : UU l1) (A∗ : Pointed-Type l2) where abstract is-trunc-type-multivariable-Ω-has-element : (k : 𝕋) → I → is-trunc (succ-𝕋 k) (type-Pointed-Type A∗) → is-trunc k (type-multivariable-Ω I A∗) is-trunc-type-multivariable-Ω-has-element k i∗ K = is-trunc-equiv k ((I , i∗) →∗ Ω A∗) ( compute-type-multivariable-Ω-pointed (I , i∗) A∗) ( is-trunc-pointed-function-type k ( K (point-Pointed-Type A∗) (point-Pointed-Type A∗))) is-trunc-type-multivariable-Ω-is-inhabited : (k : 𝕋) → is-inhabited I → is-trunc (succ-𝕋 k) (type-Pointed-Type A∗) → is-trunc k (type-multivariable-Ω I A∗) is-trunc-type-multivariable-Ω-is-inhabited k H K = rec-trunc-Prop ( is-trunc-Prop k (type-multivariable-Ω I A∗)) ( λ i∗ → is-trunc-type-multivariable-Ω-has-element k i∗ K) ( H)
Recent changes
- 2026-05-05. Fredrik Bakke. Multivariable loop spaces (#1663).