diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index 85cb76b1ce..fa925d94c1 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -9,11 +9,15 @@ module foundation.copartial-elements where
 ```agda
 open import foundation.dependent-pair-types
 open import foundation.empty-types
+open import foundation.negation
+open import foundation.partial-elements
 open import foundation.universe-levels
 
 open import foundation-core.propositions
 
 open import orthogonal-factorization-systems.closed-modalities
+
+open import synthetic-homotopy-theory.joins-of-types
 ```
 
 </details>
@@ -29,8 +33,8 @@ element of type
 
 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}}
+evaluation of a copartial element `(Q , u)` is
+{{#concept "denied" Disambiguation="copartial element" Agda=is-denied-copartial-element}}
 if the proposition `Q` holds.
 
 In order to compare copartial elements with
@@ -114,12 +118,16 @@ 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-denied-prop-copartial-element : Prop l2
+  is-denied-prop-copartial-element = pr1 a
+
+  is-denied-copartial-element : UU l2
+  is-denied-copartial-element =
+    type-Prop is-denied-prop-copartial-element
 
-  is-erased-copartial-element : UU l2
-  is-erased-copartial-element =
-    type-Prop is-erased-prop-copartial-element
+  value-copartial-element :
+    operator-closed-modality is-denied-prop-copartial-element A
+  value-copartial-element = pr2 a
 ```
 
 ### The unit of the copartial element operator
@@ -129,13 +137,42 @@ 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-denied-prop-unit-copartial-element : Prop lzero
+  is-denied-prop-unit-copartial-element = empty-Prop
 
-  is-erased-unit-copartial-element : UU lzero
-  is-erased-unit-copartial-element = empty
+  is-denied-unit-copartial-element : UU lzero
+  is-denied-unit-copartial-element = empty
 
   unit-copartial-element : copartial-element lzero A
-  pr1 unit-copartial-element = is-erased-prop-unit-copartial-element
+  pr1 unit-copartial-element = is-denied-prop-unit-copartial-element
   pr2 unit-copartial-element = unit-closed-modality empty-Prop a
 ```
+
+## Properties
+
+### Forgetful map from copartial elements to partial elements
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (a : copartial-element l2 A)
+  where
+
+  is-defined-prop-partial-element-copartial-element : Prop l2
+  is-defined-prop-partial-element-copartial-element =
+    neg-Prop (is-denied-prop-copartial-element a)
+
+  is-defined-partial-element-copartial-element : UU l2
+  is-defined-partial-element-copartial-element =
+    type-Prop is-defined-prop-partial-element-copartial-element
+
+  value-partial-element-copartial-element :
+    is-defined-partial-element-copartial-element → A
+  value-partial-element-copartial-element f =
+    map-inv-right-unit-law-join-is-empty f (value-copartial-element a)
+
+  partial-element-copartial-element : partial-element l2 A
+  pr1 partial-element-copartial-element =
+    is-defined-prop-partial-element-copartial-element
+  pr2 partial-element-copartial-element =
+    value-partial-element-copartial-element
+```
diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md
index b09633c4ad..24c8672bbc 100644
--- a/src/foundation/copartial-functions.lagda.md
+++ b/src/foundation/copartial-functions.lagda.md
@@ -29,9 +29,9 @@ 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.
+Evaluation of a copartial function `f` at `a : A` is said to be
+{{#concept "denied" Disambiguation="copartial function" Agda=is-denied-copartial-function}}
+if evaluation of the copartial element `f a` of `B` is denied.
 
 A copartial function is [equivalently](foundation-core.equivalences.md)
 described as a [morphism of arrows](foundation.morphisms-arrows.md)
@@ -69,10 +69,10 @@ In this diagram, the map going up is defined by functoriality of the operation
 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
+function is denied on the union of the subtypes where each factor is denied.
+Indeed, if `f` is denied at `a` or `map-copartial-eleemnt g` is denied at the
 copartial element `f a` of `B`, then the composite of copartial functions
-`g ∘ f` should be erased at `a`.
+`g ∘ f` should be denied 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
@@ -97,7 +97,7 @@ copartial-function :
 copartial-function l3 A B = copartial-dependent-function l3 A (λ _ → B)
 ```
 
-### Erased values of copartial dependent functions
+### Denied values of copartial dependent functions
 
 ```agda
 module _
@@ -105,15 +105,15 @@ module _
   (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-denied-prop-copartial-dependent-function : Prop l3
+  is-denied-prop-copartial-dependent-function =
+    is-denied-prop-copartial-element (f a)
 
-  is-erased-copartial-dependent-function : UU l3
-  is-erased-copartial-dependent-function = is-erased-copartial-element (f a)
+  is-denied-copartial-dependent-function : UU l3
+  is-denied-copartial-dependent-function = is-denied-copartial-element (f a)
 ```
 
-### Erased values of copartial functions
+### Denied values of copartial functions
 
 ```agda
 module _
@@ -121,13 +121,13 @@ module _
   (a : A)
   where
 
-  is-erased-prop-copartial-function : Prop l3
-  is-erased-prop-copartial-function =
-    is-erased-prop-copartial-dependent-function f a
+  is-denied-prop-copartial-function : Prop l3
+  is-denied-prop-copartial-function =
+    is-denied-prop-copartial-dependent-function f a
 
-  is-erased-copartial-function : UU l3
-  is-erased-copartial-function =
-    is-erased-copartial-dependent-function f a
+  is-denied-copartial-function : UU l3
+  is-denied-copartial-function =
+    is-denied-copartial-dependent-function f a
 ```
 
 ### Copartial dependent functions obtained from dependent functions
diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
index dfe5bf58f0..091a6b922d 100644
--- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
@@ -169,6 +169,12 @@ right-unit-law-join-is-empty :
 pr1 (right-unit-law-join-is-empty is-empty-B) = inl-join
 pr2 (right-unit-law-join-is-empty is-empty-B) =
   is-equiv-inl-join-is-empty is-empty-B
+
+map-inv-right-unit-law-join-is-empty :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  is-empty B → A * B → A
+map-inv-right-unit-law-join-is-empty H =
+  map-inv-equiv (right-unit-law-join-is-empty H)
 ```
 
 ### The left zero law for joins