small addendum to copartial elements, and proposal of erased -> denied (

#977)

Calling `f` to be erased at `a` suggests that a value of `f` at `a`
existed, but this is not accurate. Instead we propose to say that
"evaluation of `f` at `a` is denied". The main example is to deny
evaluation of the fraction `1/0` is denied, because division by 0 is not
possible.

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
+```

src/foundation/copartial-functions.lagda.md

@@ -8,6 +8,7 @@ module foundation.copartial-functions where
 
 ```agda
 open import foundation.copartial-elements
+open import foundation.partial-functions
 open import foundation.propositions
 open import foundation.universe-levels
 ```
@@ -29,9 +30,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 +70,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-element 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,37 +98,37 @@ 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 _
   {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-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 _
   {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-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
@@ -155,6 +156,34 @@ module _
     copartial-dependent-function-dependent-function f
 ```
 
+## Properties
+
+### The underlying partial dependent function of a copartial dependent function
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (f : copartial-dependent-function l3 A B)
+  where
+
+  partial-dependent-function-copartial-dependent-function :
+    partial-dependent-function l3 A B
+  partial-dependent-function-copartial-dependent-function a =
+    partial-element-copartial-element (f a)
+```
+
+### The underlying partial function of a copartial function
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
+  where
+
+  partial-function-copartial-function : partial-function l3 A B
+  partial-function-copartial-function a =
+    partial-element-copartial-element (f a)
+```
+
 ## See also
 
 - [Partial functions](foundation.partial-functions.md)

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