Exclusive disjunctions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.
Last modified on 2024-04-11.

module foundation.exclusive-disjunction where

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  _⊻_
  _⊻_ : 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))

See also

• The indexed counterpart to exclusive disjunction is unique existence.

Table of files about propositional logic

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

External links

• Exclusive or at Mathswitch
• exclusive disjunction at $n$Lab
• Exclusive disjunction at Wikipedia

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2024-04-11. Fredrik Bakke. Strict symmetrizations of binary relations (#1025).
• 2024-02-06. Fredrik Bakke. Rename (co)prod to (co)product (#1017).
• 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).
• 2023-10-16. Fredrik Bakke. Compatibility patch for Agda 2.6.4 (#846).