Equivalence between a type and the coproduct of a decidable subtype and its complement

src/foundation/complements-subtypes.lagda.md

@@ -9,6 +9,8 @@ module foundation.complements-subtypes where
 ```agda
 open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
+open import foundation.dependent-pair-types
+open import foundation.disjoint-subtypes
 open import foundation.double-negation-stable-propositions
 open import foundation.full-subtypes
 open import foundation.negation
@@ -93,3 +95,12 @@ module _
     complement-subtype C ⊆ complement-subtype B
   reverses-order-complement-subtype B⊆C x x∉C x∈B = x∉C (B⊆C x x∈B)
 ```
+
+### A subtype and its complement are disjoint
+
+```agda
+disjoint-complement-subtype :
+  {l1 l2 : Level} {A : UU l1} →
+  (B : subtype l2 A) → disjoint-subtype B (complement-subtype B)
+disjoint-complement-subtype _ _ (bx , ¬bx) = ¬bx bx
+```

src/foundation/disjoint-subtypes.lagda.md

@@ -8,6 +8,7 @@ module foundation.disjoint-subtypes where
 
 ```agda
 open import foundation.cartesian-product-types
+open import foundation.decidable-subtypes
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.intersections-subtypes
@@ -38,6 +39,20 @@ module _
 
   disjoint-subtype : UU (l1 ⊔ l2 ⊔ l3)
   disjoint-subtype = type-Prop disjoint-subtype-Prop
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  (B : decidable-subtype l2 A) (C : decidable-subtype l3 A)
+  where
+
+  disjoint-decidable-subtype-Prop : Prop (l1 ⊔ l2 ⊔ l3)
+  disjoint-decidable-subtype-Prop =
+    disjoint-subtype-Prop
+      ( subtype-decidable-subtype B)
+      ( subtype-decidable-subtype C)
+
+  disjoint-decidable-subtype : UU (l1 ⊔ l2 ⊔ l3)
+  disjoint-decidable-subtype = type-Prop disjoint-decidable-subtype-Prop
 ```
 
 ## Properties
@@ -53,3 +68,14 @@ module _
     disjoint-subtype B B → is-empty (type-subtype B)
   is-empty-disjoint-subtype-self H (b , b∈B) = H b (b∈B , b∈B)
 ```
+
+### Disjointness is symmetric
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : subtype l2 A) (C : subtype l3 A)
+  where
+
+  symmetric-disjoint-subtype : disjoint-subtype B C → disjoint-subtype C B
+  symmetric-disjoint-subtype H x (cx , bx) = H x (bx , cx)
+```

src/foundation/unions-subtypes.lagda.md

@@ -7,12 +7,21 @@ module foundation.unions-subtypes where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
 open import foundation.decidable-subtypes
 open import foundation.dependent-pair-types
+open import foundation.disjoint-subtypes
 open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
 open import foundation.large-locale-of-subtypes
+open import foundation.logical-equivalences
 open import foundation.powersets
 open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.type-arithmetic-coproduct-types
 open import foundation.universe-levels
 
 open import foundation-core.subtypes
@@ -101,3 +110,56 @@ module _
       ( union-family-of-subtypes B x)
       ( λ (i , q) → unit-trunc-Prop (i , H i x q))
 ```
+
+### The union of disjoint subtypes is equivalent to their coproduct
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} (A : subtype l2 X) (B : subtype l3 X)
+  (H : disjoint-subtype A B)
+  where
+
+  all-elements-equal-coproduct-disjoint-prop :
+    (x : X) → all-elements-equal (type-Prop (A x) + type-Prop (B x))
+  all-elements-equal-coproduct-disjoint-prop x (inl _) (inl _) =
+    ap inl (eq-type-Prop (A x))
+  all-elements-equal-coproduct-disjoint-prop x (inr _) (inr _) =
+    ap inr (eq-type-Prop (B x))
+  all-elements-equal-coproduct-disjoint-prop x (inl ax) (inr bx) =
+    ex-falso (H x (ax , bx))
+  all-elements-equal-coproduct-disjoint-prop x (inr bx) (inl ax) =
+    ex-falso (H x (ax , bx))
+
+  is-prop-coproduct-disjoint-prop :
+    (x : X) → is-prop (type-Prop (A x) + type-Prop (B x))
+  is-prop-coproduct-disjoint-prop x =
+    is-prop-all-elements-equal (all-elements-equal-coproduct-disjoint-prop x)
+
+  subtype-coproduct-disjoint-subtype : subtype (l2 ⊔ l3) X
+  subtype-coproduct-disjoint-subtype x =
+    type-Prop (A x) + type-Prop (B x) , is-prop-coproduct-disjoint-prop x
+
+  iff-disjunction-coproduct-disjoint-subtype :
+    (x : X) → type-iff-Prop ((A x) ∨ (B x)) (subtype-coproduct-disjoint-subtype x)
+  pr1 (iff-disjunction-coproduct-disjoint-subtype x) =
+    elim-disjunction (subtype-coproduct-disjoint-subtype x) inl inr
+  pr2 (iff-disjunction-coproduct-disjoint-subtype x) =
+    rec-coproduct inl-disjunction inr-disjunction
+
+  equiv-union-subtype-coproduct-disjoint-subtype :
+    type-subtype (union-subtype A B) ≃
+    type-subtype subtype-coproduct-disjoint-subtype
+  equiv-union-subtype-coproduct-disjoint-subtype =
+    equiv-tot
+      ( λ x →
+        equiv-iff'
+          ( (A x) ∨ (B x))
+          ( subtype-coproduct-disjoint-subtype x)
+          ( iff-disjunction-coproduct-disjoint-subtype x))
+
+  equiv-union-coproduct-disjoint-subtype :
+    type-subtype (union-subtype A B) ≃ type-subtype A + type-subtype B
+  equiv-union-coproduct-disjoint-subtype =
+    left-distributive-Σ-coproduct X (is-in-subtype A) (is-in-subtype B) ∘e
+    equiv-union-subtype-coproduct-disjoint-subtype
+```

src/logic/complements-decidable-subtypes.lagda.md

@@ -13,7 +13,9 @@ open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.disjoint-subtypes
 open import foundation.double-negation-stable-propositions
+open import foundation.equivalences
 open import foundation.evaluation-functions
 open import foundation.full-subtypes
 open import foundation.involutions
@@ -51,6 +53,16 @@ complement-decidable-subtype P x = neg-Decidable-Prop (P x)
 
 ## Properties
 
+### The complement of a decidable subtype is disjoint from the subtype
+
+```agda
+disjoint-complement-decidable-subtype :
+  {l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A) →
+  disjoint-decidable-subtype P (complement-decidable-subtype P)
+disjoint-complement-decidable-subtype P =
+  disjoint-complement-subtype (subtype-decidable-subtype P)
+```
+
 ### Taking complements is an involution on decidable subtypes
 
 ```agda
@@ -98,3 +110,26 @@ module _
       ( subtype-decidable-subtype P)
       ( is-decidable-decidable-subtype P)
 ```
+
+### `A` is equivalent to the coproduct of a decidable subtype and its complement
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A)
+  where
+
+  equiv-coproduct-subtype-complement-decidable-subtype :
+    A ≃
+    type-decidable-subtype P +
+    type-decidable-subtype (complement-decidable-subtype P)
+  equiv-coproduct-subtype-complement-decidable-subtype =
+    equiv-union-coproduct-disjoint-subtype
+      ( subtype-decidable-subtype P)
+      ( subtype-decidable-subtype (complement-decidable-subtype P))
+      ( disjoint-complement-decidable-subtype P) ∘e
+    inv-equiv
+      ( equiv-inclusion-is-full-subtype
+        ( subtype-decidable-subtype
+          ( union-decidable-subtype P (complement-decidable-subtype P)))
+        ( is-full-union-subtype-complement-decidable-subtype P))
+```