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


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.


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)

  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)

  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.


The canonical map from the exclusive disjunction into the exclusive sum

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

  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)

  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' 
                    ( 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' 
                    ( 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

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