Multivariable loop spaces (#1663)

Co-authored-by: Mark Williams <markrd.williams@gmail.com>

Author: fredrik-bakke

config/codespell-dictionary.txt

@@ -32,6 +32,7 @@ conisistsed->consisted
 conisistsing->consisting
 consistsed->consisted
 consistsing->consisting
+diamgram->diagram
 eacy->each,easy
 embeddding->embedding
 embedddings->embeddings
@@ -59,6 +60,7 @@ homomorphsim->homomorphism
 homomorphsims->homomorphisms
 identitification->identification
 identitifications->identifications
+inhanited->inhabited
 isomorhpism->isomorphism
 isomorhpisms->isomorphisms
 isomorhpsim->isomorphism

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)                 |

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

src/structured-types/left-invertible-magmas.lagda.md

@@ -0,0 +1,55 @@
+# Left-invertible magmas
+
+```agda
+module structured-types.left-invertible-magmas where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.dependent-products-propositions
+open import foundation.equivalences
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import structured-types.magmas
+```
+
+</details>
+
+## Idea
+
+A [magma](structured-types.magmas.md) `A` is
+{{#concept "left-invertible" Disambiguation="magma" Agda=is-left-invertible-Magma}}
+if the multiplication map `μ(a,-) : A → A` is an
+[equivalence](foundation-core.equivalences.md) for every `a : A`. In other
+words, if multiplying by a fixed element on the left is always an equivalence.
+
+Left-invertibility appears as Definition 2.1(4) of {{#cite BCFR23}} in the
+context of [H-spaces](structured-types.h-spaces.md).
+
+## Definitions
+
+### The predicate of being a left invertible magma
+
+```agda
+module _
+  {l : Level} (A : Magma l)
+  where
+
+  is-left-invertible-Magma : UU l
+  is-left-invertible-Magma = (a : type-Magma A) → is-equiv (mul-Magma A a)
+
+  is-prop-is-left-invertible-Magma : is-prop is-left-invertible-Magma
+  is-prop-is-left-invertible-Magma =
+    is-prop-Π (λ a → is-property-is-equiv (mul-Magma A a))
+
+  is-left-invertible-prop-Magma : Prop l
+  is-left-invertible-prop-Magma =
+    ( is-left-invertible-Magma , is-prop-is-left-invertible-Magma)
+```
+
+## References
+
+{{#bibliography}}

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

@@ -11,9 +11,12 @@ open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.dependent-pair-types
+open import foundation.dependent-products-truncated-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 +143,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)

src/synthetic-homotopy-theory.lagda.md

@@ -103,6 +103,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

src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md

@@ -69,6 +69,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)
@@ -77,6 +83,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)