# Copartial elements

```agda
module foundation.copartial-elements where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## 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
evaluation of a copartial element `(Q , u)` is
{{#concept "denied" Disambiguation="copartial element" Agda=is-denied-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](foundation.pullbacks.md) squares

```text
  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](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
    ∨   ∨
    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 |                                    |
    ∨     ∨               ∨                                    ∨
  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-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

```agda
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

```agda
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
```