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..85cb76b1ce
--- /dev/null
+++ b/src/foundation/copartial-elements.lagda.md
@@ -0,0 +1,141 @@
+# 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" Agda=copartial-element}} of a type `A` is an
+element of type
+
+```text
+  Σ (Q : Prop), A * Q
+```
+
+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
+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
+          T                                   T
+```
+
+Note that we make use of the
+[closed modalities](orthogonal-factorization-systems.closed-modalities.md)
+`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
+  join-copartial-element : (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 functions was not known to us 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-erased-prop-copartial-element : Prop l2
+  is-erased-prop-copartial-element = pr1 a
+
+  is-erased-copartial-element : UU l2
+  is-erased-copartial-element =
+    type-Prop is-erased-prop-copartial-element
+```
+
+### The unit of the copartial element operator
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} (a : A)
+  where
+
+  is-erased-prop-unit-copartial-element : Prop lzero
+  is-erased-prop-unit-copartial-element = empty-Prop
+
+  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-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
new file mode 100644
index 0000000000..b09633c4ad
--- /dev/null
+++ b/src/foundation/copartial-functions.lagda.md
@@ -0,0 +1,160 @@
+# 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" 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
+```
+
+where `- * Q` is the
+[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.
+
+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
+                     copartial-element (copartial-element C)
+                            ∧                 |
+   map-copartial-element g /                  | join-copartial-element
+                          /                   V
+  A ----> copartial-element B       copartial-element C
+      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 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
+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 = 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
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
+  (a : A)
+  where
+
+  is-erased-prop-copartial-function : Prop l3
+  is-erased-prop-copartial-function =
+    is-erased-prop-copartial-dependent-function f a
+
+  is-erased-copartial-function : UU l3
+  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
+
+```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 =
+    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 a66e1fdb39..ca67ef0cb8 100644
--- a/src/foundation/partial-elements.lagda.md
+++ b/src/foundation/partial-elements.lagda.md
@@ -18,24 +18,59 @@ open import foundation-core.propositions
 
 ## Idea
 
-A **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.
+A {{#concept "partial element" Agda=partial-element}} of `X` consists of a
+[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.
+
+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
 
 ```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 +81,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 functions](foundation.partial-functions.md)
+- [Partial sequences](foundation.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..48b08e0e37
--- /dev/null
+++ b/src/foundation/partial-functions.lagda.md
@@ -0,0 +1,129 @@
+# 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.
+
+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 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 = partial-dependent-function l3 A (λ _ → B)
+```
+
+### 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 _
+  {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-dependent-function f a
+
+  is-defined-partial-function : UU l3
+  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
+
+```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 = partial-dependent-function-dependent-function f
+```
+
+## 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..dd8e77715c
--- /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 `ℕ` to `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..16df4f4925
--- /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..3e7c2e0660
--- /dev/null
+++ b/src/foundation/total-partial-functions.lagda.md
@@ -0,0 +1,51 @@
+# 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" 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
+
+### 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 =