diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 3c328cc604..431ac1f200 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -26,13 +26,30 @@ function is a map
 ```
 
 where `- * Q` is the
-[closed modality](orthogonal-factorization-systems.closed-modalities.md).
+[closed modality](orthogonal-factorization-systems.closed-modalities.md), which
+is defined by the [join operation](synthetic-homotopy-theory.joins-of-types.md).
 
 A value of a copartial function `f` at `a : A` is said to be
 {{#concept "erased" Disambiguation="copartial function" Agda=is-erased-copartial-function}}
 if the copartial element `f a` of `B` is erased.
 
-{{#concept "Composition of copartial functions"}} can be defined by
+A copartial function is [equivalently](foundation-core.equivalences.md)
+described as a [morphism of arrows](foundation.morphisms-arrows.md)
+
+```text
+     A    B   1
+     |    |   |
+  id |  ⇒ | □ | T
+     V    V   V
+     A    1  Prop
+```
+
+where `□` is the
+[pushout-product](synthetic-homotopy-theory.pushout-products.md). Indeed, the
+domain of the pushout-product `B □ T` is the type of copartial elements of `B`.
+
+{{#concept "Composition" Disambiguation="copartial functions"}} of copartial
+functions can be defined by
 
 ```text
                      Σ (Q : Prop), (Σ (P : Prop), C * P) * Q
diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md
index 0b68764cb1..461c072dec 100644
--- a/src/foundation/partial-functions.lagda.md
+++ b/src/foundation/partial-functions.lagda.md
@@ -28,6 +28,22 @@ Given a partial function `f : A → B` and an element `a : A`, we say that `f` i
 {{#concept "defined" Disambiguation="partial function"}} at `a` if the partial
 element `f a` of `A` is defined.
 
+Partial functions can be described
+[equivalently](foundation-core.equivalences.md) as
+[morphisms of arrows](foundation.morphisms-arrows.md)
+
+```text
+  ∅     1   ∅
+  |     |   |
+  |  ⇒  | ∘ |
+  V     V   V
+  A   Prop  B
+```
+
+where the composition operation is
+[composition](species.composition-cauchy-series-species-of-types.md) of
+[polynomial endofunctors](trees.polynomial-endofunctors.md).
+
 ## Definitions
 
 ### Partial functions