explaining composition of copartial functions

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

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,20 +70,20 @@ copartial-function :
 copartial-function l3 A B = A → copartial-element l3 B
 ```
 
-### Prohibited values of copartial functions
+### 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-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

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)

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