# Copartial functions

Content created by Egbert Rijke.

Created on 2023-12-07.

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)