diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md
index dc561cf951..4dbc5333e7 100644
--- a/src/structured-types.lagda.md
+++ b/src/structured-types.lagda.md
@@ -18,6 +18,7 @@ open import structured-types.conjugation-pointed-types public
 open import structured-types.constant-pointed-maps public
 open import structured-types.contractible-pointed-types public
 open import structured-types.cyclic-types public
+open import structured-types.dependent-extension-h-spaces public
 open import structured-types.dependent-products-h-spaces public
 open import structured-types.dependent-products-pointed-types public
 open import structured-types.dependent-products-wild-monoids public
@@ -27,6 +28,7 @@ open import structured-types.equivalences-pointed-arrows public
 open import structured-types.equivalences-retractive-types public
 open import structured-types.equivalences-types-equipped-with-automorphisms public
 open import structured-types.equivalences-types-equipped-with-endomorphisms public
+open import structured-types.extension-h-spaces public
 open import structured-types.faithful-pointed-maps public
 open import structured-types.fibers-of-pointed-maps public
 open import structured-types.finite-multiplication-magmas public
@@ -54,10 +56,12 @@ open import structured-types.noncoherent-h-spaces public
 open import structured-types.opposite-pointed-spans public
 open import structured-types.pointed-2-homotopies public
 open import structured-types.pointed-cartesian-product-types public
+open import structured-types.pointed-dependent-function-h-spaces public
 open import structured-types.pointed-dependent-functions public
 open import structured-types.pointed-dependent-pair-types public
 open import structured-types.pointed-equivalences public
 open import structured-types.pointed-families-of-types public
+open import structured-types.pointed-function-h-spaces public
 open import structured-types.pointed-homotopies public
 open import structured-types.pointed-isomorphisms public
 open import structured-types.pointed-maps public
diff --git a/src/structured-types/central-h-spaces.lagda.md b/src/structured-types/central-h-spaces.lagda.md
index 02606c1864..f51a364c7a 100644
--- a/src/structured-types/central-h-spaces.lagda.md
+++ b/src/structured-types/central-h-spaces.lagda.md
@@ -26,7 +26,7 @@ pointed evaluation map `(A → A) →∗ A`. If the type `A` is
 [connected component](foundation.connected-components.md) of `(A ≃ A)` at the
 identity [equivalence](foundation-core.equivalences.md). An
 {{#concept "evaluative H-space" Agda=is-central-h-space}} is a pointed type such
-that the map `ev_pt : (A ≃ A)_{(id)} → A` is an equivalence.
+that the map `ev_pt : (A ≃ A)_(id) → A` is an equivalence.
 
 ## Definition
 
diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md
new file mode 100644
index 0000000000..5bb0f3b4ac
--- /dev/null
+++ b/src/structured-types/dependent-extension-h-spaces.lagda.md
@@ -0,0 +1,177 @@
+# Dependent extension H-spaces
+
+```agda
+module structured-types.dependent-extension-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.equality-extensions-dependent-maps
+open import orthogonal-factorization-systems.extensions-dependent-maps
+
+open import structured-types.h-spaces
+open import structured-types.magmas
+open import structured-types.noncoherent-h-spaces
+open import structured-types.pointed-dependent-functions
+open import structured-types.pointed-homotopies
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+Given a map `h : A → B` and a family of [H-spaces](structured-types.h-spaces.md)
+`M i` indexed by `B`, the
+{{#concept "dependent extension H-space" Agda=extension-Π-H-Space}}
+`extension-Π h M` is an H-space consisting of
+[dependent extensions](orthogonal-factorization-systems.extensions-dependent-maps.md)
+of the family of units `η : (i : A) → M (h i)` in `M` along `h`. I.e., maps
+`f : (i : B) → M i` [equipped](foundation.structure.md) with a
+[homotopy](foundation-core.homotopies.md) `f ∘ h ~ η`. The multiplication is
+given pointwise, and on the homotopy by the
+[binary action on identifications](foundation.action-on-identifications-binary-functions.md)
+of the pointwise multiplication operation of `M`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (h : A → B)
+  (M : B → H-Space l3)
+  where
+
+  type-extension-Π-H-Space : UU (l1 ⊔ l2 ⊔ l3)
+  type-extension-Π-H-Space =
+    extension-dependent-map' h (type-H-Space ∘ M) (unit-H-Space ∘ M ∘ h)
+
+  unit-extension-Π-H-Space : type-extension-Π-H-Space
+  unit-extension-Π-H-Space = (unit-H-Space ∘ M , refl-htpy)
+
+  pointed-type-extension-Π-H-Space : Pointed-Type (l1 ⊔ l2 ⊔ l3)
+  pointed-type-extension-Π-H-Space =
+    ( type-extension-Π-H-Space , unit-extension-Π-H-Space)
+
+  mul-extension-Π-H-Space :
+    type-extension-Π-H-Space →
+    type-extension-Π-H-Space →
+    type-extension-Π-H-Space
+  pr1 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i =
+    mul-H-Space (M i) (f i) (g i)
+  pr2 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i =
+    ( ap-binary (mul-H-Space (M (h i))) (f∗ i) (g∗ i)) ∙
+    ( left-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i))))
+
+  htpy-left-unit-law-mul-extension-Π-H-Space :
+    (f : type-extension-Π-H-Space) →
+    htpy-extension-dependent-map'
+      ( h)
+      ( unit-H-Space ∘ M ∘ h)
+      ( mul-extension-Π-H-Space unit-extension-Π-H-Space f)
+      ( f)
+  pr1 (htpy-left-unit-law-mul-extension-Π-H-Space (f , f∗)) i =
+    left-unit-law-mul-H-Space (M i) (f i)
+  pr2 (htpy-left-unit-law-mul-extension-Π-H-Space (f , f∗)) i =
+    inv-nat-htpy-id (left-unit-law-mul-H-Space (M (h i))) (f∗ i)
+
+  left-unit-law-mul-extension-Π-H-Space :
+    (f : type-extension-Π-H-Space) →
+    mul-extension-Π-H-Space unit-extension-Π-H-Space f ＝ f
+  left-unit-law-mul-extension-Π-H-Space f =
+    eq-htpy-extension-dependent-map'
+      ( h)
+      ( unit-H-Space ∘ M ∘ h)
+      ( mul-extension-Π-H-Space unit-extension-Π-H-Space f)
+      ( f)
+      ( htpy-left-unit-law-mul-extension-Π-H-Space f)
+
+  htpy-right-unit-law-mul-extension-Π-H-Space' :
+    (f : type-extension-Π-H-Space) →
+    htpy-extension-dependent-map'
+      ( h)
+      ( unit-H-Space ∘ M ∘ h)
+      ( mul-extension-Π-H-Space f unit-extension-Π-H-Space)
+      ( f)
+  pr1 (htpy-right-unit-law-mul-extension-Π-H-Space' (f , f∗)) i =
+    right-unit-law-mul-H-Space (M i) (f i)
+  pr2 (htpy-right-unit-law-mul-extension-Π-H-Space' (f , f∗)) i =
+    equational-reasoning
+      ( ( ap (λ f → mul-H-Space (M (h i)) f (unit-H-Space (M (h i)))) (f∗ i)) ∙
+        ( refl)) ∙
+      ( left-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i))))
+      ＝
+        ( ap (λ f → mul-H-Space (M (h i)) f (unit-H-Space (M (h i)))) (f∗ i)) ∙
+        ( right-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i))))
+        by ap-binary (_∙_) right-unit (coh-unit-laws-mul-H-Space (M (h i)))
+      ＝
+        ( right-unit-law-mul-H-Space (M (h i)) (f (h i)) ∙ f∗ i)
+        by inv-nat-htpy-id (right-unit-law-mul-H-Space (M (h i))) (f∗ i)
+
+  right-unit-law-mul-extension-Π-H-Space' :
+    (f : type-extension-Π-H-Space) →
+    mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f
+  right-unit-law-mul-extension-Π-H-Space' f =
+    eq-htpy-extension-dependent-map'
+      ( h)
+      ( unit-H-Space ∘ M ∘ h)
+      ( mul-extension-Π-H-Space f unit-extension-Π-H-Space)
+      ( f)
+      ( htpy-right-unit-law-mul-extension-Π-H-Space' f)
+
+  noncoherent-h-space-extension-Π-H-Space : Noncoherent-H-Space (l1 ⊔ l2 ⊔ l3)
+  noncoherent-h-space-extension-Π-H-Space =
+    ( pointed-type-extension-Π-H-Space ,
+      mul-extension-Π-H-Space ,
+      left-unit-law-mul-extension-Π-H-Space ,
+      right-unit-law-mul-extension-Π-H-Space')
+
+  extension-Π-H-Space : H-Space (l1 ⊔ l2 ⊔ l3)
+  extension-Π-H-Space =
+    h-space-Noncoherent-H-Space noncoherent-h-space-extension-Π-H-Space
+
+  right-unit-law-mul-extension-Π-H-Space :
+    (f : type-extension-Π-H-Space) →
+    mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f
+  right-unit-law-mul-extension-Π-H-Space =
+    right-unit-law-mul-H-Space extension-Π-H-Space
+
+  is-unital-mul-extension-Π-H-Space : is-unital mul-extension-Π-H-Space
+  is-unital-mul-extension-Π-H-Space = is-unital-mul-H-Space extension-Π-H-Space
+
+  coh-unit-laws-mul-extension-Π-H-Space :
+    coh-unit-laws
+      ( mul-extension-Π-H-Space)
+      ( unit-extension-Π-H-Space)
+      ( left-unit-law-mul-extension-Π-H-Space)
+      ( right-unit-law-mul-extension-Π-H-Space)
+  coh-unit-laws-mul-extension-Π-H-Space =
+    coh-unit-laws-mul-H-Space extension-Π-H-Space
+
+  coherent-unit-laws-mul-extension-Π-H-Space :
+    coherent-unit-laws mul-extension-Π-H-Space unit-extension-Π-H-Space
+  coherent-unit-laws-mul-extension-Π-H-Space =
+    coherent-unit-laws-mul-H-Space extension-Π-H-Space
+
+  is-coherently-unital-mul-extension-Π-H-Space :
+    is-coherently-unital mul-extension-Π-H-Space
+  is-coherently-unital-mul-extension-Π-H-Space =
+    is-coherently-unital-mul-H-Space extension-Π-H-Space
+
+  coherent-unital-mul-extension-Π-H-Space :
+    coherent-unital-mul-Pointed-Type pointed-type-extension-Π-H-Space
+  coherent-unital-mul-extension-Π-H-Space =
+    coherent-unital-mul-H-Space extension-Π-H-Space
+
+  magma-extension-Π-H-Space : Magma (l1 ⊔ l2 ⊔ l3)
+  magma-extension-Π-H-Space = magma-H-Space extension-Π-H-Space
+```
diff --git a/src/structured-types/extension-h-spaces.lagda.md b/src/structured-types/extension-h-spaces.lagda.md
new file mode 100644
index 0000000000..8212add74e
--- /dev/null
+++ b/src/structured-types/extension-h-spaces.lagda.md
@@ -0,0 +1,106 @@
+# Extension H-spaces
+
+```agda
+module structured-types.extension-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import structured-types.dependent-extension-h-spaces
+open import structured-types.h-spaces
+open import structured-types.magmas
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+Given a map `h : A → B` and an [H-space](structured-types.h-spaces.md) `M`, the
+{{#concept "extension H-space" Agda=extension-H-Space}} `extension h M` is an
+H-space consisting of
+[extensions](orthogonal-factorization-systems.extensions-maps.md) of the
+constant family of units `η : A → M` in `M` along `h`. I.e., maps `f : B → M`
+[equipped](foundation.structure.md) with a
+[homotopy](foundation-core.homotopies.md) `f ∘ h ~ η`. The multiplication is
+given pointwise, and on the homotopy by the
+[binary action on identifications](foundation.action-on-identifications-binary-functions.md)
+of the multiplication operation of `M`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (h : A → B) (M : H-Space l3)
+  where
+
+  extension-H-Space : H-Space (l1 ⊔ l2 ⊔ l3)
+  extension-H-Space = extension-Π-H-Space h (λ _ → M)
+
+  pointed-type-extension-H-Space : Pointed-Type (l1 ⊔ l2 ⊔ l3)
+  pointed-type-extension-H-Space =
+    pointed-type-H-Space extension-H-Space
+
+  type-extension-H-Space : UU (l1 ⊔ l2 ⊔ l3)
+  type-extension-H-Space =
+    type-H-Space extension-H-Space
+
+  unit-extension-H-Space : type-extension-H-Space
+  unit-extension-H-Space =
+    unit-H-Space extension-H-Space
+
+  mul-extension-H-Space :
+    type-extension-H-Space →
+    type-extension-H-Space →
+    type-extension-H-Space
+  mul-extension-H-Space = mul-H-Space extension-H-Space
+
+  left-unit-law-mul-extension-H-Space :
+    (f : type-extension-H-Space) →
+    mul-extension-H-Space unit-extension-H-Space f ＝ f
+  left-unit-law-mul-extension-H-Space =
+    left-unit-law-mul-H-Space extension-H-Space
+
+  right-unit-law-mul-extension-H-Space :
+    (f : type-extension-H-Space) →
+    mul-extension-H-Space f unit-extension-H-Space ＝ f
+  right-unit-law-mul-extension-H-Space =
+    right-unit-law-mul-H-Space extension-H-Space
+
+  is-unital-mul-extension-H-Space :
+    is-unital mul-extension-H-Space
+  is-unital-mul-extension-H-Space =
+    is-unital-mul-H-Space extension-H-Space
+
+  coh-unit-laws-mul-extension-H-Space :
+    coh-unit-laws
+      ( mul-extension-H-Space)
+      ( unit-extension-H-Space)
+      ( left-unit-law-mul-extension-H-Space)
+      ( right-unit-law-mul-extension-H-Space)
+  coh-unit-laws-mul-extension-H-Space =
+    coh-unit-laws-mul-H-Space extension-H-Space
+
+  coherent-unit-laws-mul-extension-H-Space :
+    coherent-unit-laws mul-extension-H-Space unit-extension-H-Space
+  coherent-unit-laws-mul-extension-H-Space =
+    coherent-unit-laws-mul-H-Space extension-H-Space
+
+  is-coherently-unital-mul-extension-H-Space :
+    is-coherently-unital mul-extension-H-Space
+  is-coherently-unital-mul-extension-H-Space =
+    is-coherently-unital-mul-H-Space extension-H-Space
+
+  coherent-unital-mul-extension-H-Space :
+    coherent-unital-mul-Pointed-Type pointed-type-extension-H-Space
+  coherent-unital-mul-extension-H-Space =
+    coherent-unital-mul-H-Space extension-H-Space
+
+  magma-extension-H-Space : Magma (l1 ⊔ l2 ⊔ l3)
+  magma-extension-H-Space = magma-H-Space extension-H-Space
+```
diff --git a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md
new file mode 100644
index 0000000000..11c05345aa
--- /dev/null
+++ b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md
@@ -0,0 +1,162 @@
+# Pointed dependent function H-spaces
+
+```agda
+module structured-types.pointed-dependent-function-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import structured-types.h-spaces
+open import structured-types.magmas
+open import structured-types.noncoherent-h-spaces
+open import structured-types.pointed-dependent-functions
+open import structured-types.pointed-homotopies
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+Given a family of [H-spaces](structured-types.h-spaces.md) `M i` indexed by a
+[pointed type](structured-types.pointed-types.md) `i∗ : I`, the
+{{#concept "pointed dependent functions" Disambiguation="H-space" Agda=pointed-Π-H-Space}}
+`Π∗(i : I), M i` is an H-space consisting of
+[pointed dependent functions](structured-types.pointed-dependent-functions.md)
+taking `i : I` to an element of the underlying type of `M i`, and taking `i∗` to
+the unit of `M i∗`. The multiplication is given pointwise, and at the base point
+by the
+[binary action on identifications](foundation.action-on-identifications-binary-functions.md)
+of the multiplication operation of `M i∗`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (I∗ : Pointed-Type l1)
+  (let I = type-Pointed-Type I∗)
+  (let i∗ = point-Pointed-Type I∗)
+  (M : I → H-Space l2)
+  where
+
+  type-pointed-Π-H-Space : UU (l1 ⊔ l2)
+  type-pointed-Π-H-Space = Π∗ I∗ (type-H-Space ∘ M , unit-H-Space (M i∗))
+
+  unit-pointed-Π-H-Space : type-pointed-Π-H-Space
+  unit-pointed-Π-H-Space = (unit-H-Space ∘ M , refl)
+
+  pointed-type-pointed-Π-H-Space : Pointed-Type (l1 ⊔ l2)
+  pointed-type-pointed-Π-H-Space =
+    ( type-pointed-Π-H-Space , unit-pointed-Π-H-Space)
+
+  mul-pointed-Π-H-Space :
+    type-pointed-Π-H-Space → type-pointed-Π-H-Space → type-pointed-Π-H-Space
+  pr1 (mul-pointed-Π-H-Space (f , f∗) (g , g∗)) i =
+    mul-H-Space (M i) (f i) (g i)
+  pr2 (mul-pointed-Π-H-Space (f , f∗) (g , g∗)) =
+    ( ap-binary (mul-H-Space (M i∗)) f∗ g∗) ∙
+    ( left-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗)))
+
+  pointed-htpy-left-unit-law-mul-pointed-Π-H-Space :
+    (f : type-pointed-Π-H-Space) →
+    mul-pointed-Π-H-Space unit-pointed-Π-H-Space f ~∗ f
+  pr1 (pointed-htpy-left-unit-law-mul-pointed-Π-H-Space (f , f∗)) i =
+    left-unit-law-mul-H-Space (M i) (f i)
+  pr2 (pointed-htpy-left-unit-law-mul-pointed-Π-H-Space (f , f∗)) =
+    inv-nat-htpy-id (left-unit-law-mul-H-Space (M i∗)) f∗
+
+  left-unit-law-mul-pointed-Π-H-Space :
+    (f : type-pointed-Π-H-Space) →
+    mul-pointed-Π-H-Space unit-pointed-Π-H-Space f ＝ f
+  left-unit-law-mul-pointed-Π-H-Space f =
+    eq-pointed-htpy
+      ( mul-pointed-Π-H-Space unit-pointed-Π-H-Space f)
+      ( f)
+      ( pointed-htpy-left-unit-law-mul-pointed-Π-H-Space f)
+
+  pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' :
+    (f : type-pointed-Π-H-Space) →
+    mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ~∗ f
+  pr1 (pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' (f , f∗)) i =
+    right-unit-law-mul-H-Space (M i) (f i)
+  pr2 (pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' (f , f∗)) =
+    equational-reasoning
+      (ap (λ f → mul-H-Space (M i∗) f (unit-H-Space (M i∗))) f∗ ∙ refl) ∙
+      left-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗))
+      ＝ ap (λ f → mul-H-Space (M i∗) f (unit-H-Space (M i∗))) f∗ ∙
+        right-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗))
+        by ap-binary (_∙_) right-unit (coh-unit-laws-mul-H-Space (M i∗))
+      ＝ right-unit-law-mul-H-Space (M i∗) (f i∗) ∙ f∗
+        by inv-nat-htpy-id (right-unit-law-mul-H-Space (M i∗)) f∗
+
+  right-unit-law-mul-pointed-Π-H-Space' :
+    (f : type-pointed-Π-H-Space) →
+    mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ＝ f
+  right-unit-law-mul-pointed-Π-H-Space' f =
+    eq-pointed-htpy
+      ( mul-pointed-Π-H-Space f unit-pointed-Π-H-Space)
+      ( f)
+      ( pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' f)
+
+  noncoherent-h-space-pointed-Π-H-Space : Noncoherent-H-Space (l1 ⊔ l2)
+  noncoherent-h-space-pointed-Π-H-Space =
+    ( pointed-type-pointed-Π-H-Space ,
+      mul-pointed-Π-H-Space ,
+      left-unit-law-mul-pointed-Π-H-Space ,
+      right-unit-law-mul-pointed-Π-H-Space')
+
+  pointed-Π-H-Space : H-Space (l1 ⊔ l2)
+  pointed-Π-H-Space =
+    h-space-Noncoherent-H-Space noncoherent-h-space-pointed-Π-H-Space
+
+  right-unit-law-mul-pointed-Π-H-Space :
+    (f : type-pointed-Π-H-Space) →
+    mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ＝ f
+  right-unit-law-mul-pointed-Π-H-Space =
+    right-unit-law-mul-H-Space pointed-Π-H-Space
+
+  is-unital-mul-pointed-Π-H-Space : is-unital mul-pointed-Π-H-Space
+  is-unital-mul-pointed-Π-H-Space = is-unital-mul-H-Space pointed-Π-H-Space
+
+  coh-unit-laws-mul-pointed-Π-H-Space :
+    coh-unit-laws
+      ( mul-pointed-Π-H-Space)
+      ( unit-pointed-Π-H-Space)
+      ( left-unit-law-mul-pointed-Π-H-Space)
+      ( right-unit-law-mul-pointed-Π-H-Space)
+  coh-unit-laws-mul-pointed-Π-H-Space =
+    coh-unit-laws-mul-H-Space pointed-Π-H-Space
+
+  coherent-unit-laws-mul-pointed-Π-H-Space :
+    coherent-unit-laws mul-pointed-Π-H-Space unit-pointed-Π-H-Space
+  coherent-unit-laws-mul-pointed-Π-H-Space =
+    coherent-unit-laws-mul-H-Space pointed-Π-H-Space
+
+  is-coherently-unital-mul-pointed-Π-H-Space :
+    is-coherently-unital mul-pointed-Π-H-Space
+  is-coherently-unital-mul-pointed-Π-H-Space =
+    is-coherently-unital-mul-H-Space pointed-Π-H-Space
+
+  coherent-unital-mul-pointed-Π-H-Space :
+    coherent-unital-mul-Pointed-Type pointed-type-pointed-Π-H-Space
+  coherent-unital-mul-pointed-Π-H-Space =
+    coherent-unital-mul-H-Space pointed-Π-H-Space
+
+  magma-pointed-Π-H-Space : Magma (l1 ⊔ l2)
+  magma-pointed-Π-H-Space = magma-H-Space pointed-Π-H-Space
+```
+
+## See also
+
+- Pointed dependent function H-spaces are a special case of
+  [dependent extension H-spaces](structured-types.dependent-extension-h-spaces.md)
diff --git a/src/structured-types/pointed-dependent-functions.lagda.md b/src/structured-types/pointed-dependent-functions.lagda.md
index b9ebc6b54f..72126019ed 100644
--- a/src/structured-types/pointed-dependent-functions.lagda.md
+++ b/src/structured-types/pointed-dependent-functions.lagda.md
@@ -38,6 +38,7 @@ module _
       ( ev-point (point-Pointed-Type A) {fam-Pointed-Fam A B})
       ( point-Pointed-Fam A B)
 
+  Π∗ : UU (l1 ⊔ l2)
   Π∗ = pointed-Π
 ```
 
diff --git a/src/structured-types/pointed-function-h-spaces.lagda.md b/src/structured-types/pointed-function-h-spaces.lagda.md
new file mode 100644
index 0000000000..8e6f0b76bb
--- /dev/null
+++ b/src/structured-types/pointed-function-h-spaces.lagda.md
@@ -0,0 +1,111 @@
+# Pointed function H-spaces
+
+```agda
+module structured-types.pointed-function-h-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import structured-types.h-spaces
+open import structured-types.magmas
+open import structured-types.pointed-dependent-function-h-spaces
+open import structured-types.pointed-types
+```
+
+</details>
+
+## Idea
+
+Given a [H-space](structured-types.h-spaces.md) `M` and a
+[pointed type](structured-types.pointed-types.md) `I`, the
+{{#concept "pointed function H-space" Agda=pointed-function-H-Space}} `I →∗ M`
+consists of [pointed functions](structured-types.pointed-maps.md) from `I` to
+the underlying pointed type of `M`. The multiplication is given pointwise, and
+at the base point by the
+[binary action on identifications](foundation.action-on-identifications-binary-functions.md)
+of the multiplication operation of `M`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (I∗ : Pointed-Type l1) (M : H-Space l2)
+  where
+
+  pointed-function-H-Space : H-Space (l1 ⊔ l2)
+  pointed-function-H-Space = pointed-Π-H-Space I∗ (λ _ → M)
+
+  pointed-type-pointed-function-H-Space : Pointed-Type (l1 ⊔ l2)
+  pointed-type-pointed-function-H-Space =
+    pointed-type-H-Space pointed-function-H-Space
+
+  type-pointed-function-H-Space : UU (l1 ⊔ l2)
+  type-pointed-function-H-Space =
+    type-H-Space pointed-function-H-Space
+
+  unit-pointed-function-H-Space : type-pointed-function-H-Space
+  unit-pointed-function-H-Space =
+    unit-H-Space pointed-function-H-Space
+
+  mul-pointed-function-H-Space :
+    type-pointed-function-H-Space →
+    type-pointed-function-H-Space →
+    type-pointed-function-H-Space
+  mul-pointed-function-H-Space = mul-H-Space pointed-function-H-Space
+
+  left-unit-law-mul-pointed-function-H-Space :
+    (f : type-pointed-function-H-Space) →
+    mul-pointed-function-H-Space unit-pointed-function-H-Space f ＝ f
+  left-unit-law-mul-pointed-function-H-Space =
+    left-unit-law-mul-H-Space pointed-function-H-Space
+
+  right-unit-law-mul-pointed-function-H-Space :
+    (f : type-pointed-function-H-Space) →
+    mul-pointed-function-H-Space f unit-pointed-function-H-Space ＝ f
+  right-unit-law-mul-pointed-function-H-Space =
+    right-unit-law-mul-H-Space pointed-function-H-Space
+
+  is-unital-mul-pointed-function-H-Space :
+    is-unital mul-pointed-function-H-Space
+  is-unital-mul-pointed-function-H-Space =
+    is-unital-mul-H-Space pointed-function-H-Space
+
+  coh-unit-laws-mul-pointed-function-H-Space :
+    coh-unit-laws
+      ( mul-pointed-function-H-Space)
+      ( unit-pointed-function-H-Space)
+      ( left-unit-law-mul-pointed-function-H-Space)
+      ( right-unit-law-mul-pointed-function-H-Space)
+  coh-unit-laws-mul-pointed-function-H-Space =
+    coh-unit-laws-mul-H-Space pointed-function-H-Space
+
+  coherent-unit-laws-mul-pointed-function-H-Space :
+    coherent-unit-laws
+      ( mul-pointed-function-H-Space)
+      ( unit-pointed-function-H-Space)
+  coherent-unit-laws-mul-pointed-function-H-Space =
+    coherent-unit-laws-mul-H-Space pointed-function-H-Space
+
+  is-coherently-unital-mul-pointed-function-H-Space :
+    is-coherently-unital mul-pointed-function-H-Space
+  is-coherently-unital-mul-pointed-function-H-Space =
+    is-coherently-unital-mul-H-Space pointed-function-H-Space
+
+  coherent-unital-mul-pointed-function-H-Space :
+    coherent-unital-mul-Pointed-Type pointed-type-pointed-function-H-Space
+  coherent-unital-mul-pointed-function-H-Space =
+    coherent-unital-mul-H-Space pointed-function-H-Space
+
+  magma-pointed-function-H-Space : Magma (l1 ⊔ l2)
+  magma-pointed-function-H-Space = magma-H-Space pointed-function-H-Space
+```
+
+## See also
+
+- Pointed function H-spaces are a special case of
+  [extension H-spaces](structured-types.extension-h-spaces.md)