Exclusive sums

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.exclusive-sum where

Imports

open import foundation.conjunction
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.symmetric-operations
open import foundation.universal-quantification
open import foundation.universe-levels
open import foundation.unordered-pairs

open import foundation-core.cartesian-product-types
open import foundation-core.decidable-propositions
open import foundation-core.embeddings
open import foundation-core.empty-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.transport-along-identifications

open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

The exclusive sum^¶ of two types A and B, is the type consisting of

elements of A together with a proof that B is empty, or
elements of B together with a proof that A is empty.

The exclusive sum^¶ of propositions P and Q is likewise the proposition that P holds and Q does not hold, or P does not hold and Q holds. The exclusive sum of two propositions is equivalent to the exclusive disjunction, which is shown there.

Definitions

The exclusive sum of types

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

  exclusive-sum : UU (l1 ⊔ l2)
  exclusive-sum = (A × ¬ B) + (B × ¬ A)

The exclusive sum of propositions

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

  exclusive-sum-Prop : Prop (l1 ⊔ l2)
  exclusive-sum-Prop =
    coproduct-Prop
      ( P ∧ (¬' Q))
      ( Q ∧ (¬' P))
      ( λ p q → pr2 q (pr1 p))

  type-exclusive-sum-Prop : UU (l1 ⊔ l2)
  type-exclusive-sum-Prop = type-Prop exclusive-sum-Prop

  abstract
    is-prop-type-exclusive-sum-Prop : is-prop type-exclusive-sum-Prop
    is-prop-type-exclusive-sum-Prop = is-prop-type-Prop exclusive-sum-Prop

The canonical inclusion of the exclusive sum into the coproduct

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

  map-coproduct-exclusive-sum : exclusive-sum A B → A + B
  map-coproduct-exclusive-sum (inl (a , _)) = inl a
  map-coproduct-exclusive-sum (inr (b , _)) = inr b

The symmetric operation of exclusive sum

predicate-symmetric-exclusive-sum :
  {l : Level} (p : unordered-pair (UU l)) → type-unordered-pair p → UU l
predicate-symmetric-exclusive-sum p x =
  ( element-unordered-pair p x) × (¬ (other-element-unordered-pair p x))

symmetric-exclusive-sum : {l : Level} → symmetric-operation (UU l) (UU l)
symmetric-exclusive-sum p =
  Σ (type-unordered-pair p) (predicate-symmetric-exclusive-sum p)

The symmetric operation of the exclusive sum of propositions

predicate-symmetric-exclusive-sum-Prop :
  {l : Level} (p : unordered-pair (Prop l)) →
  type-unordered-pair p → UU l
predicate-symmetric-exclusive-sum-Prop p =
  predicate-symmetric-exclusive-sum (map-unordered-pair type-Prop p)

type-symmetric-exclusive-sum-Prop :
  {l : Level} → symmetric-operation (Prop l) (UU l)
type-symmetric-exclusive-sum-Prop p =
  symmetric-exclusive-sum (map-unordered-pair type-Prop p)

all-elements-equal-type-symmetric-exclusive-sum-Prop :
  {l : Level} (p : unordered-pair (Prop l)) →
  all-elements-equal (type-symmetric-exclusive-sum-Prop p)
all-elements-equal-type-symmetric-exclusive-sum-Prop (X , P) x y =
  cases-is-prop-type-symmetric-exclusive-sum-Prop
    ( has-decidable-equality-is-finite
      ( is-finite-type-UU-Fin 2 X)
      ( pr1 x)
      ( pr1 y))
  where
  cases-is-prop-type-symmetric-exclusive-sum-Prop :
    is-decidable (pr1 x ＝ pr1 y) → x ＝ y
  cases-is-prop-type-symmetric-exclusive-sum-Prop (inl p) =
    eq-pair-Σ
      ( p)
      ( eq-is-prop
        ( is-prop-product-Prop
          ( P (pr1 y))
          ( neg-type-Prop
            ( other-element-unordered-pair
              ( map-unordered-pair (type-Prop) (X , P))
              ( pr1 y)))))
  cases-is-prop-type-symmetric-exclusive-sum-Prop (inr np) =
    ex-falso
      ( tr
        ( λ z → ¬ (type-Prop (P z)))
        ( compute-swap-2-Element-Type X (pr1 x) (pr1 y) np)
        ( pr2 (pr2 x))
        ( pr1 (pr2 y)))

is-prop-type-symmetric-exclusive-sum-Prop :
  {l : Level} (p : unordered-pair (Prop l)) →
  is-prop (type-symmetric-exclusive-sum-Prop p)
is-prop-type-symmetric-exclusive-sum-Prop p =
  is-prop-all-elements-equal
    ( all-elements-equal-type-symmetric-exclusive-sum-Prop p)

symmetric-exclusive-sum-Prop :
  {l : Level} → symmetric-operation (Prop l) (Prop l)
pr1 (symmetric-exclusive-sum-Prop E) = type-symmetric-exclusive-sum-Prop E
pr2 (symmetric-exclusive-sum-Prop E) =
  is-prop-type-symmetric-exclusive-sum-Prop E

Properties

The symmetric exclusive sum at a standard unordered pair

module _
  {l : Level} {A B : UU l}
  where

  exclusive-sum-symmetric-exclusive-sum :
    symmetric-exclusive-sum (standard-unordered-pair A B) → exclusive-sum A B
  exclusive-sum-symmetric-exclusive-sum (pair (inl (inr _)) (p , nq)) =
    inl
      ( pair p
        ( tr
          ( λ t → ¬ (element-unordered-pair (standard-unordered-pair A B) t))
          ( compute-swap-Fin-two-ℕ (zero-Fin 1))
          ( nq)))
  exclusive-sum-symmetric-exclusive-sum (pair (inr _) (q , np)) =
    inr
      ( pair
        ( q)
        ( tr
          ( λ t → ¬ (element-unordered-pair (standard-unordered-pair A B) t))
          ( compute-swap-Fin-two-ℕ (one-Fin 1))
          ( np)))

  symmetric-exclusive-sum-exclusive-sum :
    exclusive-sum A B → symmetric-exclusive-sum (standard-unordered-pair A B)
  pr1 (symmetric-exclusive-sum-exclusive-sum (inl (a , nb))) = (zero-Fin 1)
  pr1 (pr2 (symmetric-exclusive-sum-exclusive-sum (inl (a , nb)))) = a
  pr2 (pr2 (symmetric-exclusive-sum-exclusive-sum (inl (a , nb)))) =
    tr
      ( λ t → ¬ (element-unordered-pair (standard-unordered-pair A B) t))
      ( inv (compute-swap-Fin-two-ℕ (zero-Fin 1)))
      ( nb)
  pr1 (symmetric-exclusive-sum-exclusive-sum (inr (na , b))) = (one-Fin 1)
  pr1 (pr2 (symmetric-exclusive-sum-exclusive-sum (inr (b , na)))) = b
  pr2 (pr2 (symmetric-exclusive-sum-exclusive-sum (inr (b , na)))) =
    tr
      ( λ t → ¬ (element-unordered-pair (standard-unordered-pair A B) t))
      ( inv (compute-swap-Fin-two-ℕ (one-Fin 1)))
      ( na)

  eq-equiv-Prop
    ( ( ( equiv-coproduct
          ( ( ( left-unit-law-coproduct (type-Prop (P ∧ (¬' Q)))) ∘e
              ( equiv-coproduct
                ( left-absorption-Σ
                  ( λ x →
                    ( type-Prop
                      ( pr2 (standard-unordered-pair P Q) (inl (inl x)))) ×
                      ( ¬ ( type-Prop
                            ( pr2
                              ( standard-unordered-pair P Q)
                              ( map-swap-2-Element-Type
                                ( pr1 (standard-unordered-pair P Q))
                                ( inl (inl x))))))))
                ( ( equiv-product
                    ( id-equiv)
                    ( tr
                      ( λ b →
                        ( ¬ (type-Prop (pr2 (standard-unordered-pair P Q) b))) ≃
                        ( ¬ (type-Prop Q)))
                      ( inv (compute-swap-Fin-two-ℕ (zero-Fin ?)))
                      ( id-equiv))) ∘e
                    ( left-unit-law-Σ
                      ( λ y →
                        ( type-Prop
                          ( pr2 (standard-unordered-pair P Q) (inl (inr y)))) ×
                        ( ¬ ( type-Prop
                              ( pr2
                                ( standard-unordered-pair P Q)
                                ( map-swap-2-Element-Type
                                  ( pr1 (standard-unordered-pair P Q))
                                  ( inl (inr y))))))))))) ∘e
          ( ( right-distributive-Σ-coproduct
              ( Fin 0)
              ( unit)
              ( λ x →
                ( type-Prop (pr2 (standard-unordered-pair P Q) (inl x))) ×
                ( ¬ ( type-Prop
                      ( pr2
                        ( standard-unordered-pair P Q)
                        ( map-swap-2-Element-Type
                          ( pr1 (standard-unordered-pair P Q)) (inl x)))))))))
        ( ( equiv-product
            ( tr
              ( λ b →
                ¬ (type-Prop (pr2 (standard-unordered-pair P Q) b)) ≃
                ¬ (type-Prop P))
              ( inv (compute-swap-Fin-two-ℕ (one-Fin ?)))
              ( id-equiv))
            ( id-equiv)) ∘e
          ( ( commutative-product) ∘e
            ( left-unit-law-Σ
              ( λ y →
                ( type-Prop (pr2 (standard-unordered-pair P Q) (inr y))) ×
                ( ¬ ( type-Prop
                      ( pr2
                        ( standard-unordered-pair P Q)
                        ( map-swap-2-Element-Type
                          ( pr1 (standard-unordered-pair P Q))
                          ( inr y)))))))))) ∘e
      ( right-distributive-Σ-coproduct
        ( Fin 1)
        ( unit)
        ( λ x →
          ( type-Prop (pr2 (standard-unordered-pair P Q) x)) ×
          ( ¬ ( type-Prop
                ( pr2
                  ( standard-unordered-pair P Q)
                  ( map-swap-2-Element-Type
                    ( pr1 (standard-unordered-pair P Q))
                    ( x)))))))))

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

  exclusive-sum-symmetric-exclusive-sum-Prop :
    type-hom-Prop
      ( symmetric-exclusive-sum-Prop (standard-unordered-pair P Q))
      ( exclusive-sum-Prop P Q)
  exclusive-sum-symmetric-exclusive-sum-Prop (pair (inl (inr _)) (p , nq)) =
    inl
      ( pair p
        ( tr
          ( λ t →
            ¬ ( type-Prop
                ( element-unordered-pair (standard-unordered-pair P Q) t)))
          ( compute-swap-Fin-two-ℕ (zero-Fin 1))
          ( nq)))
  exclusive-sum-symmetric-exclusive-sum-Prop (pair (inr _) (q , np)) =
    inr
      ( pair q
        ( tr
          ( λ t →
            ¬ ( type-Prop
                ( element-unordered-pair (standard-unordered-pair P Q) t)))
          ( compute-swap-Fin-two-ℕ (one-Fin 1))
          ( np)))

  symmetric-exclusive-sum-exclusive-sum-Prop :
    type-hom-Prop
      ( exclusive-sum-Prop P Q)
      ( symmetric-exclusive-sum-Prop (standard-unordered-pair P Q))
  pr1 (symmetric-exclusive-sum-exclusive-sum-Prop (inl (p , nq))) = zero-Fin 1
  pr1 (pr2 (symmetric-exclusive-sum-exclusive-sum-Prop (inl (p , nq)))) = p
  pr2 (pr2 (symmetric-exclusive-sum-exclusive-sum-Prop (inl (p , nq)))) =
    tr
      ( λ t →
        ¬ (type-Prop (element-unordered-pair (standard-unordered-pair P Q) t)))
      ( inv (compute-swap-Fin-two-ℕ (zero-Fin 1)))
      ( nq)
  pr1 (symmetric-exclusive-sum-exclusive-sum-Prop (inr (q , np))) = one-Fin 1
  pr1 (pr2 (symmetric-exclusive-sum-exclusive-sum-Prop (inr (q , np)))) = q
  pr2 (pr2 (symmetric-exclusive-sum-exclusive-sum-Prop (inr (q , np)))) =
    tr
      ( λ t →
        ¬ (type-Prop (element-unordered-pair (standard-unordered-pair P Q) t)))
      ( inv (compute-swap-Fin-two-ℕ (one-Fin 1)))
      ( np)

eq-commmutative-exclusive-sum-exclusive-sum :
  {l : Level} (P Q : Prop l) →
  symmetric-exclusive-sum-Prop (standard-unordered-pair P Q) ＝
  exclusive-sum-Prop P Q
eq-commmutative-exclusive-sum-exclusive-sum P Q =
  eq-iff
    ( exclusive-sum-symmetric-exclusive-sum-Prop P Q)
    ( symmetric-exclusive-sum-exclusive-sum-Prop P Q)

The exclusive sum of decidable types is decidable

is-decidable-exclusive-sum :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → is-decidable B → is-decidable (exclusive-sum A B)
is-decidable-exclusive-sum d e =
  is-decidable-coproduct
    ( is-decidable-product d (is-decidable-neg e))
    ( is-decidable-product e (is-decidable-neg d))

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

  is-decidable-exclusive-sum-Decidable-Prop :
    is-decidable
      ( type-exclusive-sum-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q))
  is-decidable-exclusive-sum-Decidable-Prop =
      is-decidable-coproduct
      ( is-decidable-product
        ( is-decidable-Decidable-Prop P)
        ( is-decidable-neg (is-decidable-Decidable-Prop Q)))
      ( is-decidable-product
        ( is-decidable-Decidable-Prop Q)
        ( is-decidable-neg (is-decidable-Decidable-Prop P)))

  exclusive-sum-Decidable-Prop : Decidable-Prop (l1 ⊔ l2)
  pr1 exclusive-sum-Decidable-Prop =
    type-exclusive-sum-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)
  pr1 (pr2 exclusive-sum-Decidable-Prop) =
    is-prop-type-exclusive-sum-Prop
      ( prop-Decidable-Prop P)
      ( prop-Decidable-Prop Q)
  pr2 (pr2 exclusive-sum-Decidable-Prop) =
    is-decidable-exclusive-sum-Decidable-Prop

Table of files about propositional logic

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

Concept	File
Propositions (foundation-core)	`foundation-core.propositions`
Propositions (foundation)	`foundation.propositions`
Subterminal types	`foundation.subterminal-types`
Subsingleton induction	`foundation.subsingleton-induction`
Empty types (foundation-core)	`foundation-core.empty-types`
Empty types (foundation)	`foundation.empty-types`
Unit type	`foundation.unit-type`
Logical equivalences	`foundation.logical-equivalences`
Propositional extensionality	`foundation.propositional-extensionality`
Mere logical equivalences	`foundation.mere-logical-equivalences`
Conjunction	`foundation.conjunction`
Disjunction	`foundation.disjunction`
Exclusive disjunction	`foundation.exclusive-disjunction`
Existential quantification	`foundation.existential-quantification`
Uniqueness quantification	`foundation.uniqueness-quantification`
Universal quantification	`foundation.universal-quantification`
Negation	`foundation.negation`
Double negation	`foundation.double-negation`
Propositional truncations	`foundation.propositional-truncations`
Universal property of propositional truncations	`foundation.universal-property-propositional-truncation`
The induction principle of propositional truncations	`foundation.induction-principle-propositional-truncation`
Functoriality of propositional truncations	`foundation.functoriality-propositional-truncations`
Propositional resizing	`foundation.propositional-resizing`
Impredicative encodings of the logical operations	`foundation.impredicative-encodings`

Recent changes

2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).