From fa4069270488cdc7902de7fc0c2a30e1d0080001 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 7 Dec 2023 16:33:59 -0500 Subject: [PATCH] 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 | 6 + src/foundation/copartial-elements.lagda.md | 141 +++++++++++++++ src/foundation/copartial-functions.lagda.md | 160 ++++++++++++++++++ src/foundation/partial-elements.lagda.md | 62 +++++-- src/foundation/partial-functions.lagda.md | 129 ++++++++++++++ src/foundation/partial-sequences.lagda.md | 53 ++++++ .../total-partial-elements.lagda.md | 33 ++++ .../total-partial-functions.lagda.md | 51 ++++++ .../closed-modalities.lagda.md | 8 +- 9 files changed, 629 insertions(+), 14 deletions(-) create mode 100644 src/foundation/copartial-elements.lagda.md create mode 100644 src/foundation/copartial-functions.lagda.md create mode 100644 src/foundation/partial-functions.lagda.md create mode 100644 src/foundation/partial-sequences.lagda.md create mode 100644 src/foundation/total-partial-elements.lagda.md create mode 100644 src/foundation/total-partial-functions.lagda.md diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 3ce72252c2..55a3c1bc23 100644 --- a/src/foundation.lagda.md +++ b/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 diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md new file mode 100644 index 0000000000..85cb76b1ce --- /dev/null +++ b/src/foundation/copartial-elements.lagda.md @@ -0,0 +1,141 @@ +# Copartial elements + +```agda +module foundation.copartial-elements where +``` + +
Imports + +```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 +``` + +
+ +## 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 +``` diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md new file mode 100644 index 0000000000..b09633c4ad --- /dev/null +++ b/src/foundation/copartial-functions.lagda.md @@ -0,0 +1,160 @@ +# Copartial functions + +```agda +module foundation.copartial-functions where +``` + +
Imports + +```agda +open import foundation.copartial-elements +open import foundation.propositions +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 + +```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) diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md index a66e1fdb39..ca67ef0cb8 100644 --- a/src/foundation/partial-elements.lagda.md +++ b/src/foundation/partial-elements.lagda.md @@ -18,24 +18,59 @@ open import foundation-core.propositions ## Idea -A **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 **defined** if the proposition `P` holds. +A {{#concept "partial element" Agda=partial-element}} of `X` consists of a +[proposition](foundation-core.propositions.md) `P` and a map `P → X`. That is, +the type of partial elements of `X` is defined to be + +```text + Σ (P : Prop), (P → X). +``` + +We say that a partial element `(P, f)` is +{{#concept "defined" Disambiguation="partial element"}} if the proposition `P` +holds. + +Alternatively, the type of partial elements of `X` can be descibed as the +codomain of the +[composition](species.composition-cauchy-series-species-of-types.md) + +```text + 1 ∅ ∅ + | | | + T | ∘ | = | + V V V + Prop X P T X +``` + +of [polynomial-endofunctors.md](trees.polynomial-endofunctors.md). Indeed, the +codomain of this composition operation of morphisms is the polynomial +endofunctor `P T` of the map `T : 1 → Prop` evaluated at `X`, which is exactly +the type of partial elements of `X`. + +## Definitions + +### Partial elements of a type ```agda partial-element : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) partial-element l2 X = Σ (Prop l2) (λ P → type-Prop P → X) -is-defined-partial-element-Prop : - {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → Prop l2 -is-defined-partial-element-Prop x = pr1 x +module _ + {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) + where + + is-defined-prop-partial-element : Prop l2 + is-defined-prop-partial-element = pr1 x + + is-defined-partial-element : UU l2 + is-defined-partial-element = type-Prop is-defined-prop-partial-element +``` -is-defined-partial-element : - {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → UU l2 -is-defined-partial-element x = type-Prop (is-defined-partial-element-Prop x) +### The unit of the partial element operator +```agda unit-partial-element : - {l1 l2 : Level} {X : UU l1} → X → partial-element lzero X + {l1 : Level} {X : UU l1} → X → partial-element lzero X pr1 (unit-partial-element x) = unit-Prop pr2 (unit-partial-element x) y = x ``` @@ -46,3 +81,10 @@ pr2 (unit-partial-element x) y = x This remains to be shown. [#734](https://github.com/UniMath/agda-unimath/issues/734) + +## See also + +- [Copartial elements](foundation.copartial-elements.md) +- [Partial functions](foundation.partial-functions.md) +- [Partial sequences](foundation.partial-sequences.md) +- [Total partial functions](foundation.total-partial-functions.md) diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md new file mode 100644 index 0000000000..48b08e0e37 --- /dev/null +++ b/src/foundation/partial-functions.lagda.md @@ -0,0 +1,129 @@ +# Partial functions + +```agda +module foundation.partial-functions where +``` + +
Imports + +```agda +open import foundation.partial-elements +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "partial function"}} from `A` to `B` is a function from `A` into +the type of [partial elements](foundation.partial-elements.md) of `B`. In other +words, a partial function is a function + +```text + A → Σ (P : Prop), (P → B). +``` + +Given a partial function `f : A → B` and an element `a : A`, we say that `f` is +{{#concept "defined" Disambiguation="partial function"}} at `a` if the partial +element `f a` of `A` is defined. + +Partial functions can be described +[equivalently](foundation-core.equivalences.md) as +[morphisms of arrows](foundation.morphisms-arrows.md) + +```text + ∅ 1 ∅ + | | | + | ⇒ | ∘ | + V V V + A Prop B +``` + +where the composition operation is +[composition](species.composition-cauchy-series-species-of-types.md) of +[polynomial endofunctors](trees.polynomial-endofunctors.md). + +## Definitions + +### Partial dependent functions + +```agda +partial-dependent-function : + {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) → + UU (l1 ⊔ l2 ⊔ lsuc l3) +partial-dependent-function l3 A B = + (x : A) → partial-element l3 (B x) +``` + +### Partial functions + +```agda +partial-function : + {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3) +partial-function l3 A B = partial-dependent-function l3 A (λ _ → B) +``` + +### The predicate on partial dependent functions of being defined at an element in the domain + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} + (f : partial-dependent-function l3 A B) (a : A) + where + + is-defined-prop-partial-dependent-function : Prop l3 + is-defined-prop-partial-dependent-function = + is-defined-prop-partial-element (f a) + + is-defined-partial-dependent-function : UU l3 + is-defined-partial-dependent-function = + type-Prop is-defined-prop-partial-dependent-function +``` + +### The predicate on partial functions of being defined at an element in the domain + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B) + (a : A) + where + + is-defined-prop-partial-function : Prop l3 + is-defined-prop-partial-function = + is-defined-prop-partial-dependent-function f a + + is-defined-partial-function : UU l3 + is-defined-partial-function = + is-defined-partial-dependent-function f a +``` + +### The partial dependent function obtained from a dependent function + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) + where + + partial-dependent-function-dependent-function : + partial-dependent-function lzero A B + partial-dependent-function-dependent-function a = + unit-partial-element (f a) +``` + +### The partial function obtained from a function + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + partial-function-function : partial-function lzero A B + partial-function-function = partial-dependent-function-dependent-function f +``` + +## See also + +- [Copartial functions](foundation.copartial-functions.md) +- [Partial elements](foundation.partial-elements.md) +- [Partial sequences](foundation.partial-sequences.md) diff --git a/src/foundation/partial-sequences.lagda.md b/src/foundation/partial-sequences.lagda.md new file mode 100644 index 0000000000..dd8e77715c --- /dev/null +++ b/src/foundation/partial-sequences.lagda.md @@ -0,0 +1,53 @@ +# Partial sequences + +```agda +module foundation.partial-sequences where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.partial-functions +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "partial sequence"}} of elements of a type `A` is a +[partial function](foundation.partial-functions.md) from `ℕ` to `A`. In other +words, a partial sequence is a map + +```text + ℕ → Σ (P : Prop), (P → A) +``` + +from `ℕ` into the type of [partial elements](foundation.partial-elements.md) of +`A`. + +## Definitions + +### Partial sequences + +```agda +partial-sequence : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +partial-sequence l2 A = partial-function l2 ℕ A +``` + +### Defined elements of partial sequences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (a : partial-sequence l2 A) + where + + is-defined-prop-partial-sequence : ℕ → Prop l2 + is-defined-prop-partial-sequence = is-defined-prop-partial-function a + + is-defined-partial-sequence : ℕ → UU l2 + is-defined-partial-sequence = is-defined-partial-function a +``` diff --git a/src/foundation/total-partial-elements.lagda.md b/src/foundation/total-partial-elements.lagda.md new file mode 100644 index 0000000000..16df4f4925 --- /dev/null +++ b/src/foundation/total-partial-elements.lagda.md @@ -0,0 +1,33 @@ +# Total partial elements + +```agda +module foundation.total-partial-elements where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.partial-elements +open import foundation.universe-levels +``` + +
+ +## Idea + +A [partial element](foundation.partial-elements.md) `a` of `A` is said to be +{{#concept "total" Disambiguation="partial element"}} if it is defined. The type +of total partial elements of `A` is +[equivalent](foundation-core.equivalences.md) to the type `A`. + +## Definitions + +### The type of total partial elements + +```agda +total-partial-element : + {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +total-partial-element l2 A = + Σ (partial-element l2 A) is-defined-partial-element +``` diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md new file mode 100644 index 0000000000..3e7c2e0660 --- /dev/null +++ b/src/foundation/total-partial-functions.lagda.md @@ -0,0 +1,51 @@ +# Total partial functions + +```agda +module foundation.total-partial-functions where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.partial-functions +open import foundation.propositions +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`. + +## Definitions + +### The predicate of being a total partial function + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B) + where + + is-total-prop-partial-function : Prop (l1 ⊔ l3) + is-total-prop-partial-function = + Π-Prop A (is-defined-prop-partial-function f) + + is-total-partial-function : UU (l1 ⊔ l3) + is-total-partial-function = type-Prop is-total-prop-partial-function +``` + +### The type of total partial functions + +```agda +total-partial-function : + {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3) +total-partial-function l3 A B = + Σ (partial-function l3 A B) is-total-partial-function +``` diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md index 0b18cf063c..7c79d77436 100644 --- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -38,11 +38,11 @@ call these the **closed modalities**. ```agda operator-closed-modality : - (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) -operator-closed-modality l Q A = A * type-Prop Q + {l lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) +operator-closed-modality Q A = A * type-Prop Q unit-closed-modality : - {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q) + {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality {l} Q) unit-closed-modality Q = inl-join is-closed-modal : @@ -63,7 +63,7 @@ module _ is-reflective-subuniverse-closed-modality : is-reflective-subuniverse {l ⊔ lQ} (is-closed-modal Q) pr1 is-reflective-subuniverse-closed-modality = - operator-closed-modality (l ⊔ lQ) Q + operator-closed-modality {l ⊔ lQ} Q pr1 (pr2 is-reflective-subuniverse-closed-modality) = unit-closed-modality Q pr1 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) A q =