From 3fb79e550f9284de485df014b6a21af546f6546c Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 7 Dec 2023 12:35:36 -0500 Subject: [PATCH] explaining composition of copartial functions --- src/foundation/copartial-elements.lagda.md | 76 ++++++++++++++----- src/foundation/copartial-functions.lagda.md | 52 +++++++++---- src/foundation/partial-elements.lagda.md | 4 +- .../total-partial-functions.lagda.md | 9 ++- 4 files changed, 103 insertions(+), 38 deletions(-) diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md index aa3d0ebd38..1be11e918d 100644 --- a/src/foundation/copartial-elements.lagda.md +++ b/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 ``` diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md index 32b341457c..3c328cc604 100644 --- a/src/foundation/copartial-functions.lagda.md +++ b/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,7 +70,7 @@ copartial-function : copartial-function l3 A B = A → copartial-element l3 B ``` -### Prohibited values of copartial functions +### Erased values of copartial functions ```agda module _ @@ -52,12 +78,12 @@ module _ (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 diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md index fe260c49a9..11c346afb7 100644 --- a/src/foundation/partial-elements.lagda.md +++ b/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) diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md index 6f776957b5..3e7c2e0660 100644 --- a/src/foundation/total-partial-functions.lagda.md +++ b/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