diff --git a/src/foundation-core/binary-relations.lagda.md b/src/foundation-core/binary-relations.lagda.md
new file mode 100644
index 0000000000..a9f319735f
--- /dev/null
+++ b/src/foundation-core/binary-relations.lagda.md
@@ -0,0 +1,220 @@
+# Binary relations
+
+```agda
+module foundation-core.binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.iterated-dependent-product-types
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.negation
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+A {{#concept "binary relation" Agda=Relation}} on a type `A` is a family of types `R x y` depending on
+two variables `x y : A`. In the special case where each `R x y` is a
+[proposition](foundation-core.propositions.md), we say that the relation is
+valued in propositions. Thus, we take a general relation to mean a
+_proof-relevant_ relation.
+
+## Definition
+
+### Relations valued in types
+
+```agda
+Relation : {l1 : Level} (l : Level) (A : UU l1) → UU (l1 ⊔ lsuc l)
+Relation l A = A → A → UU l
+
+total-space-Relation :
+  {l1 l : Level} {A : UU l1} → Relation l A → UU (l1 ⊔ l)
+total-space-Relation {A = A} R = Σ (A × A) λ (a , a') → R a a'
+```
+
+### Relations valued in propositions
+
+```agda
+Relation-Prop :
+  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
+Relation-Prop l A = A → A → Prop l
+
+type-Relation-Prop :
+  {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Relation l2 A
+type-Relation-Prop R x y = pr1 (R x y)
+
+is-prop-type-Relation-Prop :
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) →
+  (x y : A) → is-prop (type-Relation-Prop R x y)
+is-prop-type-Relation-Prop R x y = pr2 (R x y)
+
+total-space-Relation-Prop :
+  {l : Level} {l1 : Level} {A : UU l1} → Relation-Prop l A → UU (l ⊔ l1)
+total-space-Relation-Prop {A = A} R =
+  Σ (A × A) λ (a , a') → type-Relation-Prop R a a'
+```
+
+### The predicate of being a reflexive relation
+
+A relation `R` on a type `A` is said to be **reflexive** if it comes equipped
+with a function `(x : A) → R x x`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-reflexive : UU (l1 ⊔ l2)
+  is-reflexive = (x : A) → R x x
+```
+
+### The predicate of being a reflexive relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **reflexive**
+if its underlying relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-reflexive-Relation-Prop : UU (l1 ⊔ l2)
+  is-reflexive-Relation-Prop = is-reflexive (type-Relation-Prop R)
+
+  is-prop-is-reflexive-Relation-Prop : is-prop is-reflexive-Relation-Prop
+  is-prop-is-reflexive-Relation-Prop =
+    is-prop-Π (λ x → is-prop-type-Relation-Prop R x x)
+```
+
+### The predicate of being a symmetric relation
+
+A relation `R` on a type `A` is said to be **symmetric** if it comes equipped
+with a function `(x y : A) → R x y → R y x`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-symmetric : UU (l1 ⊔ l2)
+  is-symmetric = (x y : A) → R x y → R y x
+```
+
+### The predicate of being a symmetric relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **symmetric**
+if its underlying relation is symmetric.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-symmetric-Relation-Prop : UU (l1 ⊔ l2)
+  is-symmetric-Relation-Prop = is-symmetric (type-Relation-Prop R)
+
+  is-prop-is-symmetric-Relation-Prop : is-prop is-symmetric-Relation-Prop
+  is-prop-is-symmetric-Relation-Prop =
+    is-prop-iterated-Π 3
+      ( λ x y r → is-prop-type-Relation-Prop R y x)
+```
+
+### The predicate of being a transitive relation
+
+A relation `R` on a type `A` is said to be **transitive** if it comes equipped
+with a function `(x y z : A) → R y z → R x y → R x z`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-transitive : UU (l1 ⊔ l2)
+  is-transitive = (x y z : A) → R y z → R x y → R x z
+```
+
+### The predicate of being a transitive relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **transitive**
+if its underlying relation is transitive.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-transitive-Relation-Prop : UU (l1 ⊔ l2)
+  is-transitive-Relation-Prop = is-transitive (type-Relation-Prop R)
+
+  is-prop-is-transitive-Relation-Prop : is-prop is-transitive-Relation-Prop
+  is-prop-is-transitive-Relation-Prop =
+    is-prop-iterated-Π 3
+      ( λ x y z →
+        is-prop-function-type
+          ( is-prop-function-type (is-prop-type-Relation-Prop R x z)))
+```
+
+### The predicate of being an irreflexive relation
+
+A relation `R` on a type `A` is said to be **irreflexive** if it comes equipped
+with a function `(x : A) → ¬ (R x y)`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-irreflexive : UU (l1 ⊔ l2)
+  is-irreflexive = (x : A) → ¬ (R x x)
+```
+
+### The predicate of being an asymmetric relation
+
+A relation `R` on a type `A` is said to be **asymmetric** if it comes equipped
+with a function `(x y : A) → R x y → ¬ (R y x)`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-asymmetric : UU (l1 ⊔ l2)
+  is-asymmetric = (x y : A) → R x y → ¬ (R y x)
+```
+
+### The predicate of being an antisymmetric relation
+
+A relation `R` on a type `A` is said to be **antisymmetric** if it comes
+equipped with a function `(x y : A) → R x y → R y x → x ＝ y`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-antisymmetric : UU (l1 ⊔ l2)
+  is-antisymmetric = (x y : A) → R x y → R y x → x ＝ y
+```
+
+### The predicate of being an antisymmetric relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be
+**antisymmetric** if its underlying relation is antisymmetric.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-antisymmetric-Relation-Prop : UU (l1 ⊔ l2)
+  is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R)
+```
+
diff --git a/src/foundation-core/commuting-squares-of-homotopies.lagda.md b/src/foundation-core/commuting-squares-of-homotopies.lagda.md
index 6ae7b583b4..17213f26df 100644
--- a/src/foundation-core/commuting-squares-of-homotopies.lagda.md
+++ b/src/foundation-core/commuting-squares-of-homotopies.lagda.md
@@ -840,12 +840,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)
diff --git a/src/foundation-core/commuting-squares-of-identifications.lagda.md b/src/foundation-core/commuting-squares-of-identifications.lagda.md
index 3c4058de82..f6924903a6 100644
--- a/src/foundation-core/commuting-squares-of-identifications.lagda.md
+++ b/src/foundation-core/commuting-squares-of-identifications.lagda.md
@@ -788,11 +788,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)
diff --git a/src/foundation-core/mere-equality.lagda.md b/src/foundation-core/mere-equality.lagda.md
new file mode 100644
index 0000000000..6cda68fc0a
--- /dev/null
+++ b/src/foundation-core/mere-equality.lagda.md
@@ -0,0 +1,74 @@
+# Mere equality
+
+```agda
+module foundation-core.mere-equality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation-core.binary-relations
+open import foundation.functoriality-propositional-truncation
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+Two elements in a type are said to be {{#concept "merely equal" Agda=mere-eq}} if there is an element of the
+[propositionally truncated](foundation.propositional-truncations.md) [identity type](foundation-core.identity-types.md) between them.
+
+## Definitions
+
+### Mere equality
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  mere-eq-Prop : A → A → Prop l
+  mere-eq-Prop x y = trunc-Prop (x ＝ y)
+
+  mere-eq : A → A → UU l
+  mere-eq x y = type-Prop (mere-eq-Prop x y)
+
+  is-prop-mere-eq : (x y : A) → is-prop (mere-eq x y)
+  is-prop-mere-eq x y = is-prop-type-trunc-Prop
+```
+
+## Properties
+
+### Reflexivity
+
+```agda
+refl-mere-eq :
+  {l : Level} {A : UU l} → is-reflexive (mere-eq {l} {A})
+refl-mere-eq _ = unit-trunc-Prop refl
+```
+
+### Symmetry
+
+```agda
+abstract
+  symmetric-mere-eq :
+    {l : Level} {A : UU l} → is-symmetric (mere-eq {l} {A})
+  symmetric-mere-eq _ _ = map-trunc-Prop inv
+```
+
+### Transitivity
+
+```agda
+abstract
+  transitive-mere-eq :
+    {l : Level} {A : UU l} → is-transitive (mere-eq {l} {A})
+  transitive-mere-eq x y z p q =
+    apply-universal-property-trunc-Prop q
+      ( mere-eq-Prop x z)
+      ( λ p' → map-trunc-Prop (p' ∙_) p)
+```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 760a6dda04..f107768667 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -257,6 +257,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.mere-path-cosplit-maps public
 open import foundation.monomorphisms public
diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md
index d2bdc9203d..71c3cbfde8 100644
--- a/src/foundation/0-connected-types.lagda.md
+++ b/src/foundation/0-connected-types.lagda.md
@@ -19,6 +19,7 @@ open import foundation.mere-equality
 open import foundation.propositional-truncations
 open import foundation.set-truncations
 open import foundation.sets
+open import foundation.subtypes
 open import foundation.surjective-maps
 open import foundation.unit-type
 open import foundation.universal-property-contractible-types
@@ -41,19 +42,83 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A type is said to be connected if its type of connected components, i.e., its
-set truncation, is contractible.
+A type is said to be {{#concept "0-connected" Agda=is-0-connected}} if its type
+of connected components, i.e., its
+[set truncation](foundation.set-truncations.md), is
+[contractible](foundation-core.contractible-types.md). Sometimes we simply say
+that a type is connected instead of saying that it is 0-connected.
+
+## Definitions
+
+### The predicate of being a `0`-connected type
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-0-connected-Prop : Prop l
+  is-0-connected-Prop = is-contr-Prop (type-trunc-Set A)
+
+  is-0-connected : UU l
+  is-0-connected = type-Prop is-0-connected-Prop
+
+  is-prop-is-0-connected : is-prop is-0-connected
+  is-prop-is-0-connected = is-prop-type-Prop is-0-connected-Prop
+```
+
+### The dependent universal property of pointed `0`-connected types
+
+The
+{{#concept "dependent universal property of `0`-connected types" Agda=dependent-universal-property-0-connected-type}}
+asserts that for any element `a` in a type `A` and any
+[subtype](foundation.subtypes.md) `P` of `A`, the evaluation map
+
+```text
+  ((x : A) → P x) → P a
+```
+
+is an equivalence. In other words, a type `A` with a given element `a` is
+`0`-connected precisely when any subtype contains all elements if and only if it
+contains the given element `a`.
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  ev-point-subtype :
+    {l2 : Level} (P : subtype l2 A) →
+    ((x : A) → is-in-subtype P x) → is-in-subtype P a
+  ev-point-subtype P f = f a
+
+  dependent-universal-property-0-connected-type : UUω
+  dependent-universal-property-0-connected-type =
+    {l : Level} (P : subtype l A) → is-equiv (ev-point-subtype P)
+```
+
+### The universal property of `0`-connected types
+
+The
+{{#concept "universal property of `0`-connected types" Agda=universal-property-0-connected-type}}
+asserts that maps from a type `A` equipped with a given element `a : A` into a
+[set](foundation-core.sets.md) `S` are uniquely determined by an element of `S`.
 
 ```agda
-is-0-connected-Prop : {l : Level} → UU l → Prop l
-is-0-connected-Prop A = is-contr-Prop (type-trunc-Set A)
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  universal-property-0-connected-type : UUω
+  universal-property-0-connected-type =
+    {l : Level} (S : Set l) → is-equiv (ev-point' a {type-Set S})
+```
 
-is-0-connected : {l : Level} → UU l → UU l
-is-0-connected A = type-Prop (is-0-connected-Prop A)
+## Properties
 
-is-prop-is-0-connected : {l : Level} (A : UU l) → is-prop (is-0-connected A)
-is-prop-is-0-connected A = is-prop-type-Prop (is-0-connected-Prop A)
+### `0`-connected types are inhabited
 
+```agda
 abstract
   is-inhabited-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → is-inhabited A
@@ -62,24 +127,36 @@ abstract
       ( center C)
       ( set-Prop (trunc-Prop A))
       ( unit-trunc-Prop)
+```
 
+### Any two elements in a `0`-connected type are merely equal
+
+```agda
 abstract
   mere-eq-is-0-connected :
     {l : Level} {A : UU l} → is-0-connected A → (x y : A) → mere-eq x y
   mere-eq-is-0-connected {A = A} H x y =
     apply-effectiveness-unit-trunc-Set (eq-is-contr H)
+```
+
+### A pointed type in which every element is merely equal to the base point is `0`-connected
 
+```agda
 abstract
   is-0-connected-mere-eq :
     {l : Level} {A : UU l} (a : A) →
     ((x : A) → mere-eq a x) → is-0-connected A
-  is-0-connected-mere-eq {l} {A} a e =
-    pair
-      ( unit-trunc-Set a)
-      ( apply-dependent-universal-property-trunc-Set'
-        ( λ x → set-Prop (Id-Prop (trunc-Set A) (unit-trunc-Set a) x))
-        ( λ x → apply-effectiveness-unit-trunc-Set' (e x)))
+  pr1 (is-0-connected-mere-eq {l} {A} a e) =
+    unit-trunc-Set a
+  pr2 (is-0-connected-mere-eq {l} {A} a e) =
+    apply-dependent-universal-property-trunc-Set'
+      ( λ x → set-Prop (Id-Prop (trunc-Set A) (unit-trunc-Set a) x))
+      ( λ x → apply-effectiveness-unit-trunc-Set' (e x))
+```
 
+### An inhabited type in which any two elements are merely equal is `0`-connected
+
+```agda
 abstract
   is-0-connected-mere-eq-is-inhabited :
     {l : Level} {A : UU l} →
@@ -88,17 +165,22 @@ abstract
     apply-universal-property-trunc-Prop H
       ( is-0-connected-Prop _)
       ( λ a → is-0-connected-mere-eq a (K a))
+```
+
+### The point inclusion of a given element of a type is surjective if and only if the type is `0`-connected
 
-is-0-connected-is-surjective-point :
-  {l1 : Level} {A : UU l1} (a : A) →
-  is-surjective (point a) → is-0-connected A
-is-0-connected-is-surjective-point a H =
-  is-0-connected-mere-eq a
-    ( λ x →
-      apply-universal-property-trunc-Prop
-        ( H x)
-        ( mere-eq-Prop a x)
-        ( λ u → unit-trunc-Prop (pr2 u)))
+```agda
+abstract
+  is-0-connected-is-surjective-point :
+    {l1 : Level} {A : UU l1} (a : A) →
+    is-surjective (point a) → is-0-connected A
+  is-0-connected-is-surjective-point a H =
+    is-0-connected-mere-eq a
+      ( λ x →
+        apply-universal-property-trunc-Prop
+          ( H x)
+          ( mere-eq-Prop a x)
+          ( λ u → unit-trunc-Prop (pr2 u)))
 
 abstract
   is-surjective-point-is-0-connected :
@@ -109,38 +191,75 @@ abstract
       ( mere-eq-is-0-connected H a x)
       ( trunc-Prop (fiber (point a) x))
       ( λ where refl → unit-trunc-Prop (star , refl))
+```
 
-is-trunc-map-ev-point-is-connected :
-  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
-  is-0-connected A → is-trunc (succ-𝕋 k) B →
-  is-trunc-map k (ev-point' a {B})
-is-trunc-map-ev-point-is-connected k {A} {B} a H K =
-  is-trunc-map-comp k
-    ( ev-point' star {B})
-    ( precomp (point a) B)
-    ( is-trunc-map-is-equiv k
-      ( universal-property-contr-is-contr star is-contr-unit B))
-    ( is-trunc-map-precomp-Π-is-surjective k
+### A pointed connected type `A` is `k + 1`-truncated if and only if the base point inclusion is `k`-truncated
+
+```agda
+abstract
+  is-trunc-map-ev-point-is-connected :
+    {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
+    is-0-connected A → is-trunc (succ-𝕋 k) B →
+    is-trunc-map k (ev-point' a {B})
+  is-trunc-map-ev-point-is-connected k {A} {B} a H K =
+    is-trunc-map-comp k
+      ( ev-point' star {B})
+      ( precomp (point a) B)
+      ( is-trunc-map-is-equiv k
+        ( universal-property-contr-is-contr star is-contr-unit B))
+      ( is-trunc-map-precomp-Π-is-surjective k
+        ( is-surjective-point-is-0-connected a H)
+        ( λ _ → (B , K)))
+```
+
+### The dependent universal property of `0`-connected types
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  abstract
+    is-0-connected-dependent-universal-property-0-connected-type :
+      dependent-universal-property-0-connected-type a →
+      is-0-connected A
+    is-0-connected-dependent-universal-property-0-connected-type H =
+      is-0-connected-mere-eq a
+        ( map-inv-is-equiv (H (mere-eq-Prop a)) (refl-mere-eq a))
+
+  abstract
+    dependent-universal-property-0-connected-type-is-0-connected :
+      is-0-connected A → dependent-universal-property-0-connected-type a
+    dependent-universal-property-0-connected-type-is-0-connected H P =
+      is-equiv-comp _ _
+        ( dependent-universal-property-surjection-is-surjective
+          ( point a)
+          ( is-surjective-point-is-0-connected a H)
+          ( P))
+        ( universal-property-unit (type-Prop (P a)))
+
+  equiv-dependent-universal-property-0-connected-type :
+    is-0-connected A →
+    ( {l : Level} (P : subtype l A) →
+      ((x : A) → is-in-subtype P x) ≃ is-in-subtype P a)
+  equiv-dependent-universal-property-0-connected-type H P =
+    ( equiv-universal-property-unit (type-Prop (P a))) ∘e
+    ( equiv-dependent-universal-property-surjection-is-surjective
+      ( point a)
       ( is-surjective-point-is-0-connected a H)
-      ( λ _ → (B , K)))
-
-equiv-dependent-universal-property-is-0-connected :
-  {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
-  ( {l : Level} (P : A → Prop l) →
-    ((x : A) → type-Prop (P x)) ≃ type-Prop (P a))
-equiv-dependent-universal-property-is-0-connected a H P =
-  ( equiv-universal-property-unit (type-Prop (P a))) ∘e
-  ( equiv-dependent-universal-property-surjection-is-surjective
-    ( point a)
-    ( is-surjective-point-is-0-connected a H)
-    ( P))
-
-apply-dependent-universal-property-is-0-connected :
-  {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
-  {l : Level} (P : A → Prop l) → type-Prop (P a) → (x : A) → type-Prop (P x)
-apply-dependent-universal-property-is-0-connected a H P =
-  map-inv-equiv (equiv-dependent-universal-property-is-0-connected a H P)
+      ( P))
+
+  abstract
+    apply-dependent-universal-property-0-connected-type :
+      {l2 : Level} → is-0-connected A → (P : subtype l2 A) →
+      is-in-subtype P a → (x : A) → is-in-subtype P x
+    apply-dependent-universal-property-0-connected-type H P =
+      map-inv-equiv (equiv-dependent-universal-property-0-connected-type H P)
+```
+
+### A pointed type is connected if and only if the fiber inclusion is surjective for any type family over it
 
+```agda
 abstract
   is-surjective-fiber-inclusion :
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
@@ -169,16 +288,22 @@ abstract
     is-0-connected A
   is-0-connected-is-surjective-fiber-inclusion a H =
     is-0-connected-mere-eq a (mere-eq-is-surjective-fiber-inclusion a H)
+```
 
-is-0-connected-equiv :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
-  (A ≃ B) → is-0-connected B → is-0-connected A
-is-0-connected-equiv e = is-contr-equiv _ (equiv-trunc-Set e)
+### `0`-connected types are closed under equivalences
 
-is-0-connected-equiv' :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
-  (A ≃ B) → is-0-connected A → is-0-connected B
-is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e)
+```agda
+abstract
+  is-0-connected-equiv :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    (A ≃ B) → is-0-connected B → is-0-connected A
+  is-0-connected-equiv e = is-contr-equiv _ (equiv-trunc-Set e)
+
+abstract
+  is-0-connected-equiv' :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    (A ≃ B) → is-0-connected A → is-0-connected B
+  is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e)
 ```
 
 ### `0`-connected types are closed under cartesian products
@@ -209,11 +334,14 @@ abstract
 ### A contractible type is `0`-connected
 
 ```agda
-is-0-connected-is-contr :
-  {l : Level} (X : UU l) →
-  is-contr X → is-0-connected X
-is-0-connected-is-contr X p =
-  is-contr-equiv X (inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p))) p
+abstract
+  is-0-connected-is-contr :
+    {l : Level} (X : UU l) →
+    is-contr X → is-0-connected X
+  is-0-connected-is-contr X p =
+    is-contr-equiv X
+      ( inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p)))
+      ( p)
 ```
 
 ### The image of a function with a `0`-connected domain is `0`-connected
diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md
index 0fc607dc0b..f61d9977e5 100644
--- a/src/foundation/binary-relations.lagda.md
+++ b/src/foundation/binary-relations.lagda.md
@@ -2,6 +2,8 @@
 
 ```agda
 module foundation.binary-relations where
+
+open import foundation-core.binary-relations public
 ```
 
 <details><summary>Imports</summary>
@@ -28,203 +30,12 @@ open import foundation-core.torsorial-type-families
 
 ## Idea
 
-A **binary relation** on a type `A` is a family of types `R x y` depending on
+A {{#concept "binary relation" Agda=Relation}} on a type `A` is a family of types `R x y` depending on
 two variables `x y : A`. In the special case where each `R x y` is a
 [proposition](foundation-core.propositions.md), we say that the relation is
 valued in propositions. Thus, we take a general relation to mean a
 _proof-relevant_ relation.
 
-## Definition
-
-### Relations valued in types
-
-```agda
-Relation : {l1 : Level} (l : Level) (A : UU l1) → UU (l1 ⊔ lsuc l)
-Relation l A = A → A → UU l
-
-total-space-Relation :
-  {l1 l : Level} {A : UU l1} → Relation l A → UU (l1 ⊔ l)
-total-space-Relation {A = A} R = Σ (A × A) λ (a , a') → R a a'
-```
-
-### Relations valued in propositions
-
-```agda
-Relation-Prop :
-  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
-Relation-Prop l A = A → A → Prop l
-
-type-Relation-Prop :
-  {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Relation l2 A
-type-Relation-Prop R x y = pr1 (R x y)
-
-is-prop-type-Relation-Prop :
-  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) →
-  (x y : A) → is-prop (type-Relation-Prop R x y)
-is-prop-type-Relation-Prop R x y = pr2 (R x y)
-
-total-space-Relation-Prop :
-  {l : Level} {l1 : Level} {A : UU l1} → Relation-Prop l A → UU (l ⊔ l1)
-total-space-Relation-Prop {A = A} R =
-  Σ (A × A) λ (a , a') → type-Relation-Prop R a a'
-```
-
-### The predicate of being a reflexive relation
-
-A relation `R` on a type `A` is said to be **reflexive** if it comes equipped
-with a function `(x : A) → R x x`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-reflexive : UU (l1 ⊔ l2)
-  is-reflexive = (x : A) → R x x
-```
-
-### The predicate of being a reflexive relation valued in propositions
-
-A relation `R` on a type `A` valued in propositions is said to be **reflexive**
-if its underlying relation is reflexive
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
-  where
-
-  is-reflexive-Relation-Prop : UU (l1 ⊔ l2)
-  is-reflexive-Relation-Prop = is-reflexive (type-Relation-Prop R)
-
-  is-prop-is-reflexive-Relation-Prop : is-prop is-reflexive-Relation-Prop
-  is-prop-is-reflexive-Relation-Prop =
-    is-prop-Π (λ x → is-prop-type-Relation-Prop R x x)
-```
-
-### The predicate of being a symmetric relation
-
-A relation `R` on a type `A` is said to be **symmetric** if it comes equipped
-with a function `(x y : A) → R x y → R y x`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-symmetric : UU (l1 ⊔ l2)
-  is-symmetric = (x y : A) → R x y → R y x
-```
-
-### The predicate of being a symmetric relation valued in propositions
-
-A relation `R` on a type `A` valued in propositions is said to be **symmetric**
-if its underlying relation is symmetric.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
-  where
-
-  is-symmetric-Relation-Prop : UU (l1 ⊔ l2)
-  is-symmetric-Relation-Prop = is-symmetric (type-Relation-Prop R)
-
-  is-prop-is-symmetric-Relation-Prop : is-prop is-symmetric-Relation-Prop
-  is-prop-is-symmetric-Relation-Prop =
-    is-prop-iterated-Π 3
-      ( λ x y r → is-prop-type-Relation-Prop R y x)
-```
-
-### The predicate of being a transitive relation
-
-A relation `R` on a type `A` is said to be **transitive** if it comes equipped
-with a function `(x y z : A) → R y z → R x y → R x z`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-transitive : UU (l1 ⊔ l2)
-  is-transitive = (x y z : A) → R y z → R x y → R x z
-```
-
-### The predicate of being a transitive relation valued in propositions
-
-A relation `R` on a type `A` valued in propositions is said to be **transitive**
-if its underlying relation is transitive.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
-  where
-
-  is-transitive-Relation-Prop : UU (l1 ⊔ l2)
-  is-transitive-Relation-Prop = is-transitive (type-Relation-Prop R)
-
-  is-prop-is-transitive-Relation-Prop : is-prop is-transitive-Relation-Prop
-  is-prop-is-transitive-Relation-Prop =
-    is-prop-iterated-Π 3
-      ( λ x y z →
-        is-prop-function-type
-          ( is-prop-function-type (is-prop-type-Relation-Prop R x z)))
-```
-
-### The predicate of being an irreflexive relation
-
-A relation `R` on a type `A` is said to be **irreflexive** if it comes equipped
-with a function `(x : A) → ¬ (R x y)`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-irreflexive : UU (l1 ⊔ l2)
-  is-irreflexive = (x : A) → ¬ (R x x)
-```
-
-### The predicate of being an asymmetric relation
-
-A relation `R` on a type `A` is said to be **asymmetric** if it comes equipped
-with a function `(x y : A) → R x y → ¬ (R y x)`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-asymmetric : UU (l1 ⊔ l2)
-  is-asymmetric = (x y : A) → R x y → ¬ (R y x)
-```
-
-### The predicate of being an antisymmetric relation
-
-A relation `R` on a type `A` is said to be **antisymmetric** if it comes
-equipped with a function `(x y : A) → R x y → R y x → x ＝ y`.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-antisymmetric : UU (l1 ⊔ l2)
-  is-antisymmetric = (x y : A) → R x y → R y x → x ＝ y
-```
-
-### The predicate of being an antisymmetric relation valued in propositions
-
-A relation `R` on a type `A` valued in propositions is said to be
-**antisymmetric** if its underlying relation is antisymmetric.
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
-  where
-
-  is-antisymmetric-Relation-Prop : UU (l1 ⊔ l2)
-  is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R)
-```
-
 ## Properties
 
 ### Characterization of equality of binary relations
diff --git a/src/foundation/connected-components.lagda.md b/src/foundation/connected-components.lagda.md
index c719f53bf2..d99aa4ae94 100644
--- a/src/foundation/connected-components.lagda.md
+++ b/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-core.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 :
diff --git a/src/foundation/endomorphisms.lagda.md b/src/foundation/endomorphisms.lagda.md
index 178d2f3786..e3ed8337db 100644
--- a/src/foundation/endomorphisms.lagda.md
+++ b/src/foundation/endomorphisms.lagda.md
@@ -20,6 +20,7 @@ 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
 ```
 
@@ -27,11 +28,32 @@ open import structured-types.wild-monoids
 
 ## 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` is 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)
diff --git a/src/foundation/mere-equality.lagda.md b/src/foundation/mere-equality.lagda.md
index c36b3c92e0..8af884dd22 100644
--- a/src/foundation/mere-equality.lagda.md
+++ b/src/foundation/mere-equality.lagda.md
@@ -2,6 +2,8 @@
 
 ```agda
 module foundation.mere-equality where
+
+open import foundation-core.mere-equality public
 ```
 
 <details><summary>Imports</summary>
@@ -17,7 +19,6 @@ open import foundation.universe-levels
 
 open import foundation-core.equivalence-relations
 open import foundation-core.identity-types
-open import foundation-core.propositions
 open import foundation-core.sets
 ```
 
@@ -25,58 +26,11 @@ open import foundation-core.sets
 
 ## Idea
 
-Two elements in a type are said to be merely equal if there is an element of the
-propositionally truncated identity type between them.
-
-## Definition
-
-```agda
-module _
-  {l : Level} {A : UU l}
-  where
-
-  mere-eq-Prop : A → A → Prop l
-  mere-eq-Prop x y = trunc-Prop (x ＝ y)
-
-  mere-eq : A → A → UU l
-  mere-eq x y = type-Prop (mere-eq-Prop x y)
-
-  is-prop-mere-eq : (x y : A) → is-prop (mere-eq x y)
-  is-prop-mere-eq x y = is-prop-type-trunc-Prop
-```
+Two elements in a type are said to be {{#concept "merely equal" Agda=mere-eq}} if there is an element of the
+[propositionally truncated](foundation.propositional-truncations.md) [identity type](foundation-core.identity-types.md) between them.
 
 ## Properties
 
-### Reflexivity
-
-```agda
-abstract
-  refl-mere-eq :
-    {l : Level} {A : UU l} → is-reflexive (mere-eq {l} {A})
-  refl-mere-eq _ = unit-trunc-Prop refl
-```
-
-### Symmetry
-
-```agda
-abstract
-  symmetric-mere-eq :
-    {l : Level} {A : UU l} → is-symmetric (mere-eq {l} {A})
-  symmetric-mere-eq _ _ = map-trunc-Prop inv
-```
-
-### Transitivity
-
-```agda
-abstract
-  transitive-mere-eq :
-    {l : Level} {A : UU l} → is-transitive (mere-eq {l} {A})
-  transitive-mere-eq x y z p q =
-    apply-universal-property-trunc-Prop q
-      ( mere-eq-Prop x z)
-      ( λ p' → map-trunc-Prop (p' ∙_) p)
-```
-
 ### Mere equality is an equivalence relation
 
 ```agda
@@ -109,15 +63,3 @@ module _
   pr1 reflecting-map-mere-eq = f
   pr2 reflecting-map-mere-eq = reflects-mere-eq
 ```
-
-### If mere equality maps into the identity type of `A`, then `A` is a set
-
-```agda
-is-set-mere-eq-in-id :
-  {l : Level} {A : UU l} → ((x y : A) → mere-eq x y → x ＝ y) → is-set A
-is-set-mere-eq-in-id =
-  is-set-prop-in-id
-    ( mere-eq)
-    ( is-prop-mere-eq)
-    ( refl-mere-eq)
-```
diff --git a/src/foundation/mere-equivalences.lagda.md b/src/foundation/mere-equivalences.lagda.md
index 663c8f4d24..d9d317631b 100644
--- a/src/foundation/mere-equivalences.lagda.md
+++ b/src/foundation/mere-equivalences.lagda.md
@@ -10,7 +10,7 @@ module foundation.mere-equivalences where
 open import foundation.binary-relations
 open import foundation.decidable-equality
 open import foundation.functoriality-propositional-truncation
-open import foundation.mere-equality
+open import foundation-core.mere-equality
 open import foundation.propositional-truncations
 open import foundation.univalence
 open import foundation.universe-levels
diff --git a/src/foundation/mere-homotopies.lagda.md b/src/foundation/mere-homotopies.lagda.md
new file mode 100644
index 0000000000..c338b98e82
--- /dev/null
+++ b/src/foundation/mere-homotopies.lagda.md
@@ -0,0 +1,185 @@
+# Mere homotopies
+
+```agda
+module foundation.mere-homotopies where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.0-connected-types
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalence-relations
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.functoriality-propositional-truncation
+open import foundation.homotopies
+open import foundation-core.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
+```
+
+### The mere homotopy component of a function type
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  mere-htpy-component : UU (l1 ⊔ l2)
+  mere-htpy-component = Σ ((x : A) → B x) (mere-htpy f)
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f : (x : A) → B x}
+  (g : mere-htpy-component f)
+  where
+
+  map-mere-htpy-component : (x : A) → B x
+  map-mere-htpy-component = pr1 g
+
+  mere-htpy-base-function-mere-htpy-component :
+    mere-htpy f map-mere-htpy-component
+  mere-htpy-base-function-mere-htpy-component = pr2 g
+```
+
+## Properties
+
+### The mere homotopy relation is an equivalence relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  abstract
+    refl-mere-htpy : (f : (x : A) → B x) → mere-htpy f f
+    refl-mere-htpy f = unit-trunc-Prop refl-htpy
+
+  abstract
+    transitive-mere-htpy :
+      is-transitive (mere-htpy {B = B})
+    transitive-mere-htpy f g h r s =
+      apply-twice-universal-property-trunc-Prop r s
+        ( mere-htpy-Prop f h)
+        ( λ H K → unit-trunc-Prop (K ∙h H))
+
+  abstract
+    symmetric-mere-htpy : is-symmetric (mere-htpy {B = B})
+    symmetric-mere-htpy f g r =
+      apply-universal-property-trunc-Prop r
+        ( mere-htpy-Prop g f)
+        ( λ H → unit-trunc-Prop (inv-htpy H))
+
+  mere-htpy-Equivalence-Relation :
+    equivalence-relation (l1 ⊔ l2) ((x : A) → B x)
+  pr1 mere-htpy-Equivalence-Relation = mere-htpy-Prop
+  pr1 (pr2 mere-htpy-Equivalence-Relation) = refl-mere-htpy
+  pr1 (pr2 (pr2 mere-htpy-Equivalence-Relation)) = symmetric-mere-htpy
+  pr2 (pr2 (pr2 mere-htpy-Equivalence-Relation)) = transitive-mere-htpy
+```
+
+### 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
+
+  abstract
+    mere-eq-mere-htpy : mere-htpy f g → mere-eq f g
+    mere-eq-mere-htpy = map-trunc-Prop eq-htpy
+
+  abstract
+    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
+```
+
+### The base function of a mere homotopy component
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  base-function-mere-htpy-component : mere-htpy-component f
+  pr1 base-function-mere-htpy-component = f
+  pr2 base-function-mere-htpy-component = refl-mere-htpy f
+```
+
+### Any two elements functions in a mere homotopy component are merely homotopy
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  abstract
+    mere-htpy-mere-htpy-component :
+      (g h : mere-htpy-component f) →
+      mere-htpy (map-mere-htpy-component g) (map-mere-htpy-component h)
+    mere-htpy-mere-htpy-component g h =
+      transitive-mere-htpy
+        ( map-mere-htpy-component g)
+        ( f)
+        ( map-mere-htpy-component h)
+        ( mere-htpy-base-function-mere-htpy-component h)
+        ( symmetric-mere-htpy f
+          ( map-mere-htpy-component g)
+          ( mere-htpy-base-function-mere-htpy-component g))
+```
+
+### The mere homotopy component of any function is connected
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  abstract
+    is-0-connected-mere-htpy-component : is-0-connected (mere-htpy-component f)
+    is-0-connected-mere-htpy-component =
+      is-0-connected-mere-eq
+        ( base-function-mere-htpy-component f)
+        ( λ (g , H) →
+          {!!})
+```
+
+### The mere homotopy component of a function is an ∞-group
diff --git a/src/foundation/mere-identity-endomorphisms.lagda.md b/src/foundation/mere-identity-endomorphisms.lagda.md
new file mode 100644
index 0000000000..44fb40576a
--- /dev/null
+++ b/src/foundation/mere-identity-endomorphisms.lagda.md
@@ -0,0 +1,114 @@
+# 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
+
+open import foundation-core.equivalences
+```
+
+</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
+
+  module _
+    {e : mere-identity-endomorphism}
+    where
+
+    endomorphism-mere-identity-endomorphism : A → A
+    endomorphism-mere-identity-endomorphism = pr1 e
+
+    is-mere-identity-mere-identity-endomorphism :
+      is-mere-identity-endomorphism endomorphism-mere-identity-endomorphism
+    is-mere-identity-mere-identity-endomorphism = pr2 e
+```
+
+### The predicate of being a mere identity automorphism
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (e : A ≃ A)
+  where
+
+  is-mere-identity-automorphism-Prop : Prop l1
+  is-mere-identity-automorphism-Prop = mere-htpy-Prop id (map-equiv e)
+
+  is-mere-identity-automorphism : UU l1
+  is-mere-identity-automorphism = mere-htpy id (map-equiv e)
+
+  is-prop-is-mere-identity-automorphism :
+    is-prop is-mere-identity-automorphism
+  is-prop-is-mere-identity-automorphism = is-prop-mere-htpy id (map-equiv e)
+```
+
+### Mere identity automorphisms
+
+```agda
+module _
+  {l1 : Level} (A : UU l1)
+  where
+
+  mere-identity-automorphism : UU l1
+  mere-identity-automorphism = Σ (A ≃ A) is-mere-identity-automorphism
+
+  module _
+    {e : mere-identity-automorphism}
+    where
+
+    automorphism-mere-identity-automorphism : A ≃ A
+    automorphism-mere-identity-automorphism = pr1 e
+
+    is-mere-identity-mere-identity-automorphism :
+      is-mere-identity-automorphism automorphism-mere-identity-automorphism
+    is-mere-identity-mere-identity-automorphism = pr2 e
+```
+
+## Properties
+
+### The type of mere identity endomorphisms is connected
+
diff --git a/src/foundation/mere-identity-systems.lagda.md b/src/foundation/mere-identity-systems.lagda.md
new file mode 100644
index 0000000000..4d2e06c066
--- /dev/null
+++ b/src/foundation/mere-identity-systems.lagda.md
@@ -0,0 +1,275 @@
+# Mere identity systems
+
+```agda
+module foundation.mere-identity-systems where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.0-connected-types
+open import foundation.binary-relations
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-systems
+open import foundation-core.identity-types
+open import foundation.logical-equivalences
+open import foundation-core.mere-equality
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.set-truncations
+open import foundation.subtypes
+open import foundation.torsorial-type-families
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+There are two kinds of mere identity systems: unary and binary mere identity systems.
+
+### Unary mere identity systems
+
+A [subtype](foundation.subtypes.md) `P : A → Prop` containing an element `a : A` is said to be a unary {{#concept "mere identity system" Disambiguation="unary"}} if for every `Q : (x : A) → P x → Prop` the evaluation map at the witness `ρ : P a`
+
+```text
+  ((x : A) (p : P x) → Q x p) → Q a ρ
+```
+
+is an [equivalence](foundation-core.equivalences.md). The following conditions are equivalent to being a unary mere identity system
+
+1. The underlying type of `P` is [`0`-connected](foundation.0-connected-types.md).
+2. The subtype `P` contains the same elements as the subtype of all elements [merely equal](foundation.mere-equality.md) to `a`.
+3. The evaluation map
+
+   ```text
+     ((x : A) → P x → Q x) → Q a
+   ```
+
+   is an equivalence for every subtype `Q : A → Prop`. In this case we say that `P` is the {{#concept "least subtype containing a given element"}} `a`.
+
+### Binary mere identity systems
+
+A reflexive [binary relation](foundation.binary-relations.md) `R : A → A → Prop` valued in [foundation-core.propositions.md) is said to be a binary {{#concept "mere identity system" Disambiguation="binary"}} if for every `S : (x y : A) → R x y → Prop` the evaluation map at the reflexivity element `ρ`
+
+```text
+  ((x y : A) (r : R x y) → S x y r) → S a a (ρ a)
+```
+
+is an [equivalence](foundation-core.equivalences.md) for every element `a : A`. The following conditions are equivalent to being a binary mere identity system
+
+1. The [total space](foundation.dependent-pair-types.md) `Σ A (R a)` is [`0`-connected](foundation.0-connected-types.md) for every element `a : A`.
+2. The relation `R` relates the same elements as the [mere equality relation](foundation.mere-equality.md).
+3. The evaluation map
+
+   ```text
+     ((x y : A) → R x y → S x y) → S a a
+   ```
+
+   is an equivalence for every binary relation `S : A → A → Prop`.
+4. The subtype `R a : A → Prop` is a unary mere identitity system for every `a : A`.
+
+## Definitions
+
+### The predicate of being a unary mere identity system
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A) {a : A} (ρ : is-in-subtype P a)
+  where
+
+  ev-element-subtype :
+    {l : Level} (Q : (x : A) → is-in-subtype P x → Prop l) →
+    ((x : A) (p : is-in-subtype P x) → is-in-subtype (Q x) p) →
+    is-in-subtype (Q a) ρ
+  ev-element-subtype Q f = f a ρ
+
+  is-mere-identity-system-subtype : UUω
+  is-mere-identity-system-subtype =
+    {l : Level} (Q : (x : A) → is-in-subtype P x → Prop l) →
+    is-equiv (ev-element-subtype Q)
+
+  ind-mere-identity-system-subtype :
+    is-mere-identity-system-subtype →
+    {l : Level} (Q : (x : A) → is-in-subtype P x → Prop l) →
+    type-Prop (Q a ρ) → (x : A) (p : is-in-subtype P x) → type-Prop (Q x p)
+  ind-mere-identity-system-subtype H Q =
+    map-inv-is-equiv (H Q)
+
+  rec-mere-identity-system-subtype :
+    is-mere-identity-system-subtype →
+    {l : Level} (Q : subtype l A) →
+    is-in-subtype Q a → (x : A) → is-in-subtype P x → is-in-subtype Q x
+  rec-mere-identity-system-subtype H Q =
+    ind-mere-identity-system-subtype H (λ x _ → Q x)
+```
+
+### The predicate of being a `0`-connected subtype
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A)
+  where
+
+  is-0-connected-prop-subtype : Prop (l1 ⊔ l2)
+  is-0-connected-prop-subtype = is-0-connected-Prop (type-subtype P)
+
+  is-0-connected-subtype : UU (l1 ⊔ l2)
+  is-0-connected-subtype = type-Prop is-0-connected-prop-subtype
+
+  is-prop-is-0-connected-subtype : is-prop is-0-connected-subtype
+  is-prop-is-0-connected-subtype = is-prop-type-Prop is-0-connected-prop-subtype
+```
+
+### The predicate of being the least subtype containing an element
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A) {a : A} (ρ : is-in-subtype P a)
+  where
+
+  is-least-subtype-containing-element : UUω
+  is-least-subtype-containing-element =
+    {l : Level} (Q : subtype l A) →
+    is-equiv (ev-element-subtype P ρ (λ x _ → Q x))
+```
+
+### The predicate of being a binary mere identity system
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  (ρ : is-reflexive-Relation-Prop R)
+  where
+
+  ev-refl-Reflexive-Relation-Prop :
+    {l : Level} (S : (x y : A) → subtype l (type-Relation-Prop R x y)) →
+    ((x y : A) (r : type-Relation-Prop R x y) → is-in-subtype (S x y) r) →
+    (x : A) → is-in-subtype (S x x) (ρ x)
+  ev-refl-Reflexive-Relation-Prop S f x = f x x (ρ x)
+
+  is-mere-identity-system-Reflexive-Relation-Prop : UUω
+  is-mere-identity-system-Reflexive-Relation-Prop =
+    {l : Level} (S : (x y : A) → subtype l (type-Relation-Prop R x y)) →
+    is-equiv (ev-refl-Reflexive-Relation-Prop S)
+```
+
+### The predicate of being the least reflexive relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  (ρ : is-reflexive-Relation-Prop R)
+  where
+
+  is-least-Reflexive-Relation-Prop : UUω
+  is-least-Reflexive-Relation-Prop =
+    {l : Level} (S : Relation-Prop l A) →
+    is-equiv (ev-refl-Reflexive-Relation-Prop R ρ (λ x y _ → S x y))
+```
+
+## Properties
+
+### Any unary identity system is a `0`-connected subtype
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A) {a : A} (ρ : is-in-subtype P a)
+  where
+
+  is-0-connected-is-mere-identity-system-subtype :
+    is-mere-identity-system-subtype P ρ → is-0-connected-subtype P
+  is-0-connected-is-mere-identity-system-subtype H =
+    is-0-connected-dependent-universal-property-0-connected-type
+      ( a , ρ)
+      ( λ Q → is-equiv-comp _ _ is-equiv-ev-pair (H (λ x y → Q (x , y))))
+```
+
+### The extension of a unary mere identity system to the set truncation is an identity system
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A) {a : A} (ρ : is-in-subtype P a)
+  (H : is-mere-identity-system-subtype P ρ)
+  where
+
+  abstract
+    is-torsorial-extension-trunc-set-subtype-is-mere-identity-system :
+      is-torsorial (is-in-extension-trunc-set-subtype P)
+    is-torsorial-extension-trunc-set-subtype-is-mere-identity-system =
+      is-contr-equiv'
+        ( type-trunc-Set (type-subtype P))
+        ( compute-type-extension-trunc-set-subtype P)
+        ( is-0-connected-is-mere-identity-system-subtype P ρ H)
+
+  abstract
+    is-identity-system-extension-trunc-set-subtype-is-mere-identity-system :
+      is-identity-system
+        ( is-in-extension-trunc-set-subtype P)
+        ( unit-trunc-Set a)
+        ( is-in-extension-trunc-set-is-in-subtype P a ρ)
+    is-identity-system-extension-trunc-set-subtype-is-mere-identity-system =
+      is-identity-system-is-torsorial
+        ( unit-trunc-Set a)
+        ( is-in-extension-trunc-set-is-in-subtype P a ρ)
+        ( is-torsorial-extension-trunc-set-subtype-is-mere-identity-system)
+```
+
+### Mere equality is a mere identity system
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  abstract
+    is-mere-identity-system-mere-eq :
+      is-mere-identity-system-subtype (mere-eq-Prop a) (refl-mere-eq a)
+    is-mere-identity-system-mere-eq P =
+      is-equiv-has-converse-is-prop
+        ( is-prop-Π (λ x → is-prop-Π (is-prop-is-in-subtype (P x))))
+        ( is-prop-is-in-subtype (P a) (refl-mere-eq a))
+        ( λ p x → ind-trunc-Prop (P x) (λ where refl → p))
+
+  abstract
+    ind-mere-identity-system-mere-eq :
+      {l : Level} (P : (x : A) → mere-eq a x → Prop l) →
+      (p : type-Prop (P a (refl-mere-eq a))) →
+      (x : A) (r : mere-eq a x) → type-Prop (P x r)
+    ind-mere-identity-system-mere-eq =
+      ind-mere-identity-system-subtype
+        ( mere-eq-Prop a)
+        ( refl-mere-eq a)
+        ( is-mere-identity-system-mere-eq)
+
+  abstract
+    rec-mere-identity-system-mere-eq :
+      {l : Level} (P : subtype l A) →
+      (p : is-in-subtype P a) (x : A) (r : mere-eq a x) → is-in-subtype P x
+    rec-mere-identity-system-mere-eq =
+      rec-mere-identity-system-subtype
+        ( mere-eq-Prop a)
+        ( refl-mere-eq a)
+        ( is-mere-identity-system-mere-eq)
+```
+
+### Any unary mere identity system has the same elements as the subtype of elements merely equal to the base point
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A) {a : A} (ρ : is-in-subtype P a)
+  (H : is-mere-identity-system-subtype P ρ)
+  where
+
+  has-same-elements-mere-eq-is-mere-identity-system-subtype :
+    has-same-elements-subtype (mere-eq-Prop a) P
+  pr1 (has-same-elements-mere-eq-is-mere-identity-system-subtype x) =
+    rec-mere-identity-system-mere-eq a P ρ x
+  pr2 (has-same-elements-mere-eq-is-mere-identity-system-subtype x) =
+    rec-mere-identity-system-subtype P ρ H (mere-eq-Prop a) (refl-mere-eq a) x
+```
diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md
index 154cc2d2b5..59215c0e2e 100644
--- a/src/foundation/set-truncations.lagda.md
+++ b/src/foundation/set-truncations.lagda.md
@@ -9,16 +9,23 @@ module foundation.set-truncations where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.effective-maps-equivalence-relations
 open import foundation.equality-coproduct-types
+open import foundation.function-extensionality
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
+open import foundation.logical-equivalences
 open import foundation.mere-equality
 open import foundation.postcomposition-functions
+open import foundation.propositional-extensionality
 open import foundation.reflecting-maps-equivalence-relations
+open import foundation.retractions
+open import foundation.sections
 open import foundation.sets
 open import foundation.slice
+open import foundation.subtypes
 open import foundation.surjective-maps
 open import foundation.truncations
 open import foundation.uniqueness-set-truncations
@@ -567,3 +574,169 @@ module _
   triangle-distributive-trunc-product-Set =
     pr2 (center distributive-trunc-product-Set)
 ```
+
+### Extending subtypes to set truncations
+
+Any subtype `P` of `A` extends to a subtype `P̃` of the set truncation of `A`. Futhermore, the underlying type of the extension of `P` to the set truncation of `A` is the set truncation of the underlying type of `P`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : subtype l2 A)
+  where
+
+  extension-trunc-set-subtype : subtype l2 (type-trunc-Set A)
+  extension-trunc-set-subtype =
+    map-universal-property-trunc-Set (Prop-Set l2) P
+
+  is-in-extension-trunc-set-subtype : type-trunc-Set A → UU l2
+  is-in-extension-trunc-set-subtype =
+    is-in-subtype extension-trunc-set-subtype
+
+  abstract
+    compute-extension-trunc-set-subtype :
+      has-same-elements-subtype P (extension-trunc-set-subtype ∘ unit-trunc-Set)
+    compute-extension-trunc-set-subtype x =
+      iff-eq (inv (triangle-universal-property-trunc-Set (Prop-Set l2) P x))
+
+  abstract
+    is-in-extension-trunc-set-is-in-subtype :
+      P ⊆ extension-trunc-set-subtype ∘ unit-trunc-Set
+    is-in-extension-trunc-set-is-in-subtype x =
+      forward-implication (compute-extension-trunc-set-subtype x)
+
+  abstract
+    is-in-subtype-is-in-extension-trunc-set-subtype :
+      extension-trunc-set-subtype ∘ unit-trunc-Set ⊆ P
+    is-in-subtype-is-in-extension-trunc-set-subtype x =
+      backward-implication (compute-extension-trunc-set-subtype x)
+
+  map-compute-type-extension-trunc-set-subtype :
+    type-trunc-Set (type-subtype P) → type-subtype extension-trunc-set-subtype
+  map-compute-type-extension-trunc-set-subtype =
+    map-universal-property-trunc-Set
+      ( set-subset (trunc-Set A) extension-trunc-set-subtype)
+      ( map-Σ
+        ( is-in-extension-trunc-set-subtype)
+        ( unit-trunc-Set)
+        ( is-in-extension-trunc-set-is-in-subtype))
+
+  abstract
+    triangle-map-compute-type-extension-trunc-set-subtype :
+      map-compute-type-extension-trunc-set-subtype ∘ unit-trunc-Set ~
+      map-Σ
+        ( is-in-extension-trunc-set-subtype)
+        ( unit-trunc-Set)
+        ( is-in-extension-trunc-set-is-in-subtype)
+    triangle-map-compute-type-extension-trunc-set-subtype =
+      triangle-universal-property-trunc-Set
+        ( set-subset (trunc-Set A) extension-trunc-set-subtype)
+        ( map-Σ
+          ( is-in-extension-trunc-set-subtype)
+          ( unit-trunc-Set)
+          ( is-in-extension-trunc-set-is-in-subtype))
+
+  map-inv-compute-type-extension-trunc-set-subtype :
+    type-subtype extension-trunc-set-subtype → type-trunc-Set (type-subtype P)
+  map-inv-compute-type-extension-trunc-set-subtype (x , p) =
+    function-dependent-universal-property-trunc-Set
+      ( λ y →
+        function-Set
+          ( is-in-extension-trunc-set-subtype y)
+          ( trunc-Set (type-subtype P)))
+      ( λ y q →
+        unit-trunc-Set
+          ( y , is-in-subtype-is-in-extension-trunc-set-subtype y q))
+      ( x)
+      ( p)
+
+  abstract
+    triangle-map-inv-compute-type-extension-trunc-set-subtype :
+      ( x : A) →
+      ev-pair
+        ( map-inv-compute-type-extension-trunc-set-subtype)
+        ( unit-trunc-Set x) ~
+      ( λ q →
+        unit-trunc-Set
+          ( x , is-in-subtype-is-in-extension-trunc-set-subtype x q))
+    triangle-map-inv-compute-type-extension-trunc-set-subtype x =
+      htpy-eq
+        ( compute-dependent-universal-property-trunc-Set
+          ( λ y →
+            function-Set
+              ( is-in-extension-trunc-set-subtype y)
+              ( trunc-Set (type-subtype P)))
+          ( λ y q →
+            unit-trunc-Set
+              ( y , is-in-subtype-is-in-extension-trunc-set-subtype y q))
+          ( x))
+
+  abstract
+    is-section-map-inv-compute-type-extension-trunc-set-subtype :
+      is-section
+        ( map-compute-type-extension-trunc-set-subtype)
+        ( map-inv-compute-type-extension-trunc-set-subtype)
+    is-section-map-inv-compute-type-extension-trunc-set-subtype (x , p) =
+      function-dependent-universal-property-trunc-Set
+        ( λ y →
+          Π-Set'
+            ( is-in-extension-trunc-set-subtype y)
+            ( λ q →
+              set-Prop
+                ( Id-Prop
+                  ( set-subset (trunc-Set A) extension-trunc-set-subtype)
+                  ( map-compute-type-extension-trunc-set-subtype
+                    ( map-inv-compute-type-extension-trunc-set-subtype
+                      ( y , q)))
+                  ( y , q))))
+        ( λ y q →
+          eq-type-subtype
+            ( extension-trunc-set-subtype)
+            ( ap
+              ( inclusion-subtype extension-trunc-set-subtype)
+              ( ( ap
+                  ( map-compute-type-extension-trunc-set-subtype)
+                  ( triangle-map-inv-compute-type-extension-trunc-set-subtype
+                    y q)) ∙
+                ( triangle-map-compute-type-extension-trunc-set-subtype
+                  ( y , is-in-subtype-is-in-extension-trunc-set-subtype y q)))))
+        ( x)
+        ( p)
+
+  abstract
+    is-retraction-map-inv-compute-type-extension-trunc-set-subtype :
+      is-retraction
+        ( map-compute-type-extension-trunc-set-subtype)
+        ( map-inv-compute-type-extension-trunc-set-subtype)
+    is-retraction-map-inv-compute-type-extension-trunc-set-subtype =
+      apply-dependent-universal-property-trunc-Set'
+        ( λ y →
+          set-Prop
+            ( Id-Prop
+              ( trunc-Set (type-subtype P))
+              ( map-inv-compute-type-extension-trunc-set-subtype
+                ( map-compute-type-extension-trunc-set-subtype y))
+              ( y)))
+        ( λ (y , q) →
+          ( ap
+            ( map-inv-compute-type-extension-trunc-set-subtype)
+            ( triangle-map-compute-type-extension-trunc-set-subtype (y , q))) ∙
+          ( ( triangle-map-inv-compute-type-extension-trunc-set-subtype y
+              ( is-in-extension-trunc-set-is-in-subtype y q)) ∙
+            ( ap unit-trunc-Set (eq-type-subtype P refl))))
+
+  abstract
+    is-equiv-map-compute-type-extension-trunc-set-subtype :
+      is-equiv map-compute-type-extension-trunc-set-subtype
+    is-equiv-map-compute-type-extension-trunc-set-subtype =
+      is-equiv-is-invertible
+        ( map-inv-compute-type-extension-trunc-set-subtype)
+        ( is-section-map-inv-compute-type-extension-trunc-set-subtype)
+        ( is-retraction-map-inv-compute-type-extension-trunc-set-subtype)
+
+  compute-type-extension-trunc-set-subtype :
+    type-trunc-Set (type-subtype P) ≃ type-subtype extension-trunc-set-subtype
+  pr1 compute-type-extension-trunc-set-subtype =
+    map-compute-type-extension-trunc-set-subtype
+  pr2 compute-type-extension-trunc-set-subtype =
+    is-equiv-map-compute-type-extension-trunc-set-subtype
+```
diff --git a/src/foundation/sets.lagda.md b/src/foundation/sets.lagda.md
index 32edfb667b..015741d33d 100644
--- a/src/foundation/sets.lagda.md
+++ b/src/foundation/sets.lagda.md
@@ -23,6 +23,7 @@ open import foundation-core.embeddings
 open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
+open import foundation-core.mere-equality
 open import foundation-core.precomposition-functions
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
@@ -219,6 +220,18 @@ abstract
   is-set-emb = is-trunc-emb neg-one-𝕋
 ```
 
+### If mere equality maps into the identity type of `A`, then `A` is a set
+
+```agda
+is-set-mere-eq-in-id :
+  {l : Level} {A : UU l} → ((x y : A) → mere-eq x y → x ＝ y) → is-set A
+is-set-mere-eq-in-id =
+  is-set-prop-in-id
+    ( mere-eq)
+    ( is-prop-mere-eq)
+    ( refl-mere-eq)
+```
+
 ### Any function from a proposition into a set is an embedding
 
 ```agda
diff --git a/src/foundation/subtypes.lagda.md b/src/foundation/subtypes.lagda.md
index b181a9a10d..754b54ab55 100644
--- a/src/foundation/subtypes.lagda.md
+++ b/src/foundation/subtypes.lagda.md
@@ -23,6 +23,7 @@ open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
+open import foundation-core.mere-equality
 open import foundation-core.propositions
 open import foundation-core.sets
 open import foundation-core.torsorial-type-families
diff --git a/src/group-theory/homomorphisms-concrete-group-actions.lagda.md b/src/group-theory/homomorphisms-concrete-group-actions.lagda.md
index 62057b8e87..f3e3c4d3e7 100644
--- a/src/group-theory/homomorphisms-concrete-group-actions.lagda.md
+++ b/src/group-theory/homomorphisms-concrete-group-actions.lagda.md
@@ -81,7 +81,7 @@ module _
     (g : hom-action-Concrete-Group G X Y) →
     (f ＝ g) ≃ htpy-hom-action-Concrete-Group g
   extensionality-hom-action-Concrete-Group g =
-    ( equiv-dependent-universal-property-is-0-connected
+    ( equiv-dependent-universal-property-0-connected-type
       ( shape-Concrete-Group G)
       ( is-0-connected-classifying-type-Concrete-Group G)
       ( λ u →
diff --git a/src/group-theory/symmetric-concrete-groups.lagda.md b/src/group-theory/symmetric-concrete-groups.lagda.md
index 006ef44e03..6d6ef57b1f 100644
--- a/src/group-theory/symmetric-concrete-groups.lagda.md
+++ b/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))
diff --git a/src/higher-group-theory/cartesian-products-higher-groups.lagda.md b/src/higher-group-theory/cartesian-products-higher-groups.lagda.md
index 2183bb2862..7f4ebf570e 100644
--- a/src/higher-group-theory/cartesian-products-higher-groups.lagda.md
+++ b/src/higher-group-theory/cartesian-products-higher-groups.lagda.md
@@ -77,7 +77,7 @@ module _
     type-Prop (P shape-product-∞-Group) →
     ((X : classifying-type-product-∞-Group) → type-Prop (P X))
   elim-prop-classifying-type-product-∞-Group =
-    apply-dependent-universal-property-is-0-connected
+    apply-dependent-universal-property-0-connected-type
       shape-product-∞-Group
       is-0-connected-classifying-type-product-∞-Group
 
diff --git a/src/higher-group-theory/higher-groups.lagda.md b/src/higher-group-theory/higher-groups.lagda.md
index 6102d85536..658430400e 100644
--- a/src/higher-group-theory/higher-groups.lagda.md
+++ b/src/higher-group-theory/higher-groups.lagda.md
@@ -92,7 +92,7 @@ module _
       type-Prop (P shape-∞-Group) →
       ((X : classifying-type-∞-Group) → type-Prop (P X))
     elim-prop-classifying-type-∞-Group =
-      apply-dependent-universal-property-is-0-connected
+      apply-dependent-universal-property-0-connected-type
         shape-∞-Group
         is-0-connected-classifying-type-∞-Group
 
diff --git a/src/higher-group-theory/iterated-cartesian-products-higher-groups.lagda.md b/src/higher-group-theory/iterated-cartesian-products-higher-groups.lagda.md
index e9a5b7aaab..53a99878eb 100644
--- a/src/higher-group-theory/iterated-cartesian-products-higher-groups.lagda.md
+++ b/src/higher-group-theory/iterated-cartesian-products-higher-groups.lagda.md
@@ -92,7 +92,7 @@ module _
     ((X : classifying-type-iterated-product-∞-Group) →
     type-Prop (P X))
   elim-prop-classifying-type-iterated-product-∞-Group =
-    apply-dependent-universal-property-is-0-connected
+    apply-dependent-universal-property-0-connected-type
       shape-iterated-product-∞-Group
       is-0-connected-classifying-type-iterated-product-∞-Group
 
diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md
index 6e6a4705ee..770dcb507c 100644
--- a/src/structured-types.lagda.md
+++ b/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
@@ -47,6 +48,7 @@ open import structured-types.magmas public
 open import structured-types.maps-globular-types public
 open import structured-types.maps-large-globular-types 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
diff --git a/src/structured-types/central-h-spaces.lagda.md b/src/structured-types/central-h-spaces.lagda.md
index c0ea967513..eb956e8b0b 100644
--- a/src/structured-types/central-h-spaces.lagda.md
+++ b/src/structured-types/central-h-spaces.lagda.md
@@ -7,9 +7,21 @@ module structured-types.central-h-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.0-connected-types
+open import foundation.cartesian-product-types
+open import foundation.connected-components
+open import foundation.dependent-pair-types
+open import foundation.endomorphisms
 open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.mere-identity-endomorphisms
+open import foundation.sets
 open import foundation.universe-levels
 
+open import structured-types.connected-h-spaces
+open import structured-types.h-spaces
+open import structured-types.pointed-maps
 open import structured-types.pointed-types
 ```
 
@@ -22,23 +34,172 @@ type of H-space structures on a
 [pointed type](structured-types.pointed-types.md) `A` is equivalently described
 as the type of [pointed sections](structured-types.pointed-types.md) of the
 pointed evaluation map `(A → A) →∗ A`. If the type `A` is
-[connected](foundation.connected-types.md), then the section maps to the
+[0-connected](foundation.0-connected-types.md), then the section maps to the
 [connected component](foundation.connected-components.md) of `(A ≃ A)` at the
-identity [equivalence](foundation-core.equivalences.md). An **evaluative
-H-space** is a pointed type such that the map `ev_pt : (A ≃ A)_{(id)} → A` is an
-equivalence.
+identity [equivalence](foundation-core.equivalences.md). Now the question arises
+for which H-spaces this evaluation map `(A → A) →∗ A` is an equivalence. This
+leads to the concept of _central H-space_.
 
-## Definition
+A {{#concept "central pointed type" agda=Central-Pointed-Type}} is a
+[pointed type](structured-types.pointed-types.md) such that the map
+`ev_pt : (A → A)_{(id)} → A` from the connected component of the identity
+function is an equivalence. Note that every type of [mere identity endomorphisms](foundation.mere-identity-endomorphisms.md) is an H-space, and therefore it follows that every central pointed type is also an H-space.
+
+## Definitions
+
+### The predicate of being a central pointed type
 
 ```agda
-is-central-h-space :
+is-central-Pointed-Type :
   {l : Level} (A : Pointed-Type l) → UU l
-is-central-h-space A =
+is-central-Pointed-Type A =
   is-equiv
-    { A = type-Pointed-Type A → type-Pointed-Type A}
-    ( ev-point-Pointed-Type A)
+    { A = mere-identity-endomorphism (type-Pointed-Type A)}
+    ( ev-point-Pointed-Type A ∘ pr1)
 ```
 
-## References
+### Central pointed types
+
+```agda
+Central-Pointed-Type : (l : Level) → UU (lsuc l)
+Central-Pointed-Type l = Σ (Pointed-Type l) is-central-Pointed-Type
+
+module _
+  {l : Level} (A : Central-Pointed-Type l)
+  where
+
+  pointed-type-Central-Pointed-Type : Pointed-Type l
+  pointed-type-Central-Pointed-Type = pr1 A
+
+  type-Central-Pointed-Type : UU l
+  type-Central-Pointed-Type =
+    type-Pointed-Type pointed-type-Central-Pointed-Type
+
+  point-Central-Pointed-Type : type-Central-Pointed-Type
+  point-Central-Pointed-Type =
+    point-Pointed-Type pointed-type-Central-Pointed-Type
+
+  is-central-Central-Pointed-Type :
+    is-central-Pointed-Type pointed-type-Central-Pointed-Type
+  is-central-Central-Pointed-Type = pr2 A
+
+  ev-point-Central-Pointed-Type :
+    mere-identity-endomorphism type-Central-Pointed-Type →
+    type-Central-Pointed-Type
+  ev-point-Central-Pointed-Type =
+    ev-point-Pointed-Type pointed-type-Central-Pointed-Type ∘ pr1
+
+  ev-point-equiv-Central-Pointed-Type :
+    mere-identity-endomorphism type-Central-Pointed-Type ≃
+    type-Central-Pointed-Type
+  pr1 ev-point-equiv-Central-Pointed-Type = ev-point-Central-Pointed-Type
+  pr2 ev-point-equiv-Central-Pointed-Type = is-central-Central-Pointed-Type
+```
+
+### The predicate of being a central H-space
+
+```agda
+module _
+  {l : Level} (A : H-Space l)
+  where
+
+  is-central-H-Space : UU l
+  is-central-H-Space =
+    is-0-connected-H-Space A ×
+    is-set (pointed-type-H-Space A →∗ pointed-type-H-Space A)
+
+  is-0-connected-is-central-H-Space :
+    is-central-H-Space → is-0-connected-H-Space A
+  is-0-connected-is-central-H-Space = pr1
+
+  is-set-pointed-endomap-is-central-H-Space :
+    is-central-H-Space →
+    is-set (pointed-type-H-Space A →∗ pointed-type-H-Space A)
+  is-set-pointed-endomap-is-central-H-Space = pr2
+```
+
+### Central H-spaces
+
+```agda
+Central-H-Space :
+  (l : Level) → UU (lsuc l)
+Central-H-Space l = Σ (H-Space l) is-central-H-Space
+
+module _
+  {l : Level} (A : Central-H-Space l)
+  where
+
+  h-space-Central-H-Space : H-Space l
+  h-space-Central-H-Space = pr1 A
+
+  pointed-type-Central-H-Space : Pointed-Type l
+  pointed-type-Central-H-Space =
+    pointed-type-H-Space h-space-Central-H-Space
+
+  type-Central-H-Space : UU l
+  type-Central-H-Space = type-H-Space h-space-Central-H-Space
+
+  unit-Central-H-Space : type-Central-H-Space
+  unit-Central-H-Space = unit-H-Space h-space-Central-H-Space
+
+  mul-Central-H-Space :
+    (x y : type-Central-H-Space) → type-Central-H-Space
+  mul-Central-H-Space = mul-H-Space h-space-Central-H-Space
+
+  left-unit-law-mul-Central-H-Space :
+    (x : type-Central-H-Space) →
+    mul-Central-H-Space unit-Central-H-Space x ＝ x
+  left-unit-law-mul-Central-H-Space =
+    left-unit-law-mul-H-Space h-space-Central-H-Space
+
+  right-unit-law-mul-Central-H-Space :
+    (x : type-Central-H-Space) →
+    mul-Central-H-Space x unit-Central-H-Space ＝ x
+  right-unit-law-mul-Central-H-Space =
+    right-unit-law-mul-H-Space h-space-Central-H-Space
+
+  coh-unit-laws-mul-Central-H-Space :
+    left-unit-law-mul-Central-H-Space unit-Central-H-Space ＝
+    right-unit-law-mul-Central-H-Space unit-Central-H-Space
+  coh-unit-laws-mul-Central-H-Space =
+    coh-unit-laws-mul-H-Space h-space-Central-H-Space
+
+  is-central-Central-H-Space :
+    is-central-H-Space h-space-Central-H-Space
+  is-central-Central-H-Space = pr2 A
+
+  is-0-connected-Central-H-Space :
+    is-0-connected-H-Space h-space-Central-H-Space
+  is-0-connected-Central-H-Space =
+    is-0-connected-is-central-H-Space
+      ( h-space-Central-H-Space)
+      ( is-central-Central-H-Space)
+
+  is-set-pointed-endomap-Central-H-Space :
+    is-set (pointed-type-Central-H-Space →∗ pointed-type-Central-H-Space)
+  is-set-pointed-endomap-Central-H-Space =
+    is-set-pointed-endomap-is-central-H-Space
+      ( h-space-Central-H-Space)
+      ( is-central-Central-H-Space)
+```
+
+## Properties
+
+### Central pointed types are connected
+
+```agda
+module _
+  {l1 : Level} (A : Central-Pointed-Type l1)
+  where
+
+  is-0-connected-Central-Pointed-Type :
+    is-0-connected (type-Central-Pointed-Type A)
+  is-0-connected-Central-Pointed-Type =
+    is-0-connected-equiv'
+      ( ev-point-equiv-Central-Pointed-Type A)
+      ( is-0-connected-connected-component
+        ( type-Central-Pointed-Type A → type-Central-Pointed-Type A)
+        ( id))
+```
 
 {{#bibliography}} {{#reference BCFR23}}
diff --git a/src/structured-types/connected-h-spaces.lagda.md b/src/structured-types/connected-h-spaces.lagda.md
new file mode 100644
index 0000000000..6dc3dcd03c
--- /dev/null
+++ b/src/structured-types/connected-h-spaces.lagda.md
@@ -0,0 +1,232 @@
+# Connected H-spaces
+
+```agda
+module structured-types.connected-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.0-connected-types
+open import foundation.binary-equivalences
+open import foundation.connected-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.truncation-levels
+open import foundation.universe-levels
+
+open import structured-types.h-spaces
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "connected H-space" Agda=Connected-H-Space}} is an
+[H-space](structured-types.h-spaces.md) of which the underlying type is
+[0-connected](foundation.0-connected-types.md). The binary operation
+`μ : A → A → A` of any connected H-space `A` is a
+[binary equivalence](foundation.binary-equivalences.md). This means that the
+maps
+
+```text
+  x ↦ μ x y : A → A        and         y ↦ μ x y : A → A
+```
+
+are [equivalences](foundation-core.equivalences.md) for any `x` and `y` in `A`.
+Furthermore, the [connected component](foundation.connected-components.md) of
+the unit element of an H-space is always a connected H-space. We will prove this
+fact in the file about [mere units](structured-types.mere-units-h-spaces.md).
+
+## Definitions
+
+### The predicate of being a connected H-space
+
+```agda
+module _
+  {l1 : Level} (k : 𝕋) (A : H-Space l1)
+  where
+
+  is-connected-prop-H-Space : Prop l1
+  is-connected-prop-H-Space = is-connected-Prop k (type-H-Space A)
+
+  is-connected-H-Space : UU l1
+  is-connected-H-Space = is-connected k (type-H-Space A)
+
+  is-prop-is-connected-H-Space : is-prop is-connected-H-Space
+  is-prop-is-connected-H-Space = is-prop-is-connected k (type-H-Space A)
+```
+
+### The predicate of being a 0-connected H-space
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  is-0-connected-prop-H-Space : Prop l1
+  is-0-connected-prop-H-Space = is-0-connected-Prop (type-H-Space A)
+
+  is-0-connected-H-Space : UU l1
+  is-0-connected-H-Space = is-0-connected (type-H-Space A)
+
+  is-prop-is-0-connected-H-Space : is-prop is-0-connected-H-Space
+  is-prop-is-0-connected-H-Space = is-prop-is-0-connected (type-H-Space A)
+```
+
+### The type of connected H-spaces
+
+```agda
+Connected-H-Space : (l : Level) (k : 𝕋) → UU (lsuc l)
+Connected-H-Space l k = Σ (H-Space l) (is-connected-H-Space k)
+
+module _
+  {l : Level} {k : 𝕋} (A : Connected-H-Space l k)
+  where
+
+  h-space-Connected-H-Space : H-Space l
+  h-space-Connected-H-Space = pr1 A
+
+  pointed-type-Connected-H-Space : Pointed-Type l
+  pointed-type-Connected-H-Space =
+    pointed-type-H-Space h-space-Connected-H-Space
+
+  type-Connected-H-Space : UU l
+  type-Connected-H-Space = type-H-Space h-space-Connected-H-Space
+
+  unit-Connected-H-Space : type-Connected-H-Space
+  unit-Connected-H-Space = unit-H-Space h-space-Connected-H-Space
+
+  mul-Connected-H-Space :
+    (x y : type-Connected-H-Space) → type-Connected-H-Space
+  mul-Connected-H-Space = mul-H-Space h-space-Connected-H-Space
+
+  left-unit-law-mul-Connected-H-Space :
+    (x : type-Connected-H-Space) →
+    mul-Connected-H-Space unit-Connected-H-Space x ＝ x
+  left-unit-law-mul-Connected-H-Space =
+    left-unit-law-mul-H-Space h-space-Connected-H-Space
+
+  right-unit-law-mul-Connected-H-Space :
+    (x : type-Connected-H-Space) →
+    mul-Connected-H-Space x unit-Connected-H-Space ＝ x
+  right-unit-law-mul-Connected-H-Space =
+    right-unit-law-mul-H-Space h-space-Connected-H-Space
+
+  coh-unit-laws-mul-Connected-H-Space :
+    left-unit-law-mul-Connected-H-Space unit-Connected-H-Space ＝
+    right-unit-law-mul-Connected-H-Space unit-Connected-H-Space
+  coh-unit-laws-mul-Connected-H-Space =
+    coh-unit-laws-mul-H-Space h-space-Connected-H-Space
+
+  is-connected-Connected-H-Space :
+    is-connected-H-Space k h-space-Connected-H-Space
+  is-connected-Connected-H-Space = pr2 A
+```
+
+### The type of 0-connected H-spaces
+
+```agda
+0-Connected-H-Space : (l : Level) → UU (lsuc l)
+0-Connected-H-Space l = Σ (H-Space l) is-0-connected-H-Space
+
+module _
+  {l : Level} (A : 0-Connected-H-Space l)
+  where
+
+  h-space-0-Connected-H-Space : H-Space l
+  h-space-0-Connected-H-Space = pr1 A
+
+  pointed-type-0-Connected-H-Space : Pointed-Type l
+  pointed-type-0-Connected-H-Space =
+    pointed-type-H-Space h-space-0-Connected-H-Space
+
+  type-0-Connected-H-Space : UU l
+  type-0-Connected-H-Space = type-H-Space h-space-0-Connected-H-Space
+
+  unit-0-Connected-H-Space : type-0-Connected-H-Space
+  unit-0-Connected-H-Space = unit-H-Space h-space-0-Connected-H-Space
+
+  mul-0-Connected-H-Space :
+    (x y : type-0-Connected-H-Space) → type-0-Connected-H-Space
+  mul-0-Connected-H-Space = mul-H-Space h-space-0-Connected-H-Space
+
+  left-unit-law-mul-0-Connected-H-Space :
+    (x : type-0-Connected-H-Space) →
+    mul-0-Connected-H-Space unit-0-Connected-H-Space x ＝ x
+  left-unit-law-mul-0-Connected-H-Space =
+    left-unit-law-mul-H-Space h-space-0-Connected-H-Space
+
+  right-unit-law-mul-0-Connected-H-Space :
+    (x : type-0-Connected-H-Space) →
+    mul-0-Connected-H-Space x unit-0-Connected-H-Space ＝ x
+  right-unit-law-mul-0-Connected-H-Space =
+    right-unit-law-mul-H-Space h-space-0-Connected-H-Space
+
+  coh-unit-laws-mul-0-Connected-H-Space :
+    left-unit-law-mul-0-Connected-H-Space unit-0-Connected-H-Space ＝
+    right-unit-law-mul-0-Connected-H-Space unit-0-Connected-H-Space
+  coh-unit-laws-mul-0-Connected-H-Space =
+    coh-unit-laws-mul-H-Space h-space-0-Connected-H-Space
+
+  is-0-connected-0-Connected-H-Space :
+    is-0-connected-H-Space h-space-0-Connected-H-Space
+  is-0-connected-0-Connected-H-Space = pr2 A
+```
+
+## Properties
+
+### The binary operation of any 0-connected H-space is a binary equivalence
+
+```agda
+module _
+  {l : Level} (A : 0-Connected-H-Space l)
+  where
+
+  abstract
+    is-equiv-left-mul-0-Connected-H-Space :
+      (x : type-0-Connected-H-Space A) →
+      is-equiv (λ y → mul-0-Connected-H-Space A x y)
+    is-equiv-left-mul-0-Connected-H-Space x =
+      apply-universal-property-trunc-Prop
+        ( mere-eq-is-0-connected
+          ( is-0-connected-0-Connected-H-Space A)
+          ( unit-0-Connected-H-Space A)
+          ( x))
+        ( is-equiv-Prop (mul-0-Connected-H-Space A x))
+        ( λ where
+          refl →
+            is-equiv-htpy id
+              ( left-unit-law-mul-0-Connected-H-Space A)
+              ( is-equiv-id))
+
+  abstract
+    is-equiv-right-mul-0-Connected-H-Space :
+      (y : type-0-Connected-H-Space A) →
+      is-equiv (λ x → mul-0-Connected-H-Space A x y)
+    is-equiv-right-mul-0-Connected-H-Space y =
+      apply-universal-property-trunc-Prop
+        ( mere-eq-is-0-connected
+          ( is-0-connected-0-Connected-H-Space A)
+          ( unit-0-Connected-H-Space A)
+          ( y))
+        ( is-equiv-Prop (λ x → mul-0-Connected-H-Space A x y))
+        ( λ where
+          refl →
+            is-equiv-htpy id
+              ( right-unit-law-mul-0-Connected-H-Space A)
+              ( is-equiv-id))
+
+  abstract
+    is-binary-equiv-mul-0-Connected-H-Space :
+      is-binary-equiv (mul-0-Connected-H-Space A)
+    pr1 is-binary-equiv-mul-0-Connected-H-Space =
+      is-equiv-right-mul-0-Connected-H-Space
+    pr2 is-binary-equiv-mul-0-Connected-H-Space =
+      is-equiv-left-mul-0-Connected-H-Space
+```
diff --git a/src/structured-types/h-spaces.lagda.md b/src/structured-types/h-spaces.lagda.md
index be217b8539..56971caaeb 100644
--- a/src/structured-types/h-spaces.lagda.md
+++ b/src/structured-types/h-spaces.lagda.md
@@ -9,13 +9,18 @@ module structured-types.h-spaces where
 ```agda
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-triangles-of-identifications
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 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.injective-maps
+open import foundation.path-algebra
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unital-binary-operations
 open import foundation.universe-levels
@@ -196,3 +201,120 @@ module _
             equiv-tot (λ _ → inv-equiv (equiv-right-whisker-concat refl))))) ∘e
     ( associative-Σ _ _ _)
 ```
+
+### Every type equivalent to an H-space is an H-space
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : H-Space l2) (e : A ≃ type-H-Space B)
+  where
+
+  unit-equiv-H-Space : A
+  unit-equiv-H-Space = map-inv-equiv e (unit-H-Space B)
+
+  compute-unit-equiv-H-Space : map-equiv e unit-equiv-H-Space ＝ unit-H-Space B
+  compute-unit-equiv-H-Space = is-section-map-inv-equiv e (unit-H-Space B)
+
+  mul-equiv-H-Space : A → A → A
+  mul-equiv-H-Space x y =
+    map-inv-equiv e (mul-H-Space B (map-equiv e x) (map-equiv e y))
+
+  compute-mul-equiv-H-Space :
+    (x y : A) →
+    map-equiv e (mul-equiv-H-Space x y) ＝
+    mul-H-Space B (map-equiv e x) (map-equiv e y)
+  compute-mul-equiv-H-Space x y =
+    is-section-map-inv-equiv e _
+
+  left-unit-law-mul-equiv-H-Space :
+    (x : A) → mul-equiv-H-Space unit-equiv-H-Space x ＝ x
+  left-unit-law-mul-equiv-H-Space x =
+    map-inv-is-equiv
+      ( is-emb-equiv e _ _)
+      ( ( compute-mul-equiv-H-Space _ _) ∙
+        ( ( ap (λ t → mul-H-Space B t _) compute-unit-equiv-H-Space) ∙
+          ( left-unit-law-mul-H-Space B _)))
+
+  compute-left-unit-law-mul-equiv-H-Space :
+    (x : A) →
+    ap (map-equiv e) (left-unit-law-mul-equiv-H-Space x) ＝
+    ( ( compute-mul-equiv-H-Space unit-equiv-H-Space x) ∙
+      ( ( ap (λ t → mul-H-Space B t _) (compute-unit-equiv-H-Space)) ∙
+        ( left-unit-law-mul-H-Space B (map-equiv e x))))
+  compute-left-unit-law-mul-equiv-H-Space x =
+    is-section-map-inv-is-equiv (is-emb-equiv e _ _) _
+
+  right-unit-law-mul-equiv-H-Space :
+    (x : A) → mul-equiv-H-Space x unit-equiv-H-Space ＝ x
+  right-unit-law-mul-equiv-H-Space x =
+    map-inv-is-equiv
+      ( is-emb-equiv e _ _)
+      ( ( compute-mul-equiv-H-Space _ _) ∙
+        ( ( ap (mul-H-Space B _) compute-unit-equiv-H-Space) ∙
+          ( right-unit-law-mul-H-Space B _)))
+
+  compute-right-unit-law-mul-equiv-H-Space :
+    (x : A) →
+    ( ap (map-equiv e) (right-unit-law-mul-equiv-H-Space x)) ＝
+    ( ( compute-mul-equiv-H-Space x unit-equiv-H-Space) ∙
+      ( ( ap (mul-H-Space B _) (compute-unit-equiv-H-Space)) ∙
+        ( right-unit-law-mul-H-Space B (map-equiv e x))))
+  compute-right-unit-law-mul-equiv-H-Space x =
+    is-section-map-inv-is-equiv (is-emb-equiv e _ _) _
+
+  coh-unit-laws-mul-equiv-H-Space :
+    left-unit-law-mul-equiv-H-Space unit-equiv-H-Space ＝
+    right-unit-law-mul-equiv-H-Space unit-equiv-H-Space
+  coh-unit-laws-mul-equiv-H-Space =
+    is-injective-is-equiv
+      ( is-emb-equiv e _ _)
+      ( ( compute-left-unit-law-mul-equiv-H-Space _) ∙
+        ( ( left-whisker-concat
+            ( compute-mul-equiv-H-Space _ _)
+            ( right-unwhisker-concat-coherence-square-identifications
+              ( ap (mul-H-Space B _) compute-unit-equiv-H-Space)
+              ( ap
+                ( λ t → mul-H-Space B t (map-equiv e unit-equiv-H-Space))
+                ( compute-unit-equiv-H-Space))
+              ( right-unit-law-mul-H-Space B _)
+              ( left-unit-law-mul-H-Space B _)
+              ( compute-unit-equiv-H-Space)
+              ( ( left-whisker-concat
+                  ( ap (λ t → mul-H-Space B t _) compute-unit-equiv-H-Space)
+                  ( nat-htpy-id
+                    ( left-unit-law-mul-H-Space B)
+                    ( compute-unit-equiv-H-Space))) ∙
+                ( inv
+                  ( assoc
+                    ( ap (λ t → mul-H-Space B t _) compute-unit-equiv-H-Space)
+                    ( ap (mul-H-Space B _) compute-unit-equiv-H-Space)
+                    ( left-unit-law-mul-H-Space B (unit-H-Space B)))) ∙
+                ( horizontal-concat-Id²
+                  ( triangle-ap-binary'
+                    ( mul-H-Space B)
+                    ( is-section-map-inv-equiv e _)
+                    ( is-section-map-inv-equiv e _))
+                  ( coh-unit-laws-mul-H-Space B)) ∙
+                ( assoc
+                  ( ap (mul-H-Space B _) compute-unit-equiv-H-Space)
+                  ( ap (λ t → mul-H-Space B t _) compute-unit-equiv-H-Space)
+                  ( right-unit-law-mul-H-Space B (unit-H-Space B))) ∙
+                ( inv
+                  ( left-whisker-concat
+                    ( ap (mul-H-Space B _) compute-unit-equiv-H-Space)
+                    ( nat-htpy-id
+                      ( right-unit-law-mul-H-Space B)
+                      ( compute-unit-equiv-H-Space))))))) ∙
+          ( inv (compute-right-unit-law-mul-equiv-H-Space _))))
+
+  pointed-type-equiv-H-Space : Pointed-Type l1
+  pr1 pointed-type-equiv-H-Space = A
+  pr2 pointed-type-equiv-H-Space = unit-equiv-H-Space
+
+  h-space-equiv-H-Space : H-Space l1
+  pr1 h-space-equiv-H-Space = pointed-type-equiv-H-Space
+  pr1 (pr2 h-space-equiv-H-Space) = mul-equiv-H-Space
+  pr1 (pr2 (pr2 h-space-equiv-H-Space)) = left-unit-law-mul-equiv-H-Space
+  pr1 (pr2 (pr2 (pr2 h-space-equiv-H-Space))) = right-unit-law-mul-equiv-H-Space
+  pr2 (pr2 (pr2 (pr2 h-space-equiv-H-Space))) = coh-unit-laws-mul-equiv-H-Space
+```
diff --git a/src/structured-types/mere-units-h-spaces.lagda.md b/src/structured-types/mere-units-h-spaces.lagda.md
new file mode 100644
index 0000000000..e49a1e03cb
--- /dev/null
+++ b/src/structured-types/mere-units-h-spaces.lagda.md
@@ -0,0 +1,212 @@
+# Mere units of H-spaces
+
+```agda
+module structured-types.mere-units-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.0-connected-types
+open import foundation.action-on-identifications-functions
+open import foundation.binary-equivalences
+open import foundation.connected-components
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.mere-equality
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import structured-types.connected-h-spaces
+open import structured-types.h-spaces
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "mere unit" Disambiguation="H-space"}} in an
+[H-space](structured-types.h-spaces.md) `A` is an element `x` that is
+[merely equal](foundation.mere-equality.md) to the unit element of `A`. The type
+of mere units of an H-space always forms a
+[connected H-space](structured-types.connected-h-spaces.md). In particular,
+since the multiplicative operation of a connected H-space is always a
+[binary equivalence](foundation.binary-equivalences.md), it follows that the
+binary operation restricted to the mere units of an H-space is a binary
+equivalence.
+
+## Definitions
+
+### The predicate of being a mere unit of an H-space
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  is-mere-unit-prop-H-Space : type-H-Space A → Prop l1
+  is-mere-unit-prop-H-Space x = mere-eq-Prop (unit-H-Space A) x
+
+  is-mere-unit-H-Space : type-H-Space A → UU l1
+  is-mere-unit-H-Space x = mere-eq (unit-H-Space A) x
+
+  is-prop-is-mere-unit-H-Space :
+    (x : type-H-Space A) → is-prop (is-mere-unit-H-Space x)
+  is-prop-is-mere-unit-H-Space x =
+    is-prop-mere-eq (unit-H-Space A) x
+```
+
+### The type of mere units of an H-space
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  mere-unit-H-Space : UU l1
+  mere-unit-H-Space = Σ (type-H-Space A) (is-mere-unit-H-Space A)
+```
+
+### The connected component of the unit of an H-Space
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  connected-component-unit-H-Space : UU l1
+  connected-component-unit-H-Space =
+    connected-component (type-H-Space A) (unit-H-Space A)
+
+  is-0-connected-connected-component-unit-H-Space :
+    is-0-connected connected-component-unit-H-Space
+  is-0-connected-connected-component-unit-H-Space =
+    is-0-connected-connected-component (type-H-Space A) (unit-H-Space A)
+
+  inclusion-connected-component-unit-H-Space :
+    connected-component-unit-H-Space → type-H-Space A
+  inclusion-connected-component-unit-H-Space = pr1
+```
+
+## Properties
+
+### The unit of an H-space is a mere unit
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  is-mere-unit-unit-H-Space : is-mere-unit-H-Space A (unit-H-Space A)
+  is-mere-unit-unit-H-Space = refl-mere-eq _
+```
+
+### The multiplicative operation of an H-space preserves mere units
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  abstract
+    preserves-mere-unit-mul-H-Space :
+      {x y : type-H-Space A} →
+      is-mere-unit-H-Space A x → is-mere-unit-H-Space A y →
+      is-mere-unit-H-Space A (mul-H-Space A x y)
+    preserves-mere-unit-mul-H-Space H K =
+      apply-twice-universal-property-trunc-Prop H K
+        ( is-mere-unit-prop-H-Space A _)
+        ( λ where
+          refl refl →
+            unit-trunc-Prop (inv (left-unit-law-mul-H-Space A _)))
+```
+
+### The connected component of the unit of an H-space is a connected H-space
+
+```agda
+module _
+  {l1 : Level} (A : H-Space l1)
+  where
+
+  unit-connected-component-unit-H-Space : connected-component-unit-H-Space A
+  pr1 unit-connected-component-unit-H-Space = unit-H-Space A
+  pr2 unit-connected-component-unit-H-Space = is-mere-unit-unit-H-Space A
+
+  connected-component-unit-pointed-type-H-Space : Pointed-Type l1
+  pr1 connected-component-unit-pointed-type-H-Space =
+    connected-component-unit-H-Space A
+  pr2 connected-component-unit-pointed-type-H-Space =
+    unit-connected-component-unit-H-Space
+
+  mul-connected-component-unit-H-Space :
+    (x y : connected-component-unit-H-Space A) →
+    connected-component-unit-H-Space A
+  pr1 (mul-connected-component-unit-H-Space x y) =
+    mul-H-Space A
+      ( inclusion-connected-component-unit-H-Space A x)
+      ( inclusion-connected-component-unit-H-Space A y)
+  pr2 (mul-connected-component-unit-H-Space x y) =
+    preserves-mere-unit-mul-H-Space A (pr2 x) (pr2 y)
+
+  left-unit-law-mul-connected-component-unit-H-Space :
+    (x : connected-component-unit-H-Space A) →
+    mul-connected-component-unit-H-Space
+      ( unit-connected-component-unit-H-Space)
+      ( x) ＝
+    x
+  left-unit-law-mul-connected-component-unit-H-Space x =
+    eq-type-subtype
+      ( is-mere-unit-prop-H-Space A)
+      ( left-unit-law-mul-H-Space A
+        ( inclusion-connected-component-unit-H-Space A x))
+
+  right-unit-law-mul-connected-component-unit-H-Space :
+    (x : connected-component-unit-H-Space A) →
+    mul-connected-component-unit-H-Space
+      ( x)
+      ( unit-connected-component-unit-H-Space) ＝
+    x
+  right-unit-law-mul-connected-component-unit-H-Space x =
+    eq-type-subtype
+      ( is-mere-unit-prop-H-Space A)
+      ( right-unit-law-mul-H-Space A
+        ( inclusion-connected-component-unit-H-Space A x))
+
+  coh-unit-laws-mul-connected-component-unit-H-Space :
+    left-unit-law-mul-connected-component-unit-H-Space
+      ( unit-connected-component-unit-H-Space) ＝
+    right-unit-law-mul-connected-component-unit-H-Space
+      ( unit-connected-component-unit-H-Space)
+  coh-unit-laws-mul-connected-component-unit-H-Space =
+    ap
+      ( eq-type-subtype (is-mere-unit-prop-H-Space A))
+      ( coh-unit-laws-mul-H-Space A)
+
+  connected-component-unit-h-space-H-Space : H-Space l1
+  pr1 connected-component-unit-h-space-H-Space =
+    connected-component-unit-pointed-type-H-Space
+  pr1 (pr2 connected-component-unit-h-space-H-Space) =
+    mul-connected-component-unit-H-Space
+  pr1 (pr2 (pr2 connected-component-unit-h-space-H-Space)) =
+    left-unit-law-mul-connected-component-unit-H-Space
+  pr1 (pr2 (pr2 (pr2 connected-component-unit-h-space-H-Space))) =
+    right-unit-law-mul-connected-component-unit-H-Space
+  pr2 (pr2 (pr2 (pr2 connected-component-unit-h-space-H-Space))) =
+    coh-unit-laws-mul-connected-component-unit-H-Space
+
+  connected-component-unit-connected-h-space-H-Space :
+    0-Connected-H-Space l1
+  pr1 connected-component-unit-connected-h-space-H-Space =
+    connected-component-unit-h-space-H-Space
+  pr2 connected-component-unit-connected-h-space-H-Space =
+    is-0-connected-connected-component-unit-H-Space A
+
+  is-binary-equiv-mul-connected-component-unit-H-Space :
+    is-binary-equiv mul-connected-component-unit-H-Space
+  is-binary-equiv-mul-connected-component-unit-H-Space =
+    is-binary-equiv-mul-0-Connected-H-Space
+      ( connected-component-unit-connected-h-space-H-Space)
+```