Symmetric difference of subtypes

module foundation.symmetric-difference where
Imports
open import foundation.decidable-subtypes
open import foundation.decidable-types
open import foundation.exclusive-disjunction
open import foundation.identity-types hiding (inv)
open import foundation.intersections-subtypes

open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.propositions
open import foundation-core.subtypes
open import foundation-core.universe-levels

Idea

The symmetric difference of two subtypes A and B is the subtypes that contains the elements that are either in A or in B but not in both.

Definition

module _
  {l l1 l2 : Level} {X : UU l}
  where

  symmetric-difference-subtype :
    subtype l1 X  subtype l2 X  subtype (l1  l2) X
  symmetric-difference-subtype P Q x = xor-Prop (P x) (Q x)

  symmetric-difference-decidable-subtype :
    decidable-subtype l1 X  decidable-subtype l2 X 
    decidable-subtype (l1  l2) X
  symmetric-difference-decidable-subtype P Q x = xor-Decidable-Prop (P x) (Q x)

Properties

The coproduct of two decidable subtypes is equivalent to their symmetric difference plus two times their intersection

module _
  {l l1 l2 : Level} {X : UU l}
  where

  left-cases-equiv-symmetric-difference :
    (P : decidable-subtype l1 X) (Q : decidable-subtype l2 X) 
    (x : X)  type-Decidable-Prop (P x) 
    is-decidable (type-Decidable-Prop (Q x)) 
    ( type-decidable-subtype
      ( symmetric-difference-decidable-subtype P Q)) +
    ( ( type-decidable-subtype (intersection-decidable-subtype P Q)) +
      ( type-decidable-subtype (intersection-decidable-subtype P Q)))
  left-cases-equiv-symmetric-difference P Q x p (inl q) =
    inr (inl (pair x (pair p q)))
  left-cases-equiv-symmetric-difference P Q x p (inr nq) =
    inl (pair x (inl (pair p nq)))

  right-cases-equiv-symmetric-difference :
    ( P : decidable-subtype l1 X) (Q : decidable-subtype l2 X) 
    (x : X)  type-Decidable-Prop (Q x) 
    is-decidable (type-Decidable-Prop (P x)) 
    ( type-decidable-subtype
      ( symmetric-difference-decidable-subtype P Q)) +
    ( ( type-decidable-subtype (intersection-decidable-subtype P Q)) +
      ( type-decidable-subtype (intersection-decidable-subtype P Q)))
  right-cases-equiv-symmetric-difference P Q x q (inl p) =
    inr (inr (pair x (pair p q)))
  right-cases-equiv-symmetric-difference P Q x q (inr np) =
    inl (pair x (inr (pair q np)))

  equiv-symmetric-difference :
    (P : decidable-subtype l1 X) (Q : decidable-subtype l2 X) 
    ( (type-decidable-subtype P + type-decidable-subtype Q) 
      ( ( type-decidable-subtype (symmetric-difference-decidable-subtype P Q)) +
        ( ( type-decidable-subtype (intersection-decidable-subtype P Q)) +
          ( type-decidable-subtype (intersection-decidable-subtype P Q)))))
  pr1 (equiv-symmetric-difference P Q) (inl (pair x p)) =
    left-cases-equiv-symmetric-difference P Q x p
      ( is-decidable-Decidable-Prop (Q x))
  pr1 (equiv-symmetric-difference P Q) (inr (pair x q)) =
    right-cases-equiv-symmetric-difference P Q x q
      ( is-decidable-Decidable-Prop (P x))
  pr2 (equiv-symmetric-difference P Q) =
    is-equiv-has-inverse inv retr sec
    where
    inv :
      ( type-decidable-subtype (symmetric-difference-decidable-subtype P Q)) +
      ( ( type-decidable-subtype (intersection-decidable-subtype P Q)) +
        ( type-decidable-subtype (intersection-decidable-subtype P Q))) 
      type-decidable-subtype P + type-decidable-subtype Q
    inv (inl (pair x (inl (pair p nq)))) = inl (pair x p)
    inv (inl (pair x (inr (pair q np)))) = inr (pair x q)
    inv (inr (inl (pair x (pair p q)))) = inl (pair x p)
    inv (inr (inr (pair x (pair p q)))) = inr (pair x q)
    retr :
      (C :
        ( type-decidable-subtype (symmetric-difference-decidable-subtype P Q)) +
        ( ( type-decidable-subtype (intersection-decidable-subtype P Q)) +
          ( type-decidable-subtype (intersection-decidable-subtype P Q)))) 
      ((pr1 (equiv-symmetric-difference P Q))  inv) C  C
    retr (inl (pair x (inl (pair p nq)))) =
      tr
        ( λ q' 
          ( left-cases-equiv-symmetric-difference P Q x p q') 
          ( inl (pair x (inl (pair p nq)))))
        ( eq-is-prop (is-prop-is-decidable (is-prop-type-Decidable-Prop (Q x))))
        ( refl)
    retr (inl (pair x (inr (pair q np)))) =
      tr
        ( λ p' 
          ( right-cases-equiv-symmetric-difference P Q x q p') 
          ( inl (pair x (inr (pair q np)))))
        ( eq-is-prop (is-prop-is-decidable (is-prop-type-Decidable-Prop (P x))))
        ( refl)
    retr (inr (inl (pair x (pair p q)))) =
      tr
        ( λ q' 
          (left-cases-equiv-symmetric-difference P Q x p q') 
          (inr (inl (pair x (pair p q)))))
        ( eq-is-prop (is-prop-is-decidable (is-prop-type-Decidable-Prop (Q x))))
        ( refl)
    retr (inr (inr (pair x (pair p q)))) =
      tr
        ( λ p' 
          (right-cases-equiv-symmetric-difference P Q x q p') 
          (inr (inr (pair x (pair p q)))))
        ( eq-is-prop (is-prop-is-decidable (is-prop-type-Decidable-Prop (P x))))
        ( refl)
    left-cases-sec :
      (x : X)
      (p : type-Decidable-Prop (P x))
      (q : is-decidable (type-Decidable-Prop (Q x))) 
      inv (left-cases-equiv-symmetric-difference P Q x p q)  inl (pair x p)
    left-cases-sec x p (inl q) = refl
    left-cases-sec x p (inr nq) = refl
    right-cases-sec :
      (x : X)
      (q : type-Decidable-Prop (Q x))
      (p : is-decidable (type-Decidable-Prop (P x))) 
      inv (right-cases-equiv-symmetric-difference P Q x q p)  inr (pair x q)
    right-cases-sec x q (inl p) = refl
    right-cases-sec x q (inr np) = refl
    sec :
      (C : type-decidable-subtype P + type-decidable-subtype Q) 
      (inv  pr1 (equiv-symmetric-difference P Q)) C  C
    sec (inl (pair x p)) =
      left-cases-sec x p (is-decidable-Decidable-Prop (Q x))
    sec (inr (pair x q)) =
      right-cases-sec x q (is-decidable-Decidable-Prop (P x))