# Copartial elements

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.

module foundation.copartial-elements where

Imports
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.negation
open import foundation.partial-elements
open import foundation.universe-levels

open import foundation-core.propositions

open import orthogonal-factorization-systems.closed-modalities

open import synthetic-homotopy-theory.joins-of-types


## Idea

A copartial element of a type A is an element of type

  Σ (Q : Prop), A * Q


where the type A * Q is the join of Q and A. We say that evaluation of a copartial element (Q , u) is denied if the proposition Q holds.

In order to compare copartial elements with partial elements, note that we have the following pullback squares

  A -----> Σ (Q : Prop), A * Q        1 -----> Σ (P : Prop), (P → A)
| ⌟              |                  | ⌟              |
|                |                  |                |
∨                ∨                  ∨                ∨
1 -----------> Prop                 1 -----------> Prop
F                                   F

1 -----> Σ (Q : Prop), A * Q        A -----> Σ (P : Prop), (P → A)
| ⌟              |                  | ⌟              |
|                |                  |                |
∨                ∨                  ∨                ∨
1 -----------> Prop                 1 -----------> Prop
T                                   T


Note that we make use of the closed modalities A ↦ A * Q in the formulation of copartial element, whereas the formulation of partial elements makes use of the open modalities. 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

    A   1
|   |
! | □ | T
∨   ∨
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

                                         P Q x ↦ (P * Q , x)
1     1       Σ (P Q : Prop), P * Q ---------------------> 1
|     |               |                                    |
T |  □  | T   =   T □ T |                                    |
∨     ∨               ∨                                    ∨
Prop   Prop           Prop² ------------------------------> Prop
P Q ↦ P * Q


By this morphism of arrows it follows that there is a morphism of arrows

  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.

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

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-denied-prop-copartial-element : Prop l2
is-denied-prop-copartial-element = pr1 a

is-denied-copartial-element : UU l2
is-denied-copartial-element =
type-Prop is-denied-prop-copartial-element

value-copartial-element :
operator-closed-modality is-denied-prop-copartial-element A
value-copartial-element = pr2 a


### The unit of the copartial element operator

module _
{l1 : Level} {A : UU l1} (a : A)
where

is-denied-prop-unit-copartial-element : Prop lzero
is-denied-prop-unit-copartial-element = empty-Prop

is-denied-unit-copartial-element : UU lzero
is-denied-unit-copartial-element = empty

unit-copartial-element : copartial-element lzero A
pr1 unit-copartial-element = is-denied-prop-unit-copartial-element
pr2 unit-copartial-element = unit-closed-modality empty-Prop a


## Properties

### Forgetful map from copartial elements to partial elements

module _
{l1 l2 : Level} {A : UU l1} (a : copartial-element l2 A)
where

is-defined-prop-partial-element-copartial-element : Prop l2
is-defined-prop-partial-element-copartial-element =
neg-Prop (is-denied-prop-copartial-element a)

is-defined-partial-element-copartial-element : UU l2
is-defined-partial-element-copartial-element =
type-Prop is-defined-prop-partial-element-copartial-element

value-partial-element-copartial-element :
is-defined-partial-element-copartial-element → A
value-partial-element-copartial-element f =
map-inv-right-unit-law-join-is-empty f (value-copartial-element a)

partial-element-copartial-element : partial-element l2 A
pr1 partial-element-copartial-element =
is-defined-prop-partial-element-copartial-element
pr2 partial-element-copartial-element =
value-partial-element-copartial-element