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


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
  \      ∶      /
    \    ∶    /
      ∨  ∨  ∨


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)

  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)

  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

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

  infixr 10 _∨_
  _∨_ : 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}

  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)


The disjunction satisfies the universal property of disjunctions

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

  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)

  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)

  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 =
      ( 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 ,

The unit laws for the disjunction

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

  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}

  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}

  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 =
      ( 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}

  is-decidable-disjunction :
    is-decidable A  is-decidable B  is-decidable (disjunction-type A B)
  is-decidable-disjunction is-decidable-A is-decidable-B =
      ( 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)

  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 =
      ( 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-Decidable-Prop P)
        ( is-decidable-Decidable-Prop Q))

See also

Table of files about propositional logic

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

Propositions (foundation-core)foundation-core.propositions
Propositions (foundation)foundation.propositions
Subterminal typesfoundation.subterminal-types
Subsingleton inductionfoundation.subsingleton-induction
Empty types (foundation-core)foundation-core.empty-types
Empty types (foundation)foundation.empty-types
Unit typefoundation.unit-type
Logical equivalencesfoundation.logical-equivalences
Propositional extensionalityfoundation.propositional-extensionality
Mere logical equivalencesfoundation.mere-logical-equivalences
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Double negationfoundation.double-negation
Propositional truncationsfoundation.propositional-truncations
Universal property of propositional truncationsfoundation.universal-property-propositional-truncation
The induction principle of propositional truncationsfoundation.induction-principle-propositional-truncation
Functoriality of propositional truncationsfoundation.functoriality-propositional-truncations
Propositional resizingfoundation.propositional-resizing
Impredicative encodings of the logical operationsfoundation.impredicative-encodings

Recent changes