# Disjunction

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

Created on 2022-02-08.

module foundation.disjunction where

Imports
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 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}
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))


## Table of files about propositional logic

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

ConceptFile
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
Conjunctionfoundation.conjunction
Disjunctionfoundation.disjunction
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Negationfoundation.negation
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