From c3c467523011ffe194984c6a8c94e811ea52cf2d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 13:53:19 -0500
Subject: [PATCH 01/18] partial sequences and copartial functions

---
 src/foundation.lagda.md                       |   6 ++
 src/foundation/copartial-elements.lagda.md    | 102 ++++++++++++++++++
 src/foundation/copartial-functions.lagda.md   |  72 +++++++++++++
 src/foundation/partial-elements.lagda.md      |  37 +++++--
 src/foundation/partial-functions.lagda.md     |  71 ++++++++++++
 src/foundation/partial-sequences.lagda.md     |  53 +++++++++
 .../total-partial-elements.lagda.md           |  33 ++++++
 .../total-partial-functions.lagda.md          |  50 +++++++++
 .../closed-modalities.lagda.md                |   8 +-
 9 files changed, 419 insertions(+), 13 deletions(-)
 create mode 100644 src/foundation/copartial-elements.lagda.md
 create mode 100644 src/foundation/copartial-functions.lagda.md
 create mode 100644 src/foundation/partial-functions.lagda.md
 create mode 100644 src/foundation/partial-sequences.lagda.md
 create mode 100644 src/foundation/total-partial-elements.lagda.md
 create mode 100644 src/foundation/total-partial-functions.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 3ce72252c2..55a3c1bc23 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -68,6 +68,8 @@ open import foundation.constant-maps public
 open import foundation.constant-type-families public
 open import foundation.contractible-maps public
 open import foundation.contractible-types public
+open import foundation.copartial-elements public
+open import foundation.copartial-functions public
 open import foundation.coproduct-decompositions public
 open import foundation.coproduct-decompositions-subuniverse public
 open import foundation.coproduct-types public
@@ -221,6 +223,8 @@ open import foundation.negation public
 open import foundation.noncontractible-types public
 open import foundation.pairs-of-distinct-elements public
 open import foundation.partial-elements public
+open import foundation.partial-functions public
+open import foundation.partial-sequences public
 open import foundation.partitions public
 open import foundation.path-algebra public
 open import foundation.path-split-maps public
@@ -308,6 +312,8 @@ open import foundation.symmetric-operations public
 open import foundation.telescopes public
 open import foundation.tight-apartness-relations public
 open import foundation.torsorial-type-families public
+open import foundation.total-partial-elements public
+open import foundation.total-partial-functions public
 open import foundation.towers public
 open import foundation.transfinite-cocomposition-of-maps public
 open import foundation.transport-along-equivalences public
diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
new file mode 100644
index 0000000000..aad739a2d9
--- /dev/null
+++ b/src/foundation/copartial-elements.lagda.md
@@ -0,0 +1,102 @@
+# Copartial elements
+
+```agda
+module foundation.copartial-elements where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.universe-levels
+
+open import foundation-core.propositions
+
+open import orthogonal-factorization-systems.closed-modalities
+```
+
+</details>
+
+## Idea
+
+A {{#concept "copartial element"}} of a type `A` is an element of type
+
+```text
+  Σ (Q : Prop), A * Q
+```
+
+where the type `P * A` is the
+[join](synthetic-homotopy-theory.joins-of-types.md) of `P` and `A`. We say that
+a copartial element `(P , u)` is
+{{#concept "prohibited" Disambiguation="copartial element"}} if the proposition
+`P` holds.
+
+In order to compare copartial elements with
+[partial elements](foundation.partial-elements.md), note that we have the
+following [pullback squares](foundation.pullback-squares.md)
+
+```text
+  A -----> Σ (Q : Prop), A * Q        1 -----> Σ (P : Prop), (P → A)
+  |                |                  |                |
+  |                |                  |                |
+  V                V                  V                V
+  1 -----------> Prop                 1 -----------> Prop
+          ⊥                                   ⊥
+
+  1 -----> Σ (Q : Prop), A * Q        A -----> Σ (P : Prop), (P → A)
+  |                |                  |                |
+  |                |                  |                |
+  V                V                  V                V
+  1 -----------> Prop                 1 -----------> Prop
+          ⊤                                   ⊤
+```
+
+Note that we make use of the
+[closed modalities](orthogonal-factorization-systems.closed-modalities.md)
+`A ↦ P * A` in the formulation of copartial element, whereas the formulation of
+partial elements makes use of the
+[open modalities](orthogonal-factorization-systems.open-modalities.md). The
+concepts of partial and copartial elements are dual in that sense.
+
+**Note:** The topic of copartial elements is not known in the literature, and
+our formalization on this topic should be considered experimental.
+
+## Definition
+
+### Copartial elements
+
+```agda
+copartial-element : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
+copartial-element l2 A =
+  Σ (Prop l2) (λ Q → operator-closed-modality Q A)
+
+module _
+  {l1 l2 : Level} {A : UU l1} (a : copartial-element l2 A)
+  where
+
+  is-prohibited-prop-copartial-element : Prop l2
+  is-prohibited-prop-copartial-element = pr1 a
+
+  is-prohibited-copartial-element : UU l2
+  is-prohibited-copartial-element =
+    type-Prop is-prohibited-prop-copartial-element
+```
+
+### The unit of the copartial element operator
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  is-prohibited-prop-unit-copartial-element : Prop lzero
+  is-prohibited-prop-unit-copartial-element = empty-Prop
+
+  is-prohibited-unit-copartial-element : UU lzero
+  is-prohibited-unit-copartial-element = empty
+
+  unit-copartial-element : copartial-element lzero A
+  pr1 unit-copartial-element = is-prohibited-prop-unit-copartial-element
+  pr2 unit-copartial-element = unit-closed-modality empty-Prop a
+```
diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
new file mode 100644
index 0000000000..239002b803
--- /dev/null
+++ b/src/foundation/copartial-functions.lagda.md
@@ -0,0 +1,72 @@
+# Copartial functions
+
+```agda
+module foundation.copartial-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.copartial-elements
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "copartial function"}} from `A` to `B` is a map from `A` into the
+type of [copartial elements](foundation.copartial-elements.md) of `B`. I.e., a
+copartial function is a map
+
+```text
+  A → Σ (Q : Prop), A * Q
+```
+
+where `- * Q` is the
+[closed modality](orthogonal-factorization-systems.closed-modalities.md).
+
+A value of a copartial function `f` at `a : A` is said to be
+{{#concept "prohibited" Disambiguation="copartial function"}} if the copartial
+element `f a` of `B` is prohibited.
+
+**Note:** The topic of copartial functions is not known in the literature, and
+our formalization on this topic should be considered experimental.
+
+## Definitions
+
+### Copartial functions
+
+```agda
+copartial-function :
+  {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
+copartial-function l3 A B = A → copartial-element l3 B
+```
+
+### Prohibited values of copartial functions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
+  (a : A)
+  where
+
+  is-prohibited-prop-copartial-function : Prop l3
+  is-prohibited-prop-copartial-function =
+    is-prohibited-prop-copartial-element (f a)
+
+  is-prohibited-copartial-function : UU l3
+  is-prohibited-copartial-function = is-prohibited-copartial-element (f a)
+```
+
+### Copartial functions obtained from functions
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  copartial-function-function : copartial-function lzero A B
+  copartial-function-function a = unit-copartial-element (f a)
+```
diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md
index a66e1fdb39..fe260c49a9 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -18,24 +18,36 @@ open import foundation-core.propositions
 
 ## Idea
 
-A **partial element** of `X` consists of a
+A {{#concept "partial element"}} of `X` consists of a
 [proposition](foundation-core.propositions.md) `P` and a map `P → X`. We say
-that a partial element `(P, f)` is **defined** if the proposition `P` holds.
+that a partial element `(P, f)` is
+{{#concept "defined" Disambiguation="partial element"}} if the proposition `P`
+holds.
+
+## Definitions
+
+### Partial elements of a type
 
 ```agda
 partial-element : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
 partial-element l2 X = Σ (Prop l2) (λ P → type-Prop P → X)
 
-is-defined-partial-element-Prop :
-  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → Prop l2
-is-defined-partial-element-Prop x = pr1 x
+module _
+  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X)
+  where
+
+  is-defined-prop-partial-element : Prop l2
+  is-defined-prop-partial-element = pr1 x
+
+  is-defined-partial-element : UU l2
+  is-defined-partial-element = type-Prop is-defined-prop-partial-element
+```
 
-is-defined-partial-element :
-  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → UU l2
-is-defined-partial-element x = type-Prop (is-defined-partial-element-Prop x)
+### The unit of the partial element operator
 
+```agda
 unit-partial-element :
-  {l1 l2 : Level} {X : UU l1} → X → partial-element lzero X
+  {l1 : Level} {X : UU l1} → X → partial-element lzero X
 pr1 (unit-partial-element x) = unit-Prop
 pr2 (unit-partial-element x) y = x
 ```
@@ -46,3 +58,10 @@ pr2 (unit-partial-element x) y = x
 
 This remains to be shown.
 [#734](https://github.com/UniMath/agda-unimath/issues/734)
+
+## See also
+
+- [Copartial elements](foundation.copartial-elements.md)
+- [Partial function](foundation.partial-functions.md)
+- [Partial sequences](elementary-number-theory.partial-sequences.md)
+- [Total partial functions](foundation.total-partial-functions.md)
diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md
new file mode 100644
index 0000000000..0b68764cb1
--- /dev/null
+++ b/src/foundation/partial-functions.lagda.md
@@ -0,0 +1,71 @@
+# Partial functions
+
+```agda
+module foundation.partial-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.partial-elements
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "partial function"}} from `A` to `B` is a function from `A` into
+the type of [partial elements](foundation.partial-elements.md) of `B`. In other
+words, a partial function is a function
+
+```text
+  A → Σ (P : Prop), (P → B).
+```
+
+Given a partial function `f : A → B` and an element `a : A`, we say that `f` is
+{{#concept "defined" Disambiguation="partial function"}} at `a` if the partial
+element `f a` of `A` is defined.
+
+## Definitions
+
+### Partial functions
+
+```agda
+partial-function :
+  {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
+partial-function l3 A B = A → partial-element l3 B
+```
+
+### The predicate of being defined at an element in the domain
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B)
+  (a : A)
+  where
+
+  is-defined-prop-partial-function : Prop l3
+  is-defined-prop-partial-function = is-defined-prop-partial-element (f a)
+
+  is-defined-partial-function : UU l3
+  is-defined-partial-function = type-Prop is-defined-prop-partial-function
+```
+
+### The partial function obtained from a function
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  partial-function-function : partial-function lzero A B
+  partial-function-function a = unit-partial-element (f a)
+```
+
+## See also
+
+- [Copartial functions](foundation.copartial-functions.md)
+- [Partial elements](foundation.partial-elements.md)
+- [Partial sequences](foundation.partial-sequences.md)
diff --git a/src/foundation/partial-sequences.lagda.md b/src/foundation/partial-sequences.lagda.md
new file mode 100644
index 0000000000..f9ad3ff4cd
--- /dev/null
+++ b/src/foundation/partial-sequences.lagda.md
@@ -0,0 +1,53 @@
+# Partial sequences
+
+```agda
+module foundation.partial-sequences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.partial-functions
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "partial sequence"}} of elements of a type `A` is a
+[partial function](foundation.partial-functions.md) from `ℕ` → `A`. In other
+words, a partial sequence is a map
+
+```text
+  ℕ → Σ (P : Prop), (P → A)
+```
+
+from `ℕ` into the type of [partial elements](foundation.partial-elements.md) of
+`A`.
+
+## Definitions
+
+### Partial sequences
+
+```agda
+partial-sequence : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
+partial-sequence l2 A = partial-function l2 ℕ A
+```
+
+### Defined elements of partial sequences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (a : partial-sequence l2 A)
+  where
+
+  is-defined-prop-partial-sequence : ℕ → Prop l2
+  is-defined-prop-partial-sequence = is-defined-prop-partial-function a
+
+  is-defined-partial-sequence : ℕ → UU l2
+  is-defined-partial-sequence = is-defined-partial-function a
+```
diff --git a/src/foundation/total-partial-elements.lagda.md b/src/foundation/total-partial-elements.lagda.md
new file mode 100644
index 0000000000..2d3cf9604c
--- /dev/null
+++ b/src/foundation/total-partial-elements.lagda.md
@@ -0,0 +1,33 @@
+# Total partial elements
+
+```agda
+module foundation.total-partial-elements where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.partial-elements
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [partial element](foundation.partial-elements.md) `a` of `A` is said to be
+{{#concept "total" Disambiguation="partial element"}} if it is defined. The type
+of total partial elements of `A` is
+[equivalent](foundation-core.equivalences.md) to the type `A`
+
+## Definitions
+
+### The type of total partial elements
+
+```agda
+total-partial-element :
+  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
+total-partial-element l2 A =
+  Σ (partial-element l2 A) is-defined-partial-element
+```
diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md
new file mode 100644
index 0000000000..624af890db
--- /dev/null
+++ b/src/foundation/total-partial-functions.lagda.md
@@ -0,0 +1,50 @@
+# Total partial functions
+
+```agda
+module foundation.total-partial-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.partial-functions
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [partial function](foundation.partial-functions.md) `f : A → B` is said to be
+{{#concept "total" Disambiguation="partial function"}} if the
+[partial element](foundation.partial-elements.md) `f a` of `B` is defined for
+every `a : A`. The type of total partial functions from `A` to `B` is equivalent
+to the type of [functions](foundation-core.function-types.md) from `A` to `B`.
+
+## Definitions
+
+### The predicate of being a total partial function
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B)
+  where
+
+  is-total-prop-partial-function : Prop (l1 ⊔ l3)
+  is-total-prop-partial-function =
+    Π-Prop A (is-defined-prop-partial-function f)
+
+  is-total-partial-function : UU (l1 ⊔ l3)
+  is-total-partial-function = type-Prop is-total-prop-partial-function
+```
+
+### The type of total partial functions
+
+```agda
+total-partial-function :
+  {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
+total-partial-function l3 A B =
+  Σ (partial-function l3 A B) is-total-partial-function
+```
diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
index 0b18cf063c..7c79d77436 100644
--- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
@@ -38,11 +38,11 @@ call these the **closed modalities**.
 
 ```agda
 operator-closed-modality :
-  (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ)
-operator-closed-modality l Q A = A * type-Prop Q
+  {l lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ)
+operator-closed-modality Q A = A * type-Prop Q
 
 unit-closed-modality :
-  {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q)
+  {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality {l} Q)
 unit-closed-modality Q = inl-join
 
 is-closed-modal :
@@ -63,7 +63,7 @@ module _
   is-reflective-subuniverse-closed-modality :
     is-reflective-subuniverse {l ⊔ lQ} (is-closed-modal Q)
   pr1 is-reflective-subuniverse-closed-modality =
-    operator-closed-modality (l ⊔ lQ) Q
+    operator-closed-modality {l ⊔ lQ} Q
   pr1 (pr2 is-reflective-subuniverse-closed-modality) =
     unit-closed-modality Q
   pr1 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) A q =

From dde889a5a7d08e4944d8b7ed62bda7525a271a26 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 17:55:16 -0500
Subject: [PATCH 02/18] Update src/foundation/partial-sequences.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/partial-sequences.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/partial-sequences.lagda.md b/src/foundation/partial-sequences.lagda.md
index f9ad3ff4cd..dd8e77715c 100644
--- a/src/foundation/partial-sequences.lagda.md
+++ b/src/foundation/partial-sequences.lagda.md
@@ -19,7 +19,7 @@ open import foundation.universe-levels
 ## Idea
 
 A {{#concept "partial sequence"}} of elements of a type `A` is a
-[partial function](foundation.partial-functions.md) from `ℕ` → `A`. In other
+[partial function](foundation.partial-functions.md) from `ℕ` to `A`. In other
 words, a partial sequence is a map
 
 ```text

From 8b26b91743870875cce44ce02a6add57ab5d040c Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 17:56:18 -0500
Subject: [PATCH 03/18] Update src/foundation/copartial-functions.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 239002b803..17744c6857 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -16,7 +16,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A {{#concept "copartial function"}} from `A` to `B` is a map from `A` into the
+A {{#concept "copartial function" Agda=copartial-function}} from `A` to `B` is a map from `A` into the
 type of [copartial elements](foundation.copartial-elements.md) of `B`. I.e., a
 copartial function is a map
 

From 7bde69d33dca00257a69ac19e6d49eef997def36 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 17:58:50 -0500
Subject: [PATCH 04/18] Update src/foundation/copartial-functions.lagda.md
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
---
 src/foundation/copartial-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 17744c6857..e059fc2011 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -21,7 +21,7 @@ type of [copartial elements](foundation.copartial-elements.md) of `B`. I.e., a
 copartial function is a map
 
 ```text
-  A → Σ (Q : Prop), A * Q
+  A → Σ (Q : Prop), B * Q
 ```
 
 where `- * Q` is the

From 98909e1e3e858fedbdbc837dd47a3d26f393b356 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 17:59:47 -0500
Subject: [PATCH 05/18] Update src/foundation/copartial-elements.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-elements.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index aad739a2d9..f4da7e9f53 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -29,7 +29,7 @@ A {{#concept "copartial element"}} of a type `A` is an element of type
 where the type `P * A` is the
 [join](synthetic-homotopy-theory.joins-of-types.md) of `P` and `A`. We say that
 a copartial element `(P , u)` is
-{{#concept "prohibited" Disambiguation="copartial element"}} if the proposition
+{{#concept "prohibited" Disambiguation="copartial element" Agda=is-prohibited-copartial-element}} if the [proposition](foundation-core.propositions.md)
 `P` holds.
 
 In order to compare copartial elements with

From 6183f9b02006380fc3bb70be1c82b523f69500d9 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:00:11 -0500
Subject: [PATCH 06/18] Update src/foundation/copartial-functions.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index e059fc2011..32b341457c 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -28,7 +28,7 @@ where `- * Q` is the
 [closed modality](orthogonal-factorization-systems.closed-modalities.md).
 
 A value of a copartial function `f` at `a : A` is said to be
-{{#concept "prohibited" Disambiguation="copartial function"}} if the copartial
+{{#concept "prohibited" Disambiguation="copartial function" Agda=is-prohibited-copartial-function}} if the copartial
 element `f a` of `B` is prohibited.
 
 **Note:** The topic of copartial functions is not known in the literature, and

From 7a3907375af95d3c6c4d82b5044c9805e81a9792 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:02:26 -0500
Subject: [PATCH 07/18] Update src/foundation/total-partial-elements.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/total-partial-elements.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/total-partial-elements.lagda.md b/src/foundation/total-partial-elements.lagda.md
index 2d3cf9604c..16df4f4925 100644
--- a/src/foundation/total-partial-elements.lagda.md
+++ b/src/foundation/total-partial-elements.lagda.md
@@ -19,7 +19,7 @@ open import foundation.universe-levels
 A [partial element](foundation.partial-elements.md) `a` of `A` is said to be
 {{#concept "total" Disambiguation="partial element"}} if it is defined. The type
 of total partial elements of `A` is
-[equivalent](foundation-core.equivalences.md) to the type `A`
+[equivalent](foundation-core.equivalences.md) to the type `A`.
 
 ## Definitions
 

From 9e576111849da2fc9a7c196fbe6039437923ef36 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:02:54 -0500
Subject: [PATCH 08/18] Update src/foundation/total-partial-functions.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/total-partial-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md
index 624af890db..a85567eff4 100644
--- a/src/foundation/total-partial-functions.lagda.md
+++ b/src/foundation/total-partial-functions.lagda.md
@@ -18,7 +18,7 @@ open import foundation.universe-levels
 ## Idea
 
 A [partial function](foundation.partial-functions.md) `f : A → B` is said to be
-{{#concept "total" Disambiguation="partial function"}} if the
+{{#concept "total" Disambiguation="partial function" Agda=is-total-partial-function}} if the
 [partial element](foundation.partial-elements.md) `f a` of `B` is defined for
 every `a : A`. The type of total partial functions from `A` to `B` is equivalent
 to the type of [functions](foundation-core.function-types.md) from `A` to `B`.

From da97d9b85a394eb480f1c6f08457dea9790c43ea Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:03:38 -0500
Subject: [PATCH 09/18] Update src/foundation/total-partial-functions.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/total-partial-functions.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md
index a85567eff4..6f776957b5 100644
--- a/src/foundation/total-partial-functions.lagda.md
+++ b/src/foundation/total-partial-functions.lagda.md
@@ -20,7 +20,7 @@ open import foundation.universe-levels
 A [partial function](foundation.partial-functions.md) `f : A → B` is said to be
 {{#concept "total" Disambiguation="partial function" Agda=is-total-partial-function}} if the
 [partial element](foundation.partial-elements.md) `f a` of `B` is defined for
-every `a : A`. The type of total partial functions from `A` to `B` is equivalent
+every `a : A`. The type of total partial functions from `A` to `B` is [equivalent](foundation-core.equivalences.md)
 to the type of [functions](foundation-core.function-types.md) from `A` to `B`.
 
 ## Definitions

From 1c816f78c8d80a4fc21be64ddf2c72f529a4599c Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:04:54 -0500
Subject: [PATCH 10/18] Update src/foundation/copartial-elements.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-elements.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index f4da7e9f53..aa3d0ebd38 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -20,7 +20,7 @@ open import orthogonal-factorization-systems.closed-modalities
 
 ## Idea
 
-A {{#concept "copartial element"}} of a type `A` is an element of type
+A {{#concept "copartial element" Agda=copartial-element}} of a type `A` is an element of type
 
 ```text
   Σ (Q : Prop), A * Q

From 3fb79e550f9284de485df014b6a21af546f6546c Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 12:35:36 -0500
Subject: [PATCH 11/18] explaining composition of copartial functions

---
 src/foundation/copartial-elements.lagda.md    | 76 ++++++++++++++-----
 src/foundation/copartial-functions.lagda.md   | 52 +++++++++----
 src/foundation/partial-elements.lagda.md      |  4 +-
 .../total-partial-functions.lagda.md          |  9 ++-
 4 files changed, 103 insertions(+), 38 deletions(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index aa3d0ebd38..1be11e918d 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -20,17 +20,18 @@ open import orthogonal-factorization-systems.closed-modalities
 
 ## Idea
 
-A {{#concept "copartial element" Agda=copartial-element}} of a type `A` is an element of type
+A {{#concept "copartial element" Agda=copartial-element}} of a type `A` is an
+element of type
 
 ```text
   Σ (Q : Prop), A * Q
 ```
 
-where the type `P * A` is the
-[join](synthetic-homotopy-theory.joins-of-types.md) of `P` and `A`. We say that
-a copartial element `(P , u)` is
-{{#concept "prohibited" Disambiguation="copartial element" Agda=is-prohibited-copartial-element}} if the [proposition](foundation-core.propositions.md)
-`P` holds.
+where the type `A * Q` is the
+[join](synthetic-homotopy-theory.joins-of-types.md) of `Q` and `A`. We say that
+a copartial element `(Q , u)` is
+{{#concept "erased" Disambiguation="copartial element" Agda=is-erased-copartial-element}}
+if the proposition `Q` holds.
 
 In order to compare copartial elements with
 [partial elements](foundation.partial-elements.md), note that we have the
@@ -42,23 +43,60 @@ following [pullback squares](foundation.pullback-squares.md)
   |                |                  |                |
   V                V                  V                V
   1 -----------> Prop                 1 -----------> Prop
-          ⊥                                   ⊥
+          F                                   F
 
   1 -----> Σ (Q : Prop), A * Q        A -----> Σ (P : Prop), (P → A)
   |                |                  |                |
   |                |                  |                |
   V                V                  V                V
   1 -----------> Prop                 1 -----------> Prop
-          ⊤                                   ⊤
+          T                                   T
 ```
 
 Note that we make use of the
 [closed modalities](orthogonal-factorization-systems.closed-modalities.md)
-`A ↦ P * A` in the formulation of copartial element, whereas the formulation of
+`A ↦ A * Q` in the formulation of copartial element, whereas the formulation of
 partial elements makes use of the
 [open modalities](orthogonal-factorization-systems.open-modalities.md). The
 concepts of partial and copartial elements are dual in that sense.
 
+Alternatively, the type of copartial elements of a type `A` can be defined as
+the [pushout-product](synthetic-homotopy-theory.pushout-products.md)
+
+```text
+    A   1
+    |   |
+  ! | □ | T
+    V   V
+    1  Prop
+```
+
+This point of view is useful in order to establish that copartial elements of
+copartial elements induce copartial elements. Indeed, note that
+`(A □ T) □ T ＝ A □ (T □ T)` by associativity of the pushout product, and that
+`T` is a pushout-product algebra in the sense that
+
+```text
+                                         P Q x ↦ (P * Q , x)
+    1     1       Σ (P Q : Prop), P * Q ---------------------> 1
+    |     |               |                                    |
+  T |  □  | T   =   T □ T |                                    |
+    V     V               V                                    V
+  Prop   Prop           Prop² ------------------------------> Prop
+                                       P Q ↦ P * Q
+```
+
+By this [morphism of arrows](foundation.morphisms-arrows.md) it follows that
+there is a morphism of arrows
+
+```text
+  (A □ T) □ T → A □ T,
+```
+
+i.e., that copartial copartial elements induce copartial elements. These
+considerations allow us to compose
+[copartial functions](foundation.copartial-functions.md).
+
 **Note:** The topic of copartial elements is not known in the literature, and
 our formalization on this topic should be considered experimental.
 
@@ -75,12 +113,12 @@ module _
   {l1 l2 : Level} {A : UU l1} (a : copartial-element l2 A)
   where
 
-  is-prohibited-prop-copartial-element : Prop l2
-  is-prohibited-prop-copartial-element = pr1 a
+  is-erased-prop-copartial-element : Prop l2
+  is-erased-prop-copartial-element = pr1 a
 
-  is-prohibited-copartial-element : UU l2
-  is-prohibited-copartial-element =
-    type-Prop is-prohibited-prop-copartial-element
+  is-erased-copartial-element : UU l2
+  is-erased-copartial-element =
+    type-Prop is-erased-prop-copartial-element
 ```
 
 ### The unit of the copartial element operator
@@ -90,13 +128,13 @@ module _
   {l1 : Level} {A : UU l1} (a : A)
   where
 
-  is-prohibited-prop-unit-copartial-element : Prop lzero
-  is-prohibited-prop-unit-copartial-element = empty-Prop
+  is-erased-prop-unit-copartial-element : Prop lzero
+  is-erased-prop-unit-copartial-element = empty-Prop
 
-  is-prohibited-unit-copartial-element : UU lzero
-  is-prohibited-unit-copartial-element = empty
+  is-erased-unit-copartial-element : UU lzero
+  is-erased-unit-copartial-element = empty
 
   unit-copartial-element : copartial-element lzero A
-  pr1 unit-copartial-element = is-prohibited-prop-unit-copartial-element
+  pr1 unit-copartial-element = is-erased-prop-unit-copartial-element
   pr2 unit-copartial-element = unit-closed-modality empty-Prop a
 ```
diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 32b341457c..3c328cc604 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -16,9 +16,10 @@ open import foundation.universe-levels
 
 ## Idea
 
-A {{#concept "copartial function" Agda=copartial-function}} from `A` to `B` is a map from `A` into the
-type of [copartial elements](foundation.copartial-elements.md) of `B`. I.e., a
-copartial function is a map
+A {{#concept "copartial function" Agda=copartial-function}} from `A` to `B` is a
+map from `A` into the type of
+[copartial elements](foundation.copartial-elements.md) of `B`. I.e., a copartial
+function is a map
 
 ```text
   A → Σ (Q : Prop), B * Q
@@ -28,11 +29,36 @@ where `- * Q` is the
 [closed modality](orthogonal-factorization-systems.closed-modalities.md).
 
 A value of a copartial function `f` at `a : A` is said to be
-{{#concept "prohibited" Disambiguation="copartial function" Agda=is-prohibited-copartial-function}} if the copartial
-element `f a` of `B` is prohibited.
+{{#concept "erased" Disambiguation="copartial function" Agda=is-erased-copartial-function}}
+if the copartial element `f a` of `B` is erased.
 
-**Note:** The topic of copartial functions is not known in the literature, and
-our formalization on this topic should be considered experimental.
+{{#concept "Composition of copartial functions"}} can be defined by
+
+```text
+                     Σ (Q : Prop), (Σ (P : Prop), C * P) * Q
+                            ∧                 |
+   map-copartial-element g /                  | μ
+                          /                   V
+  A ----> Σ (Q : Prop), B * Q       Σ (Q : Prop), C * Q
+      f
+```
+
+In this diagram, the map going up is defined by functoriality of the operation
+
+```text
+  X ↦ Σ (Q : Prop), X * Q
+```
+
+The map going down is defined by the pushout-product algebra structure of the
+map `T : 1 → Prop`. The main idea behind composition of copartial functions is
+that a composite of copartial function is erased on the union of the subtypes
+where each factor is erased. Indeed, if `f` is erased at `a` or
+`map-copartial-eleemnt g` is erased at the copartial element `f a` of `B`, then
+the composite of copartial functions `g ∘ f` should be erased at `a`.
+
+**Note:** The topic of copartial functions was not known to us in the
+literature, and our formalization on this topic should be considered
+experimental.
 
 ## Definitions
 
@@ -44,7 +70,7 @@ copartial-function :
 copartial-function l3 A B = A → copartial-element l3 B
 ```
 
-### Prohibited values of copartial functions
+### Erased values of copartial functions
 
 ```agda
 module _
@@ -52,12 +78,12 @@ module _
   (a : A)
   where
 
-  is-prohibited-prop-copartial-function : Prop l3
-  is-prohibited-prop-copartial-function =
-    is-prohibited-prop-copartial-element (f a)
+  is-erased-prop-copartial-function : Prop l3
+  is-erased-prop-copartial-function =
+    is-erased-prop-copartial-element (f a)
 
-  is-prohibited-copartial-function : UU l3
-  is-prohibited-copartial-function = is-prohibited-copartial-element (f a)
+  is-erased-copartial-function : UU l3
+  is-erased-copartial-function = is-erased-copartial-element (f a)
 ```
 
 ### Copartial functions obtained from functions
diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md
index fe260c49a9..11c346afb7 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -18,7 +18,7 @@ open import foundation-core.propositions
 
 ## Idea
 
-A {{#concept "partial element"}} of `X` consists of a
+A {{#concept "partial element" Agda=partial-element}} of `X` consists of a
 [proposition](foundation-core.propositions.md) `P` and a map `P → X`. We say
 that a partial element `(P, f)` is
 {{#concept "defined" Disambiguation="partial element"}} if the proposition `P`
@@ -63,5 +63,5 @@ This remains to be shown.
 
 - [Copartial elements](foundation.copartial-elements.md)
 - [Partial function](foundation.partial-functions.md)
-- [Partial sequences](elementary-number-theory.partial-sequences.md)
+- [Partial sequences](foundation.partial-sequences.md)
 - [Total partial functions](foundation.total-partial-functions.md)
diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md
index 6f776957b5..3e7c2e0660 100644
--- a/src/foundation/total-partial-functions.lagda.md
+++ b/src/foundation/total-partial-functions.lagda.md
@@ -18,10 +18,11 @@ open import foundation.universe-levels
 ## Idea
 
 A [partial function](foundation.partial-functions.md) `f : A → B` is said to be
-{{#concept "total" Disambiguation="partial function" Agda=is-total-partial-function}} if the
-[partial element](foundation.partial-elements.md) `f a` of `B` is defined for
-every `a : A`. The type of total partial functions from `A` to `B` is [equivalent](foundation-core.equivalences.md)
-to the type of [functions](foundation-core.function-types.md) from `A` to `B`.
+{{#concept "total" Disambiguation="partial function" Agda=is-total-partial-function}}
+if the [partial element](foundation.partial-elements.md) `f a` of `B` is defined
+for every `a : A`. The type of total partial functions from `A` to `B` is
+[equivalent](foundation-core.equivalences.md) to the type of
+[functions](foundation-core.function-types.md) from `A` to `B`.
 
 ## Definitions
 

From c11416ac05a18115db4bbbb57135b5e046795100 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 15:31:54 -0500
Subject: [PATCH 12/18] fix links

---
 src/foundation/copartial-functions.lagda.md | 21 +++++++++++++++++++--
 src/foundation/partial-functions.lagda.md   | 16 ++++++++++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)

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

From e154b1dbcbba8df74b6c3c53ad1c56f734a50e59 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 15:43:11 -0500
Subject: [PATCH 13/18] (co)partial dependent functions

---
 src/foundation/copartial-functions.lagda.md | 48 +++++++++++++++++--
 src/foundation/partial-functions.lagda.md   | 52 +++++++++++++++++++--
 2 files changed, 91 insertions(+), 9 deletions(-)

diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 431ac1f200..fb2e96c543 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -79,12 +79,37 @@ experimental.
 
 ## Definitions
 
+### Copartial dependent functions
+
+```agda
+copartial-dependent-function :
+  {l1 l2 : Level} (l3 : Level) (A : UU l1) → (A → UU l2) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+copartial-dependent-function l3 A B = (x : A) → copartial-element l3 (B x)
+```
+
 ### Copartial functions
 
 ```agda
 copartial-function :
   {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
-copartial-function l3 A B = A → copartial-element l3 B
+copartial-function l3 A B = copartial-dependent-function l3 A (λ _ → B)
+```
+
+### Erased values of copartial dependent functions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (f : copartial-dependent-function l3 A B) (a : A)
+  where
+
+  is-erased-prop-copartial-dependent-function : Prop l3
+  is-erased-prop-copartial-dependent-function =
+    is-erased-prop-copartial-element (f a)
+
+  is-erased-copartial-dependent-function : UU l3
+  is-erased-copartial-dependent-function = is-erased-copartial-element (f a)
 ```
 
 ### Erased values of copartial functions
@@ -97,10 +122,24 @@ module _
 
   is-erased-prop-copartial-function : Prop l3
   is-erased-prop-copartial-function =
-    is-erased-prop-copartial-element (f a)
+    is-erased-prop-copartial-dependent-function f a
 
   is-erased-copartial-function : UU l3
-  is-erased-copartial-function = is-erased-copartial-element (f a)
+  is-erased-copartial-function =
+    is-erased-copartial-dependent-function f a
+```
+
+### Copartial dependent functions obtained from dependent functions
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  copartial-dependent-function-dependent-function :
+    copartial-dependent-function lzero A B
+  copartial-dependent-function-dependent-function a =
+    unit-copartial-element (f a)
 ```
 
 ### Copartial functions obtained from functions
@@ -111,5 +150,6 @@ module _
   where
 
   copartial-function-function : copartial-function lzero A B
-  copartial-function-function a = unit-copartial-element (f a)
+  copartial-function-function =
+    copartial-dependent-function-dependent-function f
 ```
diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md
index 461c072dec..48b08e0e37 100644
--- a/src/foundation/partial-functions.lagda.md
+++ b/src/foundation/partial-functions.lagda.md
@@ -46,15 +46,42 @@ where the composition operation is
 
 ## Definitions
 
+### Partial dependent functions
+
+```agda
+partial-dependent-function :
+  {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+partial-dependent-function l3 A B =
+  (x : A) → partial-element l3 (B x)
+```
+
 ### Partial functions
 
 ```agda
 partial-function :
   {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
-partial-function l3 A B = A → partial-element l3 B
+partial-function l3 A B = partial-dependent-function l3 A (λ _ → B)
 ```
 
-### The predicate of being defined at an element in the domain
+### The predicate on partial dependent functions of being defined at an element in the domain
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (f : partial-dependent-function l3 A B) (a : A)
+  where
+
+  is-defined-prop-partial-dependent-function : Prop l3
+  is-defined-prop-partial-dependent-function =
+    is-defined-prop-partial-element (f a)
+
+  is-defined-partial-dependent-function : UU l3
+  is-defined-partial-dependent-function =
+    type-Prop is-defined-prop-partial-dependent-function
+```
+
+### The predicate on partial functions of being defined at an element in the domain
 
 ```agda
 module _
@@ -63,10 +90,25 @@ module _
   where
 
   is-defined-prop-partial-function : Prop l3
-  is-defined-prop-partial-function = is-defined-prop-partial-element (f a)
+  is-defined-prop-partial-function =
+    is-defined-prop-partial-dependent-function f a
 
   is-defined-partial-function : UU l3
-  is-defined-partial-function = type-Prop is-defined-prop-partial-function
+  is-defined-partial-function =
+    is-defined-partial-dependent-function f a
+```
+
+### The partial dependent function obtained from a dependent function
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  partial-dependent-function-dependent-function :
+    partial-dependent-function lzero A B
+  partial-dependent-function-dependent-function a =
+    unit-partial-element (f a)
 ```
 
 ### The partial function obtained from a function
@@ -77,7 +119,7 @@ module _
   where
 
   partial-function-function : partial-function lzero A B
-  partial-function-function a = unit-partial-element (f a)
+  partial-function-function = partial-dependent-function-dependent-function f
 ```
 
 ## See also

From f78929595c3321f0cbe6363e02be8e63615d911d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 15:53:12 -0500
Subject: [PATCH 14/18] remark about partial elements defined in terms of
 composition of polynomial endofunctors

---
 src/foundation/partial-elements.lagda.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md
index 11c346afb7..db8b8e7feb 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -24,6 +24,23 @@ that a partial element `(P, f)` is
 {{#concept "defined" Disambiguation="partial element"}} if the proposition `P`
 holds.
 
+Alternatively, the type of partial elements of `X` can be descibed as the
+codomain of the
+[composition](species.composition-cauchy-series-species-of-types.md)
+
+```text
+    1   ∅     ∅
+    |   |     |
+  T | ∘ |  =  |
+    V   V     V
+  Prop  X   P T X
+```
+
+of [polynomial-endofunctors.md](trees.polynomial-endofunctors.md). Indeed, the
+codomain of this composition operation of morphisms is the polynomial
+endofunctor `P T` of the map `T : 1 → Prop` evaluated at `X`, which is exactly
+the type of partial elements of `X`.
+
 ## Definitions
 
 ### Partial elements of a type

From e3090eee459f42541f26e9fd5069f68bff744b7e Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 16:05:05 -0500
Subject: [PATCH 15/18] sentence

---
 src/foundation/copartial-elements.lagda.md  |  5 +++--
 src/foundation/copartial-functions.lagda.md | 14 +++++++++-----
 src/foundation/partial-elements.lagda.md    | 11 +++++++++--
 3 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index 1be11e918d..e34f8bcc53 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -97,8 +97,9 @@ i.e., that copartial copartial elements induce copartial elements. These
 considerations allow us to compose
 [copartial functions](foundation.copartial-functions.md).
 
-**Note:** The topic of copartial elements is not known in the literature, and
-our formalization on this topic should be considered experimental.
+**Note:** The topic of copartial functions was not known to us in the
+literature, and our formalization on this topic should be considered
+experimental.
 
 ## Definition
 
diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index fb2e96c543..947a60a0ff 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -37,11 +37,11 @@ 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
+     A     B   1
+     |     |   |
+  id |  ⇒  | □ | T
+     V     V   V
+     A     1  Prop
 ```
 
 where `□` is the
@@ -153,3 +153,7 @@ module _
   copartial-function-function =
     copartial-dependent-function-dependent-function f
 ```
+
+## See also
+
+- [Partial functions](foundation.partial-functions.md)
diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md
index db8b8e7feb..5b6cb7b9e7 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -19,7 +19,14 @@ open import foundation-core.propositions
 ## Idea
 
 A {{#concept "partial element" Agda=partial-element}} of `X` consists of a
-[proposition](foundation-core.propositions.md) `P` and a map `P → X`. We say
+[proposition](foundation-core.propositions.md) `P` and a map `P → X`. That is,
+the type of partial elements of `X` is defined to be
+
+```text
+  Σ (P : Prop), (P → X).
+```
+
+We say
 that a partial element `(P, f)` is
 {{#concept "defined" Disambiguation="partial element"}} if the proposition `P`
 holds.
@@ -79,6 +86,6 @@ This remains to be shown.
 ## See also
 
 - [Copartial elements](foundation.copartial-elements.md)
-- [Partial function](foundation.partial-functions.md)
+- [Partial functions](foundation.partial-functions.md)
 - [Partial sequences](foundation.partial-sequences.md)
 - [Total partial functions](foundation.total-partial-functions.md)

From d47c818dc9b1c8bd5022a7a27d9ba2a06991624a Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 16:05:36 -0500
Subject: [PATCH 16/18] make pre-commit

---
 src/foundation/partial-elements.lagda.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md
index 5b6cb7b9e7..ca67ef0cb8 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -26,8 +26,7 @@ the type of partial elements of `X` is defined to be
   Σ (P : Prop), (P → X).
 ```
 
-We say
-that a partial element `(P, f)` is
+We say that a partial element `(P, f)` is
 {{#concept "defined" Disambiguation="partial element"}} if the proposition `P`
 holds.
 

From c79858465eb4532789f5bc17b984cb05f1b267c8 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 16:11:57 -0500
Subject: [PATCH 17/18] clarifying construction of composition of copartial
 functions

---
 src/foundation/copartial-elements.lagda.md  |  2 +-
 src/foundation/copartial-functions.lagda.md | 19 ++++++++++---------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index e34f8bcc53..50b76e3169 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -90,7 +90,7 @@ By this [morphism of arrows](foundation.morphisms-arrows.md) it follows that
 there is a morphism of arrows
 
 ```text
-  (A □ T) □ T → A □ T,
+  join-copartial-element : (A □ T) □ T → A □ T,
 ```
 
 i.e., that copartial copartial elements induce copartial elements. These
diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index 947a60a0ff..b09633c4ad 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -52,11 +52,11 @@ domain of the pushout-product `B □ T` is the type of copartial elements of `B`
 functions can be defined by
 
 ```text
-                     Σ (Q : Prop), (Σ (P : Prop), C * P) * Q
+                     copartial-element (copartial-element C)
                             ∧                 |
-   map-copartial-element g /                  | μ
+   map-copartial-element g /                  | join-copartial-element
                           /                   V
-  A ----> Σ (Q : Prop), B * Q       Σ (Q : Prop), C * Q
+  A ----> copartial-element B       copartial-element C
       f
 ```
 
@@ -66,12 +66,13 @@ In this diagram, the map going up is defined by functoriality of the operation
   X ↦ Σ (Q : Prop), X * Q
 ```
 
-The map going down is defined by the pushout-product algebra structure of the
-map `T : 1 → Prop`. The main idea behind composition of copartial functions is
-that a composite of copartial function is erased on the union of the subtypes
-where each factor is erased. Indeed, if `f` is erased at `a` or
-`map-copartial-eleemnt g` is erased at the copartial element `f a` of `B`, then
-the composite of copartial functions `g ∘ f` should be erased at `a`.
+The map going down is defined by the join operation on copartial elements, i.e.,
+the pushout-product algebra structure of the map `T : 1 → Prop`. The main idea
+behind composition of copartial functions is that a composite of copartial
+function is erased on the union of the subtypes where each factor is erased.
+Indeed, if `f` is erased at `a` or `map-copartial-eleemnt g` is erased at the
+copartial element `f a` of `B`, then the composite of copartial functions
+`g ∘ f` should be erased at `a`.
 
 **Note:** The topic of copartial functions was not known to us in the
 literature, and our formalization on this topic should be considered

From c9670dc8f840b520b09259476fa2caae6487b82b Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 7 Dec 2023 16:18:52 -0500
Subject: [PATCH 18/18] Update src/foundation/copartial-elements.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-elements.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index 50b76e3169..85cb76b1ce 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -39,14 +39,14 @@ following [pullback squares](foundation.pullback-squares.md)
 
 ```text
   A -----> Σ (Q : Prop), A * Q        1 -----> Σ (P : Prop), (P → A)
-  |                |                  |                |
+  | ⌟              |                  | ⌟              |
   |                |                  |                |
   V                V                  V                V
   1 -----------> Prop                 1 -----------> Prop
           F                                   F
 
   1 -----> Σ (Q : Prop), A * Q        A -----> Σ (P : Prop), (P → A)
-  |                |                  |                |
+  | ⌟              |                  | ⌟              |
   |                |                  |                |
   V                V                  V                V
   1 -----------> Prop                 1 -----------> Prop