From 0f598da49fd6bbcc40bcfe4bef77e357d60754a2 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 3 Nov 2025 22:31:48 +0100 Subject: [PATCH 01/24] multivariable loop spaces --- .../multivariable-loop-spaces.lagda.md | 358 ++++++++++++++++++ 1 file changed, 358 insertions(+) create mode 100644 src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md 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..b7983dc527 --- /dev/null +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -0,0 +1,358 @@ +# Multivariable loop spaces + +```agda +module synthetic-homotopy-theory.multivariable-loop-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.homotopies +open import foundation.torsorial-type-families +open import foundation.fundamental-theorem-of-identity-types +open import foundation.transport-along-identifications +open import foundation.identity-types +open import foundation.structure-identity-principle +open import foundation.universe-levels +open import foundation.coproduct-types +open import foundation.functoriality-dependent-pair-types +open import foundation.universal-property-coproduct-types +open import foundation.universal-property-maybe +open import foundation.cartesian-product-types +open import foundation.path-algebra +open import foundation.type-arithmetic-cartesian-product-types +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.homotopy-induction +open import foundation.unit-type +open import foundation.action-on-identifications-functions +open import foundation.function-types +open import foundation.equality-dependent-function-types +open import foundation.commuting-triangles-of-identifications +open import foundation.constant-type-families +open import synthetic-homotopy-theory.loop-spaces +open import foundation.equality-dependent-pair-types + +open import structured-types.h-spaces +open import structured-types.magmas +open import foundation.function-extensionality +open import structured-types.pointed-equivalences +open import structured-types.pointed-types +open import structured-types.wild-quasigroups +``` + +
+ +## Idea + +Given a [pointed type](structured-types.pointed-types.md) `i∗ : 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∗))`. We recover the normal loops as the binary loops. + +## 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 + +```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 + +```agda +module _ + {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2} + (u v : type-multivar-Ω I A∗) + where + + Eq²-multivar-Ω : + (p q : Eq-multivar-Ω u v) → UU (l1 ⊔ l2) + Eq²-multivar-Ω (p , H) (q , K) = + Σ (p ＝ q) (λ r → (i : I) → H i ∙ ap (_∙ _) r ＝ K i) + + refl-Eq²-multivar-Ω : + (p : Eq-multivar-Ω u v) → Eq²-multivar-Ω p p + refl-Eq²-multivar-Ω p = (refl , right-unit-htpy) + + Eq²-eq-multivar-Ω : + (p q : Eq-multivar-Ω u v) → p ＝ q → Eq²-multivar-Ω p q + Eq²-eq-multivar-Ω p .p refl = refl-Eq²-multivar-Ω p + + abstract + is-torsorial-Eq²-multivar-Ω : + (p : Eq-multivar-Ω u v) → 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-Ω u v) → 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-Ω u v) → (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-Ω u v) → 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 on a pointed type + +```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-Ω u = + eq-Eq-multivar-Ω + ( mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) u) + ( u) + ( Eq-left-unit-law-mul-multivar-Ω u) + + 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-Ω u = + ( 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-Ω u = + eq-Eq-multivar-Ω + ( mul-multivar-Ω I∗ A∗ u (refl-multivar-Ω I A∗)) + ( u) + ( Eq-right-unit-law-mul-multivar-Ω u) + + 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-Ω) +``` + +### The right inverse + +```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∗ , (λ x → inv (p x) ∙ 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∗) + Eq-right-inverse-law-mul-multivar-Ω (a , p) = + ( p i∗ , + λ 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) +``` + +### Associativity + +```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)) + Eq-associative-mul-multivar-Ω (a , p) (b , q) (c , r) = + ( refl , + λ 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) +``` + +### `I`-ary loops at isolated points + +`(I + 1)`-ary loops are equivalent to families `I → ΩA`, where `Ω` is the +standard loop type. + +```agda +module _ + {l1 l2 : Level} {I : UU l1} (A∗ : Pointed-Type l1) + (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) + where + + equiv-type-isolated-point-multivar-Ω : + type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) + equiv-type-isolated-point-multivar-Ω = + 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) +``` From 2a52780fdbfda7d4de26f364743498c04d1061d9 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 3 Nov 2025 22:37:37 +0100 Subject: [PATCH 02/24] pre-commit --- src/synthetic-homotopy-theory.lagda.md | 1 + 1 file changed, 1 insertion(+) 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 From 11d2280889fb4c722e9db6e131708a369ed16ec2 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 3 Nov 2025 22:41:36 +0100 Subject: [PATCH 03/24] cleanup --- .../multivariable-loop-spaces.lagda.md | 37 ++++++++----------- 1 file changed, 15 insertions(+), 22 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index b7983dc527..24ecf3b2ab 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -7,39 +7,31 @@ module synthetic-homotopy-theory.multivariable-loop-spaces where
Imports ```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.commuting-triangles-of-identifications +open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.homotopies -open import foundation.torsorial-type-families +open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types -open import foundation.transport-along-identifications +open import foundation.homotopies +open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.structure-identity-principle -open import foundation.universe-levels -open import foundation.coproduct-types -open import foundation.functoriality-dependent-pair-types -open import foundation.universal-property-coproduct-types -open import foundation.universal-property-maybe -open import foundation.cartesian-product-types open import foundation.path-algebra +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types -open import foundation.homotopy-induction open import foundation.unit-type -open import foundation.action-on-identifications-functions -open import foundation.function-types -open import foundation.equality-dependent-function-types -open import foundation.commuting-triangles-of-identifications -open import foundation.constant-type-families -open import synthetic-homotopy-theory.loop-spaces -open import foundation.equality-dependent-pair-types +open import foundation.universal-property-maybe +open import foundation.universe-levels open import structured-types.h-spaces open import structured-types.magmas -open import foundation.function-extensionality -open import structured-types.pointed-equivalences open import structured-types.pointed-types -open import structured-types.wild-quasigroups + +open import synthetic-homotopy-theory.loop-spaces ```
@@ -48,7 +40,8 @@ open import structured-types.wild-quasigroups Given a [pointed type](structured-types.pointed-types.md) `i∗ : 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∗))`. We recover the normal loops as the binary loops. +`Σ (a : A), (I → (a ＝ a∗))`. We recover the +[standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops. ## Table of files directly related to loop spaces From 3ad8d6c07058a525c72946023164aaa71ed028f1 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 3 Nov 2025 23:03:18 +0100 Subject: [PATCH 04/24] edit --- docs/tables/loop-spaces-concepts.md | 1 + .../multivariable-loop-spaces.lagda.md | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 24ecf3b2ab..daa1d103f1 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -324,7 +324,7 @@ module _ ( Eq-associative-mul-multivar-Ω x y z) ``` -### `I`-ary loops at isolated points +### `I+1`-ary loops `(I + 1)`-ary loops are equivalent to families `I → ΩA`, where `Ω` is the standard loop type. From ca811b30a1c8e60e2b8639ec25350362b4559e73 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 4 Nov 2025 15:45:48 +0100 Subject: [PATCH 05/24] edit --- .../multivariable-loop-spaces.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index daa1d103f1..cda27d817c 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -41,7 +41,8 @@ open import synthetic-homotopy-theory.loop-spaces Given a [pointed type](structured-types.pointed-types.md) `i∗ : 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∗))`. We recover the -[standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops. +[standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops, +`A` as the `∅`-ary loops, and there is a unique unary loop. ## Table of files directly related to loop spaces From e88efe7e601471baa6b2b7abf112a4667e2c369f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 4 Nov 2025 23:58:40 +0100 Subject: [PATCH 06/24] One-sided invertibility of left and right multiplication in multivariable loop spaces --- src/structured-types.lagda.md | 1 + .../left-invertible-magmas.lagda.md | 44 ++++++++++++ .../multivariable-loop-spaces.lagda.md | 68 +++++++++++++++++++ 3 files changed, 113 insertions(+) create mode 100644 src/structured-types/left-invertible-magmas.lagda.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..83a701deda --- /dev/null +++ b/src/structured-types/left-invertible-magmas.lagda.md @@ -0,0 +1,44 @@ +# Left-invertible magmas + +```agda +module structured-types.left-invertible-magmas where +``` + +
Imports + +```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 +``` + +
+ +## Idea + +A [magma](structured.magma.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`. + +## 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) +``` diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index cda27d817c..7392965b61 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -13,12 +13,15 @@ open import foundation.commuting-triangles-of-identifications open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.function-types 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.path-algebra +open import foundation.retractions +open import foundation.sections open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.type-arithmetic-cartesian-product-types @@ -28,6 +31,7 @@ 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-types @@ -350,3 +354,67 @@ module _ ≃ (I → type-Ω A∗) by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl) ``` + +### One-sided 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 + + map-section-left-mul-multivar-Ω : + type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗ + map-section-left-mul-multivar-Ω a = + mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) + + is-section-map-section-left-mul-multivar-Ω : + (a : type-multivar-Ω I A∗) → + is-section (mul-multivar-Ω I∗ A∗ a) (map-section-left-mul-multivar-Ω a) + is-section-map-section-left-mul-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 + + section-left-mul-multivar-Ω : + (a : type-multivar-Ω I A∗) → section (mul-multivar-Ω I∗ A∗ a) + section-left-mul-multivar-Ω a = + ( map-section-left-mul-multivar-Ω a , + is-section-map-section-left-mul-multivar-Ω a) + + map-retraction-right-mul-multivar-Ω : + type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗ + map-retraction-right-mul-multivar-Ω a x = + mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a) + + is-retraction-map-retraction-right-mul-multivar-Ω : + (a : type-multivar-Ω I A∗) → + is-retraction + ( λ x → mul-multivar-Ω I∗ A∗ x a) + ( map-retraction-right-mul-multivar-Ω a) + is-retraction-map-retraction-right-mul-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 + + retraction-right-mul-multivar-Ω : + (a : type-multivar-Ω I A∗) → retraction (λ x → mul-multivar-Ω I∗ A∗ x a) + retraction-right-mul-multivar-Ω a = + ( map-retraction-right-mul-multivar-Ω a , + is-retraction-map-retraction-right-mul-multivar-Ω a) +``` From c65104bf87f4757389f2ba26b2e3dafafb7f6b74 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 4 Nov 2025 23:58:46 +0100 Subject: [PATCH 07/24] import --- src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 7392965b61..92beb98755 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -31,7 +31,6 @@ 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-types From a4d0fc4a108bf38ffdf1261308c329f6159dd523 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 00:00:03 +0100 Subject: [PATCH 08/24] reference --- src/structured-types/left-invertible-magmas.lagda.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/structured-types/left-invertible-magmas.lagda.md b/src/structured-types/left-invertible-magmas.lagda.md index 83a701deda..8c8e097ff5 100644 --- a/src/structured-types/left-invertible-magmas.lagda.md +++ b/src/structured-types/left-invertible-magmas.lagda.md @@ -24,6 +24,9 @@ A [magma](structured.magma.md) `A` is if the multiplication map `μ(a,-) : A → A` is an [equivalence](foundation-core.equivalences.md) for every `a : A`. +Left-invertibility in the context of [H-spaces](structured-types.h-spaces.md) +appears as Definition 2.1(4) of {{#cite BCFR23}}. + ## Definition ```agda @@ -42,3 +45,7 @@ module _ is-left-invertible-prop-Magma = ( is-left-invertible-Magma , is-prop-is-left-invertible-Magma) ``` + +## References + +{{#bibliography}} From f2a8ef51e9527a57dd6051ca4c689b75433a4200 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 13:22:58 +0100 Subject: [PATCH 09/24] edit --- .../left-invertible-magmas.lagda.md | 2 +- .../multivariable-loop-spaces.lagda.md | 87 ++++++++++--------- 2 files changed, 46 insertions(+), 43 deletions(-) diff --git a/src/structured-types/left-invertible-magmas.lagda.md b/src/structured-types/left-invertible-magmas.lagda.md index 8c8e097ff5..90d2da821b 100644 --- a/src/structured-types/left-invertible-magmas.lagda.md +++ b/src/structured-types/left-invertible-magmas.lagda.md @@ -19,7 +19,7 @@ open import structured-types.magmas ## Idea -A [magma](structured.magma.md) `A` is +A [magma](structured-types.magma.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`. diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 92beb98755..9eaefb6cce 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -47,6 +47,9 @@ pointed type `a∗ : A`, we can form the `I`-ary loop space in `A` as the type [standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops, `A` as the `∅`-ary loops, and there is a unique unary loop. +The type of `I`-ary loops have an associative coherent H-space structure with +right inverses. + ## Table of files directly related to loop spaces {{#include tables/loop-spaces-concepts.md}} @@ -122,25 +125,25 @@ module _ ```agda module _ {l1 l2 : Level} {I : UU l1} {A∗ : Pointed-Type l2} - (u v : type-multivar-Ω I A∗) + (x y : type-multivar-Ω I A∗) where Eq²-multivar-Ω : - (p q : Eq-multivar-Ω u v) → UU (l1 ⊔ l2) + (p q : Eq-multivar-Ω x y) → UU (l1 ⊔ l2) Eq²-multivar-Ω (p , H) (q , K) = - Σ (p ＝ q) (λ r → (i : I) → H i ∙ ap (_∙ _) r ＝ K i) + Σ (p ＝ q) (λ r → (i : I) → H i ∙ ap (_∙ pr2 y i) r ＝ K i) refl-Eq²-multivar-Ω : - (p : Eq-multivar-Ω u v) → Eq²-multivar-Ω p p + (p : Eq-multivar-Ω x y) → Eq²-multivar-Ω p p refl-Eq²-multivar-Ω p = (refl , right-unit-htpy) Eq²-eq-multivar-Ω : - (p q : Eq-multivar-Ω u v) → p ＝ q → Eq²-multivar-Ω p q + (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-Ω u v) → is-torsorial (Eq²-multivar-Ω p) + (p : Eq-multivar-Ω x y) → is-torsorial (Eq²-multivar-Ω p) is-torsorial-Eq²-multivar-Ω (a , p) = is-torsorial-Eq-structure ( is-torsorial-Id a) @@ -148,19 +151,19 @@ module _ ( is-torsorial-htpy (p ∙h refl-htpy)) is-equiv-Eq²-eq-multivar-Ω : - (p q : Eq-multivar-Ω u v) → is-equiv (Eq²-eq-multivar-Ω p q) + (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-Ω u v) → (p ＝ q) ≃ Eq²-multivar-Ω p q + (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-Ω u v) → Eq²-multivar-Ω p q → p ＝ q + (p q : Eq-multivar-Ω x y) → Eq²-multivar-Ω p q → p ＝ q eq-Eq²-multivar-Ω p q = map-inv-equiv (extensionality²-multivar-Ω p q) ``` @@ -176,7 +179,7 @@ module _ 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) + 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-Ω) @@ -200,26 +203,26 @@ module _ 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-Ω u = + left-unit-law-mul-multivar-Ω x = eq-Eq-multivar-Ω - ( mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) u) - ( u) - ( Eq-left-unit-law-mul-multivar-Ω u) + ( 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-Ω u = + 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-Ω u = + right-unit-law-mul-multivar-Ω x = eq-Eq-multivar-Ω - ( mul-multivar-Ω I∗ A∗ u (refl-multivar-Ω I A∗)) - ( u) - ( Eq-right-unit-law-mul-multivar-Ω u) + ( 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-Ω @@ -254,36 +257,36 @@ module _ (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∗ , (λ x → inv (p x) ∙ p i∗)) + right-inv-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗ + right-inv-multivar-Ω (a , p) = (a∗ , (λ x → inv (p x) ∙ p i∗)) Eq-right-inverse-law-mul-multivar-Ω : (x : type-multivar-Ω I A∗) → Eq-multivar-Ω - ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x)) + ( mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω x)) ( refl-multivar-Ω I A∗) Eq-right-inverse-law-mul-multivar-Ω (a , p) = ( p i∗ , λ 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) + (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) ＝ + mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω x) ＝ refl-multivar-Ω I A∗ right-inverse-law-mul-multivar-Ω x = eq-Eq-multivar-Ω - ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x)) + ( mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω x)) ( refl-multivar-Ω I A∗) ( Eq-right-inverse-law-mul-multivar-Ω x) ``` @@ -367,16 +370,16 @@ module _ map-section-left-mul-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗ map-section-left-mul-multivar-Ω a = - mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) + mul-multivar-Ω I∗ A∗ (right-inv-multivar-Ω I∗ A∗ a) is-section-map-section-left-mul-multivar-Ω : (a : type-multivar-Ω I A∗) → is-section (mul-multivar-Ω I∗ A∗ a) (map-section-left-mul-multivar-Ω a) is-section-map-section-left-mul-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∗ a (mul-multivar-Ω I∗ A∗ (right-inv-multivar-Ω I∗ A∗ a) x) + ＝ mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a)) x + by inv (associative-mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a) x) ＝ mul-multivar-Ω I∗ A∗ (refl-multivar-Ω I A∗) x by ap @@ -394,7 +397,7 @@ module _ map-retraction-right-mul-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗ map-retraction-right-mul-multivar-Ω a x = - mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a) + mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω I∗ A∗ a) is-retraction-map-retraction-right-mul-multivar-Ω : (a : type-multivar-Ω I A∗) → @@ -403,9 +406,9 @@ module _ ( map-retraction-right-mul-multivar-Ω a) is-retraction-map-retraction-right-mul-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∗ (mul-multivar-Ω I∗ A∗ x a) (right-inv-multivar-Ω I∗ A∗ a) + ＝ mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a)) + by associative-mul-multivar-Ω I∗ A∗ x a (right-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 From 0ee6f724064090d661d66284041dfa0f93bd58a7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 13:47:59 +0100 Subject: [PATCH 10/24] invertibility of multivariable loop spaces --- .../multivariable-loop-spaces.lagda.md | 246 +++++++++++++----- 1 file changed, 180 insertions(+), 66 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 9eaefb6cce..388c905c38 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -31,6 +31,7 @@ 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-types @@ -247,7 +248,7 @@ module _ coherence-unit-laws-mul-multivar-Ω) ``` -### The right inverse +### Associativity ```agda module _ @@ -257,13 +258,53 @@ module _ (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) where - right-inv-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗ - right-inv-multivar-Ω (a , p) = (a∗ , (λ x → inv (p x) ∙ p i∗)) + 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)) + Eq-associative-mul-multivar-Ω (a , p) (b , q) (c , r) = + ( refl , + λ 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 inverse + +```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 (right-inv-multivar-Ω x)) + ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x)) ( refl-multivar-Ω I A∗) Eq-right-inverse-law-mul-multivar-Ω (a , p) = ( p i∗ , @@ -282,53 +323,37 @@ module _ right-inverse-law-mul-multivar-Ω : (x : type-multivar-Ω I A∗) → - mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω x) ＝ + 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 (right-inv-multivar-Ω x)) + ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x)) ( refl-multivar-Ω I A∗) ( Eq-right-inverse-law-mul-multivar-Ω x) -``` -### Associativity - -```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-left-inverse-law-mul-multivar-Ω : + (x : 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)) - Eq-associative-mul-multivar-Ω (a , p) (b , q) (c , r) = + ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x) + ( refl-multivar-Ω I A∗) + Eq-left-inverse-law-mul-multivar-Ω (a , p) = ( refl , - λ 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 = + ( λ 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∗ (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) + ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x) + ( refl-multivar-Ω I A∗) + ( Eq-left-inverse-law-mul-multivar-Ω x) ``` ### `I+1`-ary loops @@ -357,7 +382,7 @@ module _ by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl) ``` -### One-sided invertibility of left and right multiplication +### Invertibility of left and right multiplication ```agda module _ @@ -367,19 +392,19 @@ module _ (let A = type-Pointed-Type A∗) where - map-section-left-mul-multivar-Ω : + left-mul-inv-multivar-Ω : type-multivar-Ω I A∗ → type-multivar-Ω I A∗ → type-multivar-Ω I A∗ - map-section-left-mul-multivar-Ω a = - mul-multivar-Ω I∗ A∗ (right-inv-multivar-Ω I∗ A∗ a) + left-mul-inv-multivar-Ω a = + mul-multivar-Ω I∗ A∗ (inv-multivar-Ω I∗ A∗ a) - is-section-map-section-left-mul-multivar-Ω : + is-section-left-mul-inv-multivar-Ω : (a : type-multivar-Ω I A∗) → - is-section (mul-multivar-Ω I∗ A∗ a) (map-section-left-mul-multivar-Ω a) - is-section-map-section-left-mul-multivar-Ω a x = + 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∗ (right-inv-multivar-Ω I∗ A∗ a) x) - ＝ mul-multivar-Ω I∗ A∗ (mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a)) x - by inv (associative-mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a) x) + 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 @@ -388,35 +413,124 @@ module _ ＝ 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 = - ( map-section-left-mul-multivar-Ω a , - is-section-map-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-Ω +``` - map-retraction-right-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∗ - map-retraction-right-mul-multivar-Ω a x = - mul-multivar-Ω I∗ A∗ x (right-inv-multivar-Ω I∗ A∗ a) + right-mul-inv-multivar-Ω a x = + mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω I∗ A∗ a) - is-retraction-map-retraction-right-mul-multivar-Ω : + 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) - ( map-retraction-right-mul-multivar-Ω a) - is-retraction-map-retraction-right-mul-multivar-Ω a x = + ( 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) (right-inv-multivar-Ω I∗ A∗ a) - ＝ mul-multivar-Ω I∗ A∗ x (mul-multivar-Ω I∗ A∗ a (right-inv-multivar-Ω I∗ A∗ a)) - by associative-mul-multivar-Ω I∗ A∗ x a (right-inv-multivar-Ω I∗ A∗ a) + 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) + (a : type-multivar-Ω I A∗) → + retraction (λ x → mul-multivar-Ω I∗ A∗ x a) retraction-right-mul-multivar-Ω a = - ( map-retraction-right-mul-multivar-Ω a , - is-retraction-map-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) ``` From 1c2a2d227455f1972a3b49c6fe24e3e56850db88 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 13:51:10 +0100 Subject: [PATCH 11/24] fix link --- src/structured-types/left-invertible-magmas.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/structured-types/left-invertible-magmas.lagda.md b/src/structured-types/left-invertible-magmas.lagda.md index 90d2da821b..6d85ad9373 100644 --- a/src/structured-types/left-invertible-magmas.lagda.md +++ b/src/structured-types/left-invertible-magmas.lagda.md @@ -19,7 +19,7 @@ open import structured-types.magmas ## Idea -A [magma](structured-types.magma.md) `A` is +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`. From 8cfabcb55d984fe418df7219bc15058f62e835e2 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 18:17:23 +0100 Subject: [PATCH 12/24] =?UTF-8?q?$=CE=A9=5F{=CE=A3I}(A)=20=E2=89=83=20?= =?UTF-8?q?=CE=A9=5FI(=CE=A9(A))$?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../multivariable-loop-spaces.lagda.md | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 388c905c38..e1b02d3761 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -36,6 +36,9 @@ open import structured-types.magmas open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces +open import synthetic-homotopy-theory.suspension-structures +open import synthetic-homotopy-theory.suspensions-of-pointed-types +open import synthetic-homotopy-theory.suspensions-of-types ``` @@ -534,3 +537,28 @@ module _ equiv-right-mul-multivar-Ω a = ((λ x → mul-multivar-Ω I∗ A∗ x a) , is-equiv-right-mul-multivar-Ω a) ``` + +### `ΣI`-ary loops are `I`-ary loops of loops + +For every type $I$ we have the equivalence + +$$Ω_{ΣI}(A) ≃ Ω_I(Ω(A)).$$ + +```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∗) +``` From 20901b837a13eedb8537755246076fad56f22ab3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 18:18:10 +0100 Subject: [PATCH 13/24] move a section --- .../multivariable-loop-spaces.lagda.md | 52 +++++++++---------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index e1b02d3761..c2b91b6e56 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -359,32 +359,6 @@ module _ ( Eq-left-inverse-law-mul-multivar-Ω x) ``` -### `I+1`-ary loops - -`(I + 1)`-ary loops are equivalent to families `I → ΩA`, where `Ω` is the -standard loop type. - -```agda -module _ - {l1 l2 : Level} {I : UU l1} (A∗ : Pointed-Type l1) - (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) - where - - equiv-type-isolated-point-multivar-Ω : - type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) - equiv-type-isolated-point-multivar-Ω = - 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) -``` - ### Invertibility of left and right multiplication ```agda @@ -538,6 +512,32 @@ module _ ((λ x → mul-multivar-Ω I∗ A∗ x a) , is-equiv-right-mul-multivar-Ω a) ``` +### `I+1`-ary loops + +`(I + 1)`-ary loops are equivalent to families `I → ΩA`, where `Ω` is the +standard loop type. + +```agda +module _ + {l1 l2 : Level} {I : UU l1} (A∗ : Pointed-Type l1) + (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) + where + + equiv-type-isolated-point-multivar-Ω : + type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) + equiv-type-isolated-point-multivar-Ω = + 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 the equivalence From 5e900de6c537f57e0879893c4dc0f6b031692f13 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 5 Nov 2025 18:31:17 +0100 Subject: [PATCH 14/24] idea --- .../multivariable-loop-spaces.lagda.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index c2b91b6e56..d62b0705d4 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -45,14 +45,15 @@ open import synthetic-homotopy-theory.suspensions-of-types ## Idea -Given a [pointed type](structured-types.pointed-types.md) `i∗ : I`, and a -pointed type `a∗ : A`, we can form the `I`-ary loop space in `A` as the type +Given a type `I` and a [pointed type](structured-types.pointed-types.md) +`a∗ : A`, we can form the `I`-ary loop space in `A` as the type `Σ (a : A), (I → (a ＝ a∗))`. We recover the [standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops, -`A` as the `∅`-ary loops, and there is a unique unary loop. +`A` as the `∅`-ary loops, and there is a unique unary loop. The `𝕊¹`-ary loops +correspond to [loops of loops](synthetic-homotopy-theory.double-loop-spaces.md). -The type of `I`-ary loops have an associative coherent H-space structure with -right inverses. +For every point of `I` there is a coherent, associative, and invertible H-space +structure on `I`-ary loops. ## Table of files directly related to loop spaces From d75d5d13a33d10b2c23bc02693d8a91b07cb67fb Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 6 Nov 2025 12:15:02 +0100 Subject: [PATCH 15/24] work --- .../cofibers-of-maps.lagda.md | 11 +++++++++++ 1 file changed, 11 insertions(+) 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) From 9d63522429d7940fcabd67ce5d1273b93bf9aff6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 7 Nov 2025 16:13:45 +0100 Subject: [PATCH 16/24] =?UTF-8?q?If=20`I`=20is=20pointed=20then=20`I`-ary?= =?UTF-8?q?=20loops=20are=20pointed=20equivalent=20to=20pointed=20maps=20`?= =?UTF-8?q?I=20=E2=86=92=E2=88=97=20=CE=A9A`=20Co-authored-by:=20markrd-wi?= =?UTF-8?q?lliams=20?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../multivariable-loop-spaces.lagda.md | 82 +++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index d62b0705d4..b160f40351 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -12,6 +12,7 @@ open import foundation.cartesian-product-types open import foundation.commuting-triangles-of-identifications open import foundation.coproduct-types open import foundation.dependent-pair-types +open import foundation.constant-maps open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-pair-types @@ -34,11 +35,15 @@ open import structured-types.h-spaces open import structured-types.left-invertible-magmas open import structured-types.magmas open import structured-types.pointed-types +open import structured-types.pointed-homotopies +open import structured-types.pointed-maps +open import structured-types.pointed-equivalences open import synthetic-homotopy-theory.loop-spaces open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.suspensions-of-pointed-types open import synthetic-homotopy-theory.suspensions-of-types +open import synthetic-homotopy-theory.cavallos-trick ``` @@ -539,6 +544,83 @@ module _ by left-unit-law-Σ-is-contr (is-torsorial-Id' a∗) (a∗ , refl) ``` +### 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 + + 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) +``` + ### `ΣI`-ary loops are `I`-ary loops of loops For every type $I$ we have the equivalence From 34300cbef904f20046f549494149b0b9dfe5c6c1 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 7 Nov 2025 16:16:52 +0100 Subject: [PATCH 17/24] pre-commit Co-authored-by: Mark Williams --- .../multivariable-loop-spaces.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index b160f40351..535f61dfb8 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -10,9 +10,9 @@ module synthetic-homotopy-theory.multivariable-loop-spaces where 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.constant-maps open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-pair-types @@ -34,16 +34,16 @@ 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-types +open import structured-types.pointed-equivalences open import structured-types.pointed-homotopies open import structured-types.pointed-maps -open import structured-types.pointed-equivalences +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.suspension-structures open import synthetic-homotopy-theory.suspensions-of-pointed-types open import synthetic-homotopy-theory.suspensions-of-types -open import synthetic-homotopy-theory.cavallos-trick ``` From cb05c59e5db5e8edc8814cd73f1f9aec3596b85b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 7 Nov 2025 16:27:28 +0100 Subject: [PATCH 18/24] edits --- .../multivariable-loop-spaces.lagda.md | 42 +++++++++++-------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 535f61dfb8..43bad2c5fd 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -51,14 +51,19 @@ open import synthetic-homotopy-theory.suspensions-of-types ## Idea Given a type `I` and a [pointed type](structured-types.pointed-types.md) -`a∗ : A`, we can form the `I`-ary loop space in `A` as the type -`Σ (a : A), (I → (a ＝ a∗))`. We recover the -[standard loops](synthetic-homotopy-theory.loop-spaces.md) as the binary loops, -`A` as the `∅`-ary loops, and there is a unique unary loop. The `𝕊¹`-ary loops -correspond to [loops of loops](synthetic-homotopy-theory.double-loop-spaces.md). - -For every point of `I` there is a coherent, associative, and invertible H-space -structure on `I`-ary loops. +`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 +binary loops, the type `A` itself as the `∅`-ary loops, and there is a unique +unary loop. The `𝕊¹`-ary loops correspond to +[loops of loops](synthetic-homotopy-theory.double-loop-spaces.md). + +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 @@ -623,9 +628,12 @@ module _ ### `ΣI`-ary loops are `I`-ary loops of loops -For every type $I$ we have the equivalence +For every type $I$ we have an equivalence + +$$Ω_{ΣI}(A) ≃ Ω_I(Ω(A))$$ -$$Ω_{ΣI}(A) ≃ Ω_I(Ω(A)).$$ +where $ΣI$ denotes the +[suspension](synthetic-homotopy-theory.suspensions-of-types.md) of $I$. ```agda module _ @@ -637,11 +645,11 @@ module _ 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∗) + Σ 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∗) ``` From 394ac4df02d928f116525474d207549664328a85 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 7 Nov 2025 16:31:08 +0100 Subject: [PATCH 19/24] imports --- src/structured-types/left-invertible-magmas.lagda.md | 7 ++++--- .../multivariable-loop-spaces.lagda.md | 3 --- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/structured-types/left-invertible-magmas.lagda.md b/src/structured-types/left-invertible-magmas.lagda.md index 6d85ad9373..de0a6427b2 100644 --- a/src/structured-types/left-invertible-magmas.lagda.md +++ b/src/structured-types/left-invertible-magmas.lagda.md @@ -22,10 +22,11 @@ open import structured-types.magmas 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`. +[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 in the context of [H-spaces](structured-types.h-spaces.md) -appears as Definition 2.1(4) of {{#cite BCFR23}}. +Left-invertibility appears as Definition 2.1(4) of {{#cite BCFR23}} in the +context of [H-spaces](structured-types.h-spaces.md). ## Definition diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 43bad2c5fd..00292c7233 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -14,7 +14,6 @@ open import foundation.constant-maps open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies @@ -41,8 +40,6 @@ 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.suspension-structures -open import synthetic-homotopy-theory.suspensions-of-pointed-types open import synthetic-homotopy-theory.suspensions-of-types ``` From a35d142a732b8edfd976c2b7f068dd1ee13c0987 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 7 Nov 2025 20:33:26 +0100 Subject: [PATCH 20/24] fix reasoning syntax --- .../multivariable-loop-spaces.lagda.md | 154 +++++++++--------- 1 file changed, 77 insertions(+), 77 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 00292c7233..e8813173a4 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -197,7 +197,7 @@ module _ multivar-Ω-Magma = (type-multivar-Ω I A∗ , mul-multivar-Ω) ``` -### The coherent H-space of `I`-ary loops on a pointed type +### The coherent H-space of `I`-ary loops, for pointed `I` ```agda module _ @@ -259,7 +259,7 @@ module _ coherence-unit-laws-mul-multivar-Ω) ``` -### Associativity +### Associativity of multiplication ```agda module _ @@ -274,10 +274,9 @@ module _ 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-Ω (a , p) (b , q) (c , r) = - ( refl , - λ x → - equational-reasoning + 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 @@ -286,7 +285,7 @@ module _ by ap ( λ u → (p x ∙ inv u) ∙ (q x ∙ inv (r i∗) ∙ r x)) - ( inv (is-section-inv-concat' (r i∗) (q i∗)))) + ( inv (is-section-inv-concat' (r i∗) (q i∗))) associative-mul-multivar-Ω : (x y z : type-multivar-Ω I A∗) → @@ -299,7 +298,10 @@ module _ ( Eq-associative-mul-multivar-Ω x y z) ``` -### The inverse +### 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 _ @@ -317,20 +319,19 @@ module _ Eq-multivar-Ω ( mul-multivar-Ω I∗ A∗ x (inv-multivar-Ω x)) ( refl-multivar-Ω I A∗) - Eq-right-inverse-law-mul-multivar-Ω (a , p) = - ( p i∗ , - λ 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) + 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∗) → @@ -347,14 +348,13 @@ module _ Eq-multivar-Ω ( mul-multivar-Ω I∗ A∗ (inv-multivar-Ω x) x) ( refl-multivar-Ω I A∗) - Eq-left-inverse-law-mul-multivar-Ω (a , p) = - ( refl , - ( λ 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))) + 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∗) → @@ -387,36 +387,36 @@ module _ 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 + 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 + 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) @@ -468,13 +468,13 @@ module _ ( 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 + 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∗) → @@ -483,13 +483,13 @@ module _ ( 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 + 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∗) → @@ -535,15 +535,15 @@ module _ type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) equiv-type-isolated-point-multivar-Ω = 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) + Σ 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) ``` ### If `I` is pointed then `I`-ary loops are pointed equivalent to pointed maps `I →∗ ΩA` From 823f20db0bd7d640d069b4d7b49cac14605df236 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 00:40:27 +0100 Subject: [PATCH 21/24] pre-commit --- .../multivariable-loop-spaces.lagda.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index e8813173a4..26892d624f 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -88,7 +88,7 @@ module _ ## Properties -### Characterizing equality +### Characterizing equality in `I`-ary loop spaces ```agda module _ @@ -132,7 +132,7 @@ module _ map-inv-equiv (extensionality-multivar-Ω x y) ``` -### Characterizing equality of equality +### Characterizing equality of equality in `I`-ary loop spaces ```agda module _ @@ -487,7 +487,8 @@ module _ ＝ 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) + 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 From b1512d433d5e9756d1f8b4fc3f5b8fc1047a04f8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 00:45:53 +0100 Subject: [PATCH 22/24] explain arity --- .../multivariable-loop-spaces.lagda.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 26892d624f..0ce2a6529c 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -52,15 +52,18 @@ Given a type `I` and a [pointed type](structured-types.pointed-types.md) `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 -binary loops, the type `A` itself as the `∅`-ary loops, and there is a unique -unary loop. The `𝕊¹`-ary loops correspond to -[loops of loops](synthetic-homotopy-theory.double-loop-spaces.md). +`1+1`-ary loops, the type `A` itself as the `∅`-ary loops, and there is a unique +`1`-ary loop. 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`. +loops of `A` and `(I,x) →∗ ΩA`. ## Table of files directly related to loop spaces From 9cf1a96e86d5de4d36e11890afbf9e8b007c28af Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 00:56:01 +0100 Subject: [PATCH 23/24] =?UTF-8?q?=E2=88=85-ary=20loops?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../multivariable-loop-spaces.lagda.md | 75 ++++++++++++------- 1 file changed, 49 insertions(+), 26 deletions(-) diff --git a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 0ce2a6529c..2a1b0a4cd1 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -13,6 +13,7 @@ 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 @@ -27,6 +28,7 @@ open import foundation.torsorial-type-families 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 @@ -524,32 +526,6 @@ module _ ((λ x → mul-multivar-Ω I∗ A∗ x a) , is-equiv-right-mul-multivar-Ω a) ``` -### `I+1`-ary loops - -`(I + 1)`-ary loops are equivalent to families `I → ΩA`, where `Ω` is the -standard loop type. - -```agda -module _ - {l1 l2 : Level} {I : UU l1} (A∗ : Pointed-Type l1) - (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) - where - - equiv-type-isolated-point-multivar-Ω : - type-multivar-Ω (I + unit) A∗ ≃ (I → type-Ω A∗) - equiv-type-isolated-point-multivar-Ω = - 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) -``` - ### 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 @@ -627,6 +603,53 @@ module _ 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 From 34edbb2cac269b511e675c777a08c896fcd6974b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 10:44:50 +0100 Subject: [PATCH 24/24] Truncatedness of `I`-ary loops --- config/codespell-dictionary.txt | 2 + src/structured-types/pointed-maps.lagda.md | 17 +++++ .../multivariable-loop-spaces.lagda.md | 62 ++++++++++++++----- 3 files changed, 66 insertions(+), 15 deletions(-) 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/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/multivariable-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md index 2a1b0a4cd1..f70aa3511f 100644 --- a/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/multivariable-loop-spaces.lagda.md @@ -20,11 +20,15 @@ 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 @@ -54,8 +58,8 @@ Given a type `I` and a [pointed type](structured-types.pointed-types.md) `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, the type `A` itself as the `∅`-ary loops, and there is a unique -`1`-ary loop. The `𝕊¹`-ary loops correspond to +`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 @@ -540,19 +544,21 @@ module _ (let A = type-Pointed-Type A∗) (let a∗ = point-Pointed-Type A∗) where - 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) + 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∗) @@ -677,3 +683,29 @@ module _ ≃ Σ (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) +```