Partial and copartial functions

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)