Cavallo's trick for H-spaces

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -1269,7 +1269,7 @@ module _
                     ( eq-counting-equivalence-class-R n)
                     ( eq-is-prop is-prop-type-trunc-Prop))) ∙
                 ( inv
-                  ( eq-tr-type-Ω
+                  ( eq-conjugation-tr-type-Ω
                     ( eq-pair-Σ
                       ( eq-counting-equivalence-class-R n)
                       ( eq-is-prop is-prop-type-trunc-Prop))

src/foundation-core/homotopies.lagda.md

@@ -315,10 +315,17 @@ Given a homotopy `H : f ~ g` we obtain a natural map `f x ＝ f y → g x ＝ g
 given by conjugation by `H`.
 
 ```agda
-conjugate-htpy :
+module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B}
-  (H : f ~ g) {x y : A} → f x ＝ f y → g x ＝ g y
-conjugate-htpy H {x} {y} p = inv (H x) ∙ (p ∙ H y)
+  (H : f ~ g) {x y : A}
+  where
+
+  conjugate-htpy : f x ＝ f y → g x ＝ g y
+  conjugate-htpy p = inv (H x) ∙ (p ∙ H y)
+
+  compute-conjugate-htpy-ap :
+    (p : x ＝ y) → conjugate-htpy (ap f p) ＝ ap g p
+  compute-conjugate-htpy-ap refl = left-inv (H x)
 ```
 
 ### Homotopies preserve the laws of the action on identity types

src/foundation-core/identity-types.lagda.md

@@ -251,6 +251,11 @@ module _
     {x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
     (p ∙ q) ∙ r ＝ p ∙ (q ∙ r)
   assoc refl q r = refl
+
+  inv-assoc :
+    {x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
+    p ∙ (q ∙ r) ＝ (p ∙ q) ∙ r
+  inv-assoc p q r = inv (assoc p q r)
 ```
 
 ### The unit laws for concatenation
@@ -504,7 +509,7 @@ module _
 
   is-injective-concat' :
     {x y z : A} (r : y ＝ z) {p q : x ＝ y} → p ∙ r ＝ q ∙ r → p ＝ q
-  is-injective-concat' refl s = (inv right-unit) ∙ (s ∙ right-unit)
+  is-injective-concat' refl s = inv right-unit ∙ s ∙ right-unit
 ```
 
 ## Equational reasoning

src/foundation/action-on-higher-identifications-functions.lagda.md

@@ -149,8 +149,8 @@ module _
       ( ap-comp g f q)
       ( (ap² g ∘ ap² f) α)
   compute-comp-ap² =
-    (horizontal-concat-Id² refl (inv (ap-comp (ap g) (ap f) α)) ∙
-      (nat-htpy (ap-comp g f) α))
+    ( horizontal-concat-Id² refl (inv (ap-comp (ap g) (ap f) α))) ∙
+    ( nat-htpy (ap-comp g f) α)
 ```
 
 ### The action of a constant function on higher identifications is constant

src/foundation/commuting-triangles-of-identifications.lagda.md

@@ -46,11 +46,11 @@ module _
 
   coherence-triangle-identifications :
     (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
-  coherence-triangle-identifications left right top = left ＝ top ∙ right
+  coherence-triangle-identifications left right top = (left ＝ top ∙ right)
 
   coherence-triangle-identifications' :
     (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
-  coherence-triangle-identifications' left right top = top ∙ right ＝ left
+  coherence-triangle-identifications' left right top = (top ∙ right ＝ left)
 ```
 
 ### The horizontally constant triangle of identifications

src/foundation/identity-types.lagda.md

@@ -21,6 +21,8 @@ open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.homotopies
+open import foundation-core.retractions
+open import foundation-core.sections
 ```
 
 </details>
@@ -58,6 +60,20 @@ mac-lane-pentagon :
 mac-lane-pentagon refl refl refl refl = refl
 ```
 
+### Conjugation by the right unit law
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  conjugate-right-unit :
+    {x y : A} {p q : x ＝ y} (s : p ＝ q) →
+    inv right-unit ∙ ap (_∙ refl) s ∙ right-unit ＝ s
+  conjugate-right-unit refl =
+    ap (_∙ right-unit) right-unit ∙ left-inv right-unit
+```
+
 ### The groupoidal operations on identity types are equivalences
 
 ```agda
@@ -180,10 +196,24 @@ module _
   where
 
   is-section-is-injective-concat :
-    {x y z : A} (p : x ＝ y) {q r : y ＝ z} (s : (p ∙ q) ＝ (p ∙ r)) →
-    ap (concat p z) (is-injective-concat p s) ＝ s
+    {x y z : A} (p : x ＝ y) {q r : y ＝ z} →
+    is-section (ap (concat p z)) (is-injective-concat p {q} {r})
   is-section-is-injective-concat refl refl = refl
 
+  is-retraction-is-injective-concat :
+    {x y z : A} (p : x ＝ y) {q r : y ＝ z} →
+    is-retraction (ap (concat p z)) (is-injective-concat p {q} {r})
+  is-retraction-is-injective-concat refl refl = refl
+
+  is-equiv-is-injective-concat :
+    {x y z : A} (p : x ＝ y) {q r : y ＝ z} →
+    is-equiv (is-injective-concat p {q} {r})
+  is-equiv-is-injective-concat {z = z} p =
+    is-equiv-is-invertible
+      ( ap (concat p z))
+      ( is-retraction-is-injective-concat p)
+      ( is-section-is-injective-concat p)
+
   cases-is-section-is-injective-concat' :
     {x y : A} {p q : x ＝ y} (s : p ＝ q) →
     ( ap
@@ -192,31 +222,46 @@ module _
     ( right-unit ∙ (s ∙ inv right-unit))
   cases-is-section-is-injective-concat' {p = refl} refl = refl
 
-  is-section-is-injective-concat' :
-    {x y z : A} (r : y ＝ z) {p q : x ＝ y} (s : (p ∙ r) ＝ (q ∙ r)) →
-    ap (concat' x r) (is-injective-concat' r s) ＝ s
-  is-section-is-injective-concat' refl s =
-    ( ap (λ u → ap (concat' _ refl) (is-injective-concat' refl u)) (inv α)) ∙
-    ( ( cases-is-section-is-injective-concat'
-        ( inv right-unit ∙ (s ∙ right-unit))) ∙
-      ( α))
-    where
-    α :
-      ( ( right-unit) ∙
-        ( ( inv right-unit ∙ (s ∙ right-unit)) ∙
-          ( inv right-unit))) ＝
-      ( s)
-    α =
-      ( ap
-        ( concat right-unit _)
-        ( ( assoc (inv right-unit) (s ∙ right-unit) (inv right-unit)) ∙
-          ( ( ap
-              ( concat (inv right-unit) _)
+  abstract
+    is-section-is-injective-concat' :
+      {x y z : A} (r : y ＝ z) {p q : x ＝ y} →
+      is-section (ap (concat' x r)) (is-injective-concat' r {p} {q})
+    is-section-is-injective-concat' refl {p} {q} s =
+      ( ap (λ u → ap (concat' _ refl) (is-injective-concat' refl u)) (inv α)) ∙
+      ( ( cases-is-section-is-injective-concat'
+          ( inv right-unit ∙ (s ∙ right-unit))) ∙
+        ( α))
+      where
+      α :
+        ( ( right-unit) ∙
+          ( ( inv right-unit ∙ (s ∙ right-unit)) ∙
+            ( inv right-unit))) ＝
+        ( s)
+      α =
+        ( ap
+          ( concat right-unit (q ∙ refl))
+          ( ( assoc (inv right-unit) (s ∙ right-unit) (inv right-unit)) ∙
+            ( ap
+              ( concat (inv right-unit) (q ∙ refl))
               ( ( assoc s right-unit (inv right-unit)) ∙
-                ( ( ap (concat s _) (right-inv right-unit)) ∙
-                  ( right-unit))))))) ∙
-      ( ( inv (assoc right-unit (inv right-unit) s)) ∙
-        ( ( ap (concat' _ s) (right-inv right-unit))))
+                ( ap (concat s (q ∙ refl)) (right-inv right-unit)) ∙
+                ( right-unit))))) ∙
+        ( inv (assoc right-unit (inv right-unit) s)) ∙
+        ( ( ap (concat' (p ∙ refl) s) (right-inv right-unit)))
+
+  is-retraction-is-injective-concat' :
+    {x y z : A} (r : y ＝ z) {p q : x ＝ y} →
+    is-retraction (ap (concat' x r)) (is-injective-concat' r {p} {q})
+  is-retraction-is-injective-concat' refl = conjugate-right-unit
+
+  is-equiv-is-injective-concat' :
+    {x y z : A} (r : y ＝ z) {p q : x ＝ y} →
+    is-equiv (is-injective-concat' r {p} {q})
+  is-equiv-is-injective-concat' {x} r =
+    is-equiv-is-invertible
+      ( ap (concat' x r))
+      ( is-retraction-is-injective-concat' r)
+      ( is-section-is-injective-concat' r)
 ```
 
 ### Applying the right unit law on one side of a higher identification is an equivalence

src/foundation/whiskering-identifications-concatenation.lagda.md

@@ -64,7 +64,7 @@ module _
     is-equiv-left-whisker-concat
 ```
 
-### Right whiskering of identification is an equivalence
+### Right whiskering of identifications is an equivalence
 
 ```agda
 module _
@@ -82,3 +82,35 @@ module _
   pr2 equiv-right-whisker-concat =
     is-equiv-right-whisker-concat
 ```
+
+### Left unwhiskering of identifications is an equivalence
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A} (p : x ＝ y) {q q' : y ＝ z}
+  where
+
+  is-equiv-left-unwhisker-concat :
+    is-equiv (λ (α : p ∙ q ＝ p ∙ q') → left-unwhisker-concat p α)
+  is-equiv-left-unwhisker-concat = is-equiv-is-injective-concat p
+
+  equiv-left-unwhisker-concat : (p ∙ q ＝ p ∙ q') ≃ (q ＝ q')
+  equiv-left-unwhisker-concat =
+    ( left-unwhisker-concat p , is-equiv-left-unwhisker-concat)
+```
+
+### Right unwhiskering of identifications is an equivalence
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A} {p p' : x ＝ y} (q : y ＝ z)
+  where
+
+  is-equiv-right-unwhisker-concat :
+    is-equiv (λ (α : p ∙ q ＝ p' ∙ q) → right-unwhisker-concat q α)
+  is-equiv-right-unwhisker-concat = is-equiv-is-injective-concat' q
+
+  equiv-right-unwhisker-concat : (p ∙ q ＝ p' ∙ q) ≃ (p ＝ p')
+  equiv-right-unwhisker-concat =
+    ( right-unwhisker-concat q , is-equiv-right-unwhisker-concat)
+```

src/higher-group-theory/conjugation.lagda.md

@@ -53,7 +53,7 @@ module _
   map-conjugation-∞-Group = map-hom-∞-Group G G conjugation-∞-Group
 
   compute-map-conjugation-∞-Group :
-    map-conjugation-Ω g ~ map-conjugation-∞-Group
+    conjugation-type-Ω g ~ map-conjugation-∞-Group
   compute-map-conjugation-∞-Group =
     htpy-compute-action-on-loops-conjugation-Pointed-Type
       ( g)

src/higher-group-theory/equivalences-higher-groups.lagda.md

@@ -57,7 +57,7 @@ module _
     pointed-equiv-equiv-∞-Group = pointed-equiv-Ω-pointed-equiv e
 
     equiv-equiv-∞-Group : type-∞-Group G ≃ type-∞-Group H
-    equiv-equiv-∞-Group = equiv-map-Ω-pointed-equiv e
+    equiv-equiv-∞-Group = equiv-Ω-pointed-equiv e
 ```
 
 ### The identity equivalence of higher groups

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

@@ -89,7 +89,7 @@ module _
 
   compute-action-on-loops-conjugation-Pointed-Type' :
     {u : type-Pointed-Type B} (p : point-Pointed-Type B ＝ u) →
-    conjugation-Ω' p ~∗ action-on-loops-conjugation-Pointed-Type p
+    tr-Ω p ~∗ action-on-loops-conjugation-Pointed-Type p
   pr1 (compute-action-on-loops-conjugation-Pointed-Type' refl) ω = inv (ap-id ω)
   pr2 (compute-action-on-loops-conjugation-Pointed-Type' refl) = refl
 
@@ -103,7 +103,7 @@ module _
 
   htpy-compute-action-on-loops-conjugation-Pointed-Type :
     {u : type-Pointed-Type B} (p : point-Pointed-Type B ＝ u) →
-    map-conjugation-Ω p ~ map-action-on-loops-conjugation-Pointed-Type p
+    conjugation-type-Ω p ~ map-action-on-loops-conjugation-Pointed-Type p
   htpy-compute-action-on-loops-conjugation-Pointed-Type p =
     pr1 (compute-action-on-loops-conjugation-Pointed-Type p)
 ```

src/structured-types/h-spaces.lagda.md

@@ -15,7 +15,9 @@ open import foundation.evaluation-functions
 open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.sections
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
@@ -73,7 +75,7 @@ using `make-H-Space`.
 ```agda
 H-Space : (l : Level) → UU (lsuc l)
 H-Space l =
-  Σ ( Pointed-Type l) coherent-unital-mul-Pointed-Type
+  Σ (Pointed-Type l) coherent-unital-mul-Pointed-Type
 
 make-H-Space :
   {l : Level} →
@@ -162,15 +164,19 @@ module _
 ```agda
 h-space-Noncoherent-H-Space :
   {l : Level} → Noncoherent-H-Space l → H-Space l
-pr1 (h-space-Noncoherent-H-Space A) = pointed-type-Noncoherent-H-Space A
-pr1 (pr2 (h-space-Noncoherent-H-Space A)) = mul-Noncoherent-H-Space A
+pr1 (h-space-Noncoherent-H-Space A) =
+  pointed-type-Noncoherent-H-Space A
+pr1 (pr2 (h-space-Noncoherent-H-Space A)) =
+  mul-Noncoherent-H-Space A
 pr2 (pr2 (h-space-Noncoherent-H-Space A)) =
   coherent-unit-laws-unit-laws
     ( mul-Noncoherent-H-Space A)
     ( unit-laws-mul-Noncoherent-H-Space A)
 ```
 
-### The type of H-space structures on `A` is equivalent to the type of sections of `ev-point : (A → A) →∗ A`
+### The type of H-space structures on `A` is equivalent to the type of sections of `ev-point : (A → A, id) →∗ A`
+
+This is Proposition 2.2 (1)⇔(2) {{#cite BCFR23}}.
 
 ```agda
 module _
@@ -189,10 +195,34 @@ module _
     pointed-section-ev-point-Pointed-Type ≃ coherent-unital-mul-Pointed-Type A
   compute-pointed-section-ev-point-Pointed-Type =
     ( equiv-tot
-      ( λ _ →
-        equiv-Σ _
+      ( λ x →
+        equiv-Σ
+          ( λ α →
+            Σ ( right-unit-law x (point-Pointed-Type A))
+              ( coh-unit-laws x (point-Pointed-Type A) α))
           ( equiv-funext)
-          ( λ _ →
-            equiv-tot (λ _ → inv-equiv (equiv-right-whisker-concat refl))))) ∘e
+          ( λ _ → equiv-tot (λ _ → equiv-right-unwhisker-concat refl)))) ∘e
     ( associative-Σ)
+
+module _
+  {l : Level} (A : H-Space l)
+  where
+
+  ev-endo-H-Space :
+    endo-Pointed-Type (type-H-Space A) →∗ pointed-type-H-Space A
+  ev-endo-H-Space = ev-endo-Pointed-Type (pointed-type-H-Space A)
+
+  pointed-section-ev-endo-H-Space : pointed-section ev-endo-H-Space
+  pointed-section-ev-endo-H-Space =
+    map-inv-equiv
+      ( compute-pointed-section-ev-point-Pointed-Type (pointed-type-H-Space A))
+      ( coherent-unital-mul-H-Space A)
+
+  section-ev-endo-H-Space : section (map-pointed-map ev-endo-H-Space)
+  section-ev-endo-H-Space =
+    section-pointed-section ev-endo-H-Space pointed-section-ev-endo-H-Space
 ```
+
+## References
+
+{{#bibliography}}

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

@@ -173,14 +173,23 @@ commutes.
 ```agda
 module _
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
-  (f g : pointed-Π A B) (G : unpointed-htpy-pointed-Π f g)
+  (f g : pointed-Π A B)
   where
 
-  coherence-point-unpointed-htpy-pointed-Π : UU l2
-  coherence-point-unpointed-htpy-pointed-Π =
+  coherence-point-unpointed-htpy-pointed-Π' :
+    function-pointed-Π f (point-Pointed-Type A) ＝
+    function-pointed-Π g (point-Pointed-Type A) →
+    UU l2
+  coherence-point-unpointed-htpy-pointed-Π' G =
     coherence-triangle-identifications
       ( preserves-point-function-pointed-Π f)
       ( preserves-point-function-pointed-Π g)
+      ( G)
+
+  coherence-point-unpointed-htpy-pointed-Π :
+    unpointed-htpy-pointed-Π f g → UU l2
+  coherence-point-unpointed-htpy-pointed-Π G =
+    coherence-point-unpointed-htpy-pointed-Π'
       ( G (point-Pointed-Type A))
 ```