# Exclusive sums

Content created by Egbert Rijke and Fredrik Bakke.

Created 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.

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