Copartial functions

Content created by Egbert Rijke.

Created on 2023-12-07.
Last modified on 2024-04-25.

module foundation.copartial-functions where
Imports 
open import foundation.copartial-elements
open import foundation.partial-functions
open import foundation.propositions
open import foundation.universe-levels

Idea

A copartial function from A to B is a map from A into the type of copartial elements of B. I.e., a copartial function is a map

  A → Σ (Q : Prop), B * Q

where - * Q is the closed modality, which is defined by the join operation.

Evaluation of a copartial function f at a : A is said to be denied if evaluation of the copartial element f a of B is denied.

A copartial function is equivalently described as a morphism of arrows

     A     B   1
     |     |   |
  id |  ⇒  | □ | T
     ∨     ∨   ∨
     A     1  Prop

where □ is the pushout-product. Indeed, the domain of the pushout-product B □ T is the type of copartial elements of B.

Composition of copartial functions can be defined by

                     copartial-element (copartial-element C)
                            ∧                 |
   map-copartial-element g /                  | join-copartial-element
                          /                   ∨
  A ----> copartial-element B       copartial-element C
      f

In this diagram, the map going up is defined by functoriality of the operation

  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 denied on the union of the subtypes where each factor is denied. Indeed, if f is denied at a or map-copartial-element g is denied at the copartial element f a of B, then the composite of copartial functions g ∘ f should be denied 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

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

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)

Denied values of copartial dependent functions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (f : copartial-dependent-function l3 A B) (a : A)
  where

  is-denied-prop-copartial-dependent-function : Prop l3
  is-denied-prop-copartial-dependent-function =
    is-denied-prop-copartial-element (f a)

  is-denied-copartial-dependent-function : UU l3
  is-denied-copartial-dependent-function = is-denied-copartial-element (f a)

Denied values of copartial functions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
  (a : A)
  where

  is-denied-prop-copartial-function : Prop l3
  is-denied-prop-copartial-function =
    is-denied-prop-copartial-dependent-function f a

  is-denied-copartial-function : UU l3
  is-denied-copartial-function =
    is-denied-copartial-dependent-function f a

Copartial dependent functions obtained from dependent functions

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

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

Properties

The underlying partial dependent function of a copartial dependent function

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (f : copartial-dependent-function l3 A B)
  where

  partial-dependent-function-copartial-dependent-function :
    partial-dependent-function l3 A B
  partial-dependent-function-copartial-dependent-function a =
    partial-element-copartial-element (f a)

The underlying partial function of a copartial function

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
  where

  partial-function-copartial-function : partial-function l3 A B
  partial-function-copartial-function a =
    partial-element-copartial-element (f a)

See also

Recent changes