Disjunction

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-02-08.
Last modified on 2024-04-11.

module foundation.disjunction where

open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.functoriality-coproduct-types
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions

Idea

The disjunction^¶ of two propositions P and Q is the proposition that P holds or Q holds, and is defined as propositional truncation of the coproduct of their underlying types

  P ∨ Q := ║ P + Q ║₋₁

The universal property^¶ of the disjunction states that, for every proposition R, the evaluation map

  ev : ((P ∨ Q) → R) → ((P → R) ∧ (Q → R))

is a logical equivalence, and thus the disjunction is the least upper bound of P and Q in the locale of propositions: there is a pair of logical implications P → R and Q → R, if and only if P ∨ Q implies R

P ---> P ∨ Q <--- Q
  \      ∶      /
    \    ∶    /
      ∨  ∨  ∨
         R.

Definitions

The disjunction of arbitrary types

Given arbitrary types A and B, the truncation

  ║ A + B ║₋₁

satisfies the universal property of

  ║ A ║₋₁ ∨ ║ B ║₋₁

and is thus equivalent to it. Therefore, we may reasonably call this construction the disjunction^¶ of types. It is important to keep in mind that this is not a generalization of the concept but rather a conflation, and should be read as the statement A or B is (merely) inhabited.

Because propositions are a special case of types, and Agda can generally infer types for us, we will continue to conflate the two in our formalizations for the benefit that we have to specify the propositions in our code less often. For instance, even though the introduction rules for disjunction are phrased in terms of disjunction of types, they equally apply to disjunction of propositions.

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

  disjunction-type-Prop : Prop (l1 ⊔ l2)
  disjunction-type-Prop = trunc-Prop (A + B)

  disjunction-type : UU (l1 ⊔ l2)
  disjunction-type = type-Prop disjunction-type-Prop

  is-prop-disjunction-type : is-prop disjunction-type
  is-prop-disjunction-type = is-prop-type-Prop disjunction-type-Prop

The disjunction

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  disjunction-Prop : Prop (l1 ⊔ l2)
  disjunction-Prop = disjunction-type-Prop (type-Prop P) (type-Prop Q)

  type-disjunction-Prop : UU (l1 ⊔ l2)
  type-disjunction-Prop = type-Prop disjunction-Prop

  abstract
    is-prop-disjunction-Prop : is-prop type-disjunction-Prop
    is-prop-disjunction-Prop = is-prop-type-Prop disjunction-Prop

  infixr  _∨_
  _∨_ : Prop (l1 ⊔ l2)
  _∨_ = disjunction-Prop

Notation. The symbol used for the disjunction _∨_ is the logical or ∨ (agda-input: \vee \or), and not the latin small letter v v.

The introduction rules for the disjunction

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  inl-disjunction : A → disjunction-type A B
  inl-disjunction = unit-trunc-Prop ∘ inl

  inr-disjunction : B → disjunction-type A B
  inr-disjunction = unit-trunc-Prop ∘ inr

Note. Even though the introduction rules are formalized in terms of disjunction of types, it equally applies to disjunction of propositions. This is because propositions are a special case of types. The benefit of this approach is that Agda can infer types for us, but not generally propositions.

The universal property of disjunctions

ev-disjunction :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} →
  (disjunction-type A B → C) → (A → C) × (B → C)
pr1 (ev-disjunction h) = h ∘ inl-disjunction
pr2 (ev-disjunction h) = h ∘ inr-disjunction

universal-property-disjunction-type :
  {l1 l2 l3 : Level} → UU l1 → UU l2 → Prop l3 → UUω
universal-property-disjunction-type A B S =
  {l : Level} (R : Prop l) →
  (type-Prop S → type-Prop R) ↔ ((A → type-Prop R) × (B → type-Prop R))

universal-property-disjunction-Prop :
  {l1 l2 l3 : Level} → Prop l1 → Prop l2 → Prop l3 → UUω
universal-property-disjunction-Prop P Q =
  universal-property-disjunction-type (type-Prop P) (type-Prop Q)

Properties

The disjunction satisfies the universal property of disjunctions

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  elim-disjunction' :
    {l : Level} (R : Prop l) →
    (A → type-Prop R) × (B → type-Prop R) →
    disjunction-type A B → type-Prop R
  elim-disjunction' R (f , g) =
    map-universal-property-trunc-Prop R (rec-coproduct f g)

  up-disjunction :
    universal-property-disjunction-type A B (disjunction-type-Prop A B)
  up-disjunction R = ev-disjunction , elim-disjunction' R

The elimination principle of disjunctions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : Prop l3)
  where

  elim-disjunction :
    (A → type-Prop R) → (B → type-Prop R) →
    disjunction-type A B → type-Prop R
  elim-disjunction f g = elim-disjunction' R (f , g)

Propositions that satisfy the universal property of a disjunction are equivalent to the disjunction

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (Q : Prop l3)
  (up-Q : universal-property-disjunction-type A B Q)
  where

  forward-implication-iff-universal-property-disjunction :
    disjunction-type A B → type-Prop Q
  forward-implication-iff-universal-property-disjunction =
    elim-disjunction Q
      ( pr1 (forward-implication (up-Q Q) id))
      ( pr2 (forward-implication (up-Q Q) id))

  backward-implication-iff-universal-property-disjunction :
    type-Prop Q → disjunction-type A B
  backward-implication-iff-universal-property-disjunction =
    backward-implication
      ( up-Q (disjunction-type-Prop A B))
      ( inl-disjunction , inr-disjunction)

  iff-universal-property-disjunction :
    disjunction-type A B ↔ type-Prop Q
  iff-universal-property-disjunction =
    ( forward-implication-iff-universal-property-disjunction ,
      backward-implication-iff-universal-property-disjunction)

The unit laws for the disjunction

module _
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  where

  map-left-unit-law-disjunction-is-empty-Prop :
    is-empty (type-Prop P) → type-disjunction-Prop P Q → type-Prop Q
  map-left-unit-law-disjunction-is-empty-Prop f =
    elim-disjunction Q (ex-falso ∘ f) id

  map-right-unit-law-disjunction-is-empty-Prop :
    is-empty (type-Prop Q) → type-disjunction-Prop P Q → type-Prop P
  map-right-unit-law-disjunction-is-empty-Prop f =
    elim-disjunction P id (ex-falso ∘ f)

The unit laws for the disjunction of types

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  map-left-unit-law-disjunction-is-empty-type :
    is-empty A → disjunction-type A B → is-inhabited B
  map-left-unit-law-disjunction-is-empty-type f =
    elim-disjunction (is-inhabited-Prop B) (ex-falso ∘ f) unit-trunc-Prop

  map-right-unit-law-disjunction-is-empty-type :
    is-empty B → disjunction-type A B → is-inhabited A
  map-right-unit-law-disjunction-is-empty-type f =
    elim-disjunction (is-inhabited-Prop A) unit-trunc-Prop (ex-falso ∘ f)

The disjunction of arbitrary types is the disjunction of inhabitedness propositions

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  universal-property-disjunction-trunc :
    universal-property-disjunction-type A B
      ( disjunction-Prop (trunc-Prop A) (trunc-Prop B))
  universal-property-disjunction-trunc R =
    ( λ f →
      ( f ∘ inl-disjunction ∘ unit-trunc-Prop ,
        f ∘ inr-disjunction ∘ unit-trunc-Prop)) ,
    ( λ (f , g) →
      rec-trunc-Prop R
        ( rec-coproduct (rec-trunc-Prop R f) (rec-trunc-Prop R g)))

  iff-compute-disjunction-trunc :
    disjunction-type A B ↔ type-disjunction-Prop (trunc-Prop A) (trunc-Prop B)
  iff-compute-disjunction-trunc =
    iff-universal-property-disjunction
      ( disjunction-Prop (trunc-Prop A) (trunc-Prop B))
      ( universal-property-disjunction-trunc)

The disjunction preserves decidability

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-decidable-disjunction :
    is-decidable A → is-decidable B → is-decidable (disjunction-type A B)
  is-decidable-disjunction is-decidable-A is-decidable-B =
    is-decidable-trunc-Prop-is-merely-decidable
      ( A + B)
      ( unit-trunc-Prop (is-decidable-coproduct is-decidable-A is-decidable-B))

module _
  {l1 l2 : Level} (P : Decidable-Prop l1) (Q : Decidable-Prop l2)
  where

  type-disjunction-Decidable-Prop : UU (l1 ⊔ l2)
  type-disjunction-Decidable-Prop =
    type-disjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)

  is-prop-disjunction-Decidable-Prop :
    is-prop type-disjunction-Decidable-Prop
  is-prop-disjunction-Decidable-Prop =
    is-prop-disjunction-Prop
      ( prop-Decidable-Prop P)
      ( prop-Decidable-Prop Q)

  disjunction-Decidable-Prop : Decidable-Prop (l1 ⊔ l2)
  disjunction-Decidable-Prop =
    ( type-disjunction-Decidable-Prop ,
      is-prop-disjunction-Decidable-Prop ,
      is-decidable-disjunction
        ( is-decidable-Decidable-Prop P)
        ( is-decidable-Decidable-Prop Q))

See also

• The indexed counterpart to disjunction is existential quantification.

Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

External links

• Logical disjunction at Mathswitch
• disjunction at $n$Lab
• Logical disjunction at Wikipedia

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2024-02-06. Fredrik Bakke. Rename (co)prod to (co)product (#1017).
• 2024-01-25. Fredrik Bakke. Basic properties of orthogonal maps (#979).
• 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).
• 2023-10-08. Egbert Rijke and Fredrik Bakke. Nontrivial groups, and a correction of a statement in torsion-free groups (#815).