Exclusive disjunctions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.

module foundation.exclusive-disjunction where

Imports
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equality-coproduct-types
open import foundation.exclusive-sum
open import foundation.functoriality-coproduct-types
open import foundation.propositional-truncations
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.universal-property-coproduct-types
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions


Idea

The exclusive disjunction of two propositions P and Q is the proposition that precisely one of P and Q holds, and is defined as the proposition that the coproduct of their underlying types is contractible

  P ⊻ Q := is-contr (P + Q)


It necessarily follows that precisely one of the two propositions hold, and the other does not. This is captured by the exclusive sum.

Definitions

The exclusive disjunction of arbitrary types

The definition of exclusive sum is sometimes generalized to arbitrary types, which we record here for completeness.

The exclusive disjunction of the types A and B is the proposition that their coproduct is contractible

  A ⊻ B := is-contr (A + B).


Note that unlike the case for disjunction and existential quantification, but analogous to the case of uniqueness quantification, the exclusive disjunction of types does not coincide with the exclusive disjunction of the summands' propositional reflections:

  A ⊻ B ≠ ║ A ║₋₁ ⊻ ║ B ║₋₁.

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

xor-type-Prop : Prop (l1 ⊔ l2)
xor-type-Prop = is-contr-Prop (A + B)

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

is-prop-xor-type : is-prop xor-type
is-prop-xor-type = is-prop-type-Prop xor-type-Prop


The exclusive disjunction

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

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

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

is-prop-xor-Prop : is-prop type-xor-Prop
is-prop-xor-Prop = is-prop-type-Prop xor-Prop

infixr 10 _⊻_
_⊻_ : Prop (l1 ⊔ l2)
_⊻_ = xor-Prop


Notation. The symbol used for exclusive disjunction ⊻ can be written with the escape sequence \veebar.

Properties

The canonical map from the exclusive disjunction into the exclusive sum

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

map-exclusive-sum-xor : xor-type A B → exclusive-sum A B
map-exclusive-sum-xor (inl a , H) =
inl (a , (λ b → is-empty-eq-coproduct-inl-inr a b (H (inr b))))
map-exclusive-sum-xor (inr b , H) =
inr (b , (λ a → is-empty-eq-coproduct-inr-inl b a (H (inl a))))


The exclusive disjunction of two propositions is equivalent to their exclusive sum

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

equiv-exclusive-sum-xor-Prop : type-xor-Prop P Q ≃ type-exclusive-sum-Prop P Q
equiv-exclusive-sum-xor-Prop =
( equiv-coproduct
( equiv-tot
( λ p →
( ( equiv-Π-equiv-family (compute-eq-coproduct-inl-inr p)) ∘e
( left-unit-law-product-is-contr
( is-contr-Π
( λ p' →
is-contr-equiv'
( p ＝ p')
( equiv-ap-emb (emb-inl (type-Prop P) (type-Prop Q)))
( is-prop-type-Prop P p p'))))) ∘e
( equiv-dependent-universal-property-coproduct (inl p ＝_))))
( equiv-tot
( λ q →
( ( equiv-Π-equiv-family (compute-eq-coproduct-inr-inl q)) ∘e
( right-unit-law-product-is-contr
( is-contr-Π
( λ q' →
is-contr-equiv'
( q ＝ q')
( equiv-ap-emb (emb-inr (type-Prop P) (type-Prop Q)))
( is-prop-type-Prop Q q q'))))) ∘e
( equiv-dependent-universal-property-coproduct (inr q ＝_))))) ∘e
( right-distributive-Σ-coproduct
( type-Prop P)
( type-Prop Q)
( λ x → (y : type-Prop P + type-Prop Q) → x ＝ y))


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