Copartial elements

Content created by Egbert Rijke and Fredrik Bakke.

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

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

Recent changes