Partial and copartial functions (#975)

This PR adds partial and copartial functions to the library. Partial
functions were needed to define partial sequences, which are ultimately
needed for some OEIS entries. Copartial functions are simply the dual of
partial functions, which I came up with while formalizing partial
functions.

Note that partial functions are defined using the open modalities, so
naturally copartial functions are defined using the closed modalities.
They specify where a function is prohibited. The terminology in the
files about copartial functions is not established in the literature (as
far as I know), and should be considered experimental.

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

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

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)