Central H-spaces

src/foundation-core/commuting-squares-of-homotopies.lagda.md

@@ -746,12 +746,12 @@ module _
       ( coh x)
       ( H x)
 
-  right-unwhisker-cohernece-square-homotopies :
+  right-unwhisker-concat-coherence-square-homotopies :
     {u : (x : A) → B x} (H : i ~ u) →
     coherence-square-homotopies top left (right ∙h H) (bottom ∙h H) →
     coherence-square-homotopies top left right bottom
-  right-unwhisker-cohernece-square-homotopies H coh x =
-    right-unwhisker-cohernece-square-identifications
+  right-unwhisker-concat-coherence-square-homotopies H coh x =
+    right-unwhisker-concat-coherence-square-identifications
       ( top x)
       ( left x)
       ( right x)

src/foundation-core/commuting-squares-of-identifications.lagda.md

@@ -700,11 +700,11 @@ module _
         ( inv right-unit)
         ( s))
 
-  right-unwhisker-cohernece-square-identifications :
+  right-unwhisker-concat-coherence-square-identifications :
     {u : A} (p : w ＝ u) →
     coherence-square-identifications top left (right ∙ p) (bottom ∙ p) →
     coherence-square-identifications top left right bottom
-  right-unwhisker-cohernece-square-identifications refl =
+  right-unwhisker-concat-coherence-square-identifications refl =
     ( inv-concat-right-identification-coherence-square-identifications
       ( top)
       ( left)

src/foundation.lagda.md

@@ -254,6 +254,8 @@ open import foundation.mere-embeddings public
 open import foundation.mere-equality public
 open import foundation.mere-equivalences public
 open import foundation.mere-functions public
+open import foundation.mere-homotopies public
+open import foundation.mere-identity-endomorphisms public
 open import foundation.mere-logical-equivalences public
 open import foundation.monomorphisms public
 open import foundation.morphisms-arrows public

src/foundation/connected-components.lagda.md

@@ -10,6 +10,7 @@ module foundation.connected-components where
 open import foundation.0-connected-types
 open import foundation.dependent-pair-types
 open import foundation.logical-equivalences
+open import foundation.mere-equality
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.universe-levels
@@ -60,7 +61,7 @@ module _
 
   connected-component : UU l
   connected-component =
-    Σ A (λ x → type-trunc-Prop (x ＝ a))
+    Σ A (mere-eq a)
 
   point-connected-component : connected-component
   pr1 point-connected-component = a
@@ -77,7 +78,7 @@ module _
   abstract
     mere-equality-connected-component :
       (X : connected-component) →
-      type-trunc-Prop (value-connected-component X ＝ a)
+      mere-eq a (value-connected-component X)
     mere-equality-connected-component X = pr2 X
 ```
 
@@ -96,11 +97,11 @@ abstract
       ( λ (x , p) →
         apply-universal-property-trunc-Prop
           ( p)
-          ( trunc-Prop ((a , unit-trunc-Prop refl) ＝ (x , p)))
+          ( mere-eq-Prop (a , unit-trunc-Prop refl) (x , p))
           ( λ p' →
             unit-trunc-Prop
               ( eq-pair-Σ
-                ( inv p')
+                ( p')
                 ( all-elements-equal-type-trunc-Prop _ p))))
 
 connected-component-∞-Group :

src/foundation/endomorphisms.lagda.md

@@ -20,18 +20,40 @@ open import foundation-core.sets
 open import group-theory.monoids
 open import group-theory.semigroups
 
+open import structured-types.h-spaces
 open import structured-types.wild-monoids
 ```
 
 </details>
 
 ## Idea
 
-An **endomorphism** on a type `A` is a map `A → A`.
+An {{#concept "endomorphism"}} on a type `A` is a function `A → A`. The type of
+endomorphisms on `A` an [H-space](structured-types.h-spaces.md). Note that the
+unit laws for function composition hold judgmentally, so
+[function extensionality](foundation.function-extensionality.md) is not required
+to establish the H-space structure on the type of endomorphisms `A → A`.
+Furthermore, since function composition is strictly associative, the type of
+endomorphisms `A → A` is also a [wild monoid](structured-types.wild-monoids.md).
 
 ## Properties
 
-### Endomorphisms form a monoid
+### The type of endomorphisms on any type is an H-space
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  endo-H-Space : H-Space l
+  pr1 endo-H-Space = endo-Pointed-Type A
+  pr1 (pr2 endo-H-Space) g f = g ∘ f
+  pr1 (pr2 (pr2 endo-H-Space)) f = refl
+  pr1 (pr2 (pr2 (pr2 endo-H-Space))) f = refl
+  pr2 (pr2 (pr2 (pr2 endo-H-Space))) = refl
+```
+
+### The type of endomorphisms form a wild monoid
 
 ```agda
 endo-Wild-Monoid : {l : Level} → UU l → Wild-Monoid l
@@ -45,12 +67,20 @@ pr1 (pr2 (pr2 (endo-Wild-Monoid A))) g f = refl
 pr1 (pr2 (pr2 (pr2 (endo-Wild-Monoid A)))) g f = refl
 pr1 (pr2 (pr2 (pr2 (pr2 (endo-Wild-Monoid A))))) g f = refl
 pr2 (pr2 (pr2 (pr2 (pr2 (endo-Wild-Monoid A))))) = star
+```
 
+### The type of endomorphisms on a set form a semigroup
+
+```agda
 endo-Semigroup : {l : Level} → Set l → Semigroup l
 pr1 (endo-Semigroup A) = endo-Set A
 pr1 (pr2 (endo-Semigroup A)) g f = g ∘ f
 pr2 (pr2 (endo-Semigroup A)) h g f = refl
+```
 
+### The type of endomorphisms on a set form a monoid
+
+```agda
 endo-Monoid : {l : Level} → Set l → Monoid l
 pr1 (endo-Monoid A) = endo-Semigroup A
 pr1 (pr2 (endo-Monoid A)) = id
@@ -62,3 +92,4 @@ pr2 (pr2 (pr2 (endo-Monoid A))) f = refl
 
 - For endomorphisms in a category see
   [`category-theory.endomorphisms-in-categories`](category-theory.endomorphisms-in-categories.md).
+- [Mere identity endomorphisms](foundation.mere-identity-endomorphisms.md)

src/foundation/mere-homotopies.lagda.md

@@ -0,0 +1,70 @@
+# Mere homotopies
+
+```agda
+module foundation.mere-homotopies where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.functoriality-propositional-truncation
+open import foundation.homotopies
+open import foundation.mere-equality
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "mere homotopy" Agda=mere-htpy}} between two dependent functions
+`f g : (a : A) → B a` is an element of the
+[propositional truncation](foundation.propositional-truncations.md)
+
+```text
+  ║ f ~ g ║₋₁
+```
+
+of the type of [homotopies](foundation-core.homotopies.md) between `f` and `g`.
+
+## Definitions
+
+### Mere homotopies
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f g : (x : A) → B x)
+  where
+
+  mere-htpy-Prop : Prop (l1 ⊔ l2)
+  mere-htpy-Prop = trunc-Prop (f ~ g)
+
+  mere-htpy : UU (l1 ⊔ l2)
+  mere-htpy = type-trunc-Prop (f ~ g)
+
+  is-prop-mere-htpy : is-prop mere-htpy
+  is-prop-mere-htpy = is-prop-type-trunc-Prop
+```
+
+## Properties
+
+### Two functions are merely homotopic if and only if they are merely equal
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f g : (x : A) → B x)
+  where
+
+  mere-eq-mere-htpy : mere-htpy f g → mere-eq f g
+  mere-eq-mere-htpy = map-trunc-Prop eq-htpy
+
+  mere-htpy-mere-eq : mere-eq f g → mere-htpy f g
+  mere-htpy-mere-eq = map-trunc-Prop htpy-eq
+
+  equiv-mere-htpy-mere-eq : mere-eq f g ≃ mere-htpy f g
+  equiv-mere-htpy-mere-eq = equiv-trunc-Prop equiv-funext
+```

src/foundation/mere-identity-endomorphisms.lagda.md

@@ -0,0 +1,56 @@
+# Mere identity endomorphisms
+
+```agda
+module foundation.mere-identity-endomorphisms where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.mere-homotopies
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [endomorphism](foundation-core.endomorphisms.md) `f : A → A` on a type `A` is
+said to be a
+{{#concept "mere identity endomorphism" Agda=mere-identity-endomorphism}} if it
+is [merely homotopic](foundation.mere-homotopies.md) to the
+[identity function](foundation-core.function-types.md).
+
+## Definitions
+
+### The predicate of being a mere identity endomorphism
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (f : A → A)
+  where
+
+  is-mere-identity-endomorphism-Prop : Prop l1
+  is-mere-identity-endomorphism-Prop = mere-htpy-Prop id f
+
+  is-mere-identity-endomorphism : UU l1
+  is-mere-identity-endomorphism = mere-htpy id f
+
+  is-prop-is-mere-identity-endomorphism :
+    is-prop is-mere-identity-endomorphism
+  is-prop-is-mere-identity-endomorphism = is-prop-mere-htpy id f
+```
+
+### Mere identity endomorphisms
+
+```agda
+module _
+  {l1 : Level} (A : UU l1)
+  where
+
+  mere-identity-endomorphism : UU l1
+  mere-identity-endomorphism = Σ (A → A) is-mere-identity-endomorphism
+```

src/group-theory/symmetric-concrete-groups.lagda.md

@@ -70,7 +70,7 @@ module _
     (X ＝ Y) ≃ equiv-classifying-type-symmetric-Concrete-Group X Y
   extensionality-classifying-type-symmetric-Concrete-Group X =
     extensionality-type-subtype
-      ( λ Y → mere-eq-Prop Y A)
+      ( mere-eq-Prop A)
       ( pr2 X)
       ( id-equiv)
       ( extensionality-Set (pr1 X))

src/structured-types.lagda.md

@@ -15,6 +15,7 @@ open import structured-types.commuting-squares-of-pointed-homotopies public
 open import structured-types.commuting-squares-of-pointed-maps public
 open import structured-types.commuting-triangles-of-pointed-maps public
 open import structured-types.conjugation-pointed-types public
+open import structured-types.connected-h-spaces public
 open import structured-types.constant-pointed-maps public
 open import structured-types.contractible-pointed-types public
 open import structured-types.cyclic-types public
@@ -45,6 +46,7 @@ open import structured-types.large-symmetric-globular-types public
 open import structured-types.large-transitive-globular-types public
 open import structured-types.magmas public
 open import structured-types.mere-equivalences-types-equipped-with-endomorphisms public
+open import structured-types.mere-units-h-spaces public
 open import structured-types.morphisms-h-spaces public
 open import structured-types.morphisms-magmas public
 open import structured-types.morphisms-pointed-arrows public