From 675830533620b221a54ddcbdf7a1304615ffd579 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Sun, 23 Mar 2025 13:51:23 -0700
Subject: [PATCH 1/4] Progress

---
 src/foundation/complements-subtypes.lagda.md  | 11 ++++
 src/foundation/disjoint-subtypes.lagda.md     | 26 ++++++++
 src/foundation/unions-subtypes.lagda.md       | 61 +++++++++++++++++++
 .../complements-decidable-subtypes.lagda.md   | 35 +++++++++++
 4 files changed, 133 insertions(+)

diff --git a/src/foundation/complements-subtypes.lagda.md b/src/foundation/complements-subtypes.lagda.md
index 3331a3455c..dfcbe670c3 100644
--- a/src/foundation/complements-subtypes.lagda.md
+++ b/src/foundation/complements-subtypes.lagda.md
@@ -10,11 +10,13 @@ module foundation.complements-subtypes where
 open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
 open import foundation.double-negation-stable-propositions
+open import foundation.dependent-pair-types
 open import foundation.full-subtypes
 open import foundation.negation
 open import foundation.postcomposition-functions
 open import foundation.powersets
 open import foundation.propositional-truncations
+open import foundation.disjoint-subtypes
 open import foundation.unions-subtypes
 open import foundation.universe-levels
 
@@ -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
+```
diff --git a/src/foundation/disjoint-subtypes.lagda.md b/src/foundation/disjoint-subtypes.lagda.md
index e21739bbd5..9364b88519 100644
--- a/src/foundation/disjoint-subtypes.lagda.md
+++ b/src/foundation/disjoint-subtypes.lagda.md
@@ -14,6 +14,7 @@ open import foundation.intersections-subtypes
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
+open import foundation.decidable-subtypes
 ```
 
 </details>
@@ -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)
+```
diff --git a/src/foundation/unions-subtypes.lagda.md b/src/foundation/unions-subtypes.lagda.md
index a3ae84790a..12d65d7b7c 100644
--- a/src/foundation/unions-subtypes.lagda.md
+++ b/src/foundation/unions-subtypes.lagda.md
@@ -7,11 +7,20 @@ module foundation.unions-subtypes where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.equivalences
+open import foundation.empty-types
+open import foundation.coproduct-types
 open import foundation.decidable-subtypes
+open import foundation.type-arithmetic-coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
+open import foundation.disjoint-subtypes
+open import foundation.logical-equivalences
 open import foundation.large-locale-of-subtypes
+open import foundation.propositions
 open import foundation.powersets
+open import foundation.functoriality-dependent-pair-types
 open import foundation.propositional-truncations
 open import foundation.universe-levels
 
@@ -101,3 +110,55 @@ 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)
+
+  coproduct-disjoint-subtype : subtype (l2 ⊔ l3) X
+  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) (coproduct-disjoint-subtype x)
+  pr1 (iff-disjunction-coproduct-disjoint-subtype x) =
+    elim-disjunction (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 coproduct-disjoint-subtype
+  equiv-union-subtype-coproduct-disjoint-subtype =
+    equiv-tot
+      ( λ x →
+        equiv-iff'
+          ( A x ∨ B x)
+          ( 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
+```
diff --git a/src/logic/complements-decidable-subtypes.lagda.md b/src/logic/complements-decidable-subtypes.lagda.md
index ae2a775f33..29b4a182c2 100644
--- a/src/logic/complements-decidable-subtypes.lagda.md
+++ b/src/logic/complements-decidable-subtypes.lagda.md
@@ -11,12 +11,14 @@ open import foundation.complements-subtypes
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
+open import foundation.equivalences
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.double-negation-stable-propositions
 open import foundation.evaluation-functions
 open import foundation.full-subtypes
 open import foundation.involutions
+open import foundation.disjoint-subtypes
 open import foundation.negation
 open import foundation.postcomposition-functions
 open import foundation.powersets
@@ -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))
+```

From bd9a1b9622727601cad501283f6405244c20e370 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Sun, 23 Mar 2025 13:55:53 -0700
Subject: [PATCH 2/4] make pre-commit

---
 src/foundation/complements-subtypes.lagda.md  |  4 +--
 src/foundation/disjoint-subtypes.lagda.md     |  2 +-
 src/foundation/unions-subtypes.lagda.md       | 27 ++++++++++---------
 .../complements-decidable-subtypes.lagda.md   |  4 +--
 4 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/src/foundation/complements-subtypes.lagda.md b/src/foundation/complements-subtypes.lagda.md
index dfcbe670c3..11e12fc9a9 100644
--- a/src/foundation/complements-subtypes.lagda.md
+++ b/src/foundation/complements-subtypes.lagda.md
@@ -9,14 +9,14 @@ module foundation.complements-subtypes where
 ```agda
 open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
-open import foundation.double-negation-stable-propositions
 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
 open import foundation.postcomposition-functions
 open import foundation.powersets
 open import foundation.propositional-truncations
-open import foundation.disjoint-subtypes
 open import foundation.unions-subtypes
 open import foundation.universe-levels
 
diff --git a/src/foundation/disjoint-subtypes.lagda.md b/src/foundation/disjoint-subtypes.lagda.md
index 9364b88519..5b5df704da 100644
--- a/src/foundation/disjoint-subtypes.lagda.md
+++ b/src/foundation/disjoint-subtypes.lagda.md
@@ -8,13 +8,13 @@ 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
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
-open import foundation.decidable-subtypes
 ```
 
 </details>
diff --git a/src/foundation/unions-subtypes.lagda.md b/src/foundation/unions-subtypes.lagda.md
index 12d65d7b7c..dcce5de9a4 100644
--- a/src/foundation/unions-subtypes.lagda.md
+++ b/src/foundation/unions-subtypes.lagda.md
@@ -8,20 +8,20 @@ module foundation.unions-subtypes where
 
 ```agda
 open import foundation.action-on-identifications-functions
-open import foundation.equivalences
-open import foundation.empty-types
 open import foundation.coproduct-types
 open import foundation.decidable-subtypes
-open import foundation.type-arithmetic-coproduct-types
 open import foundation.dependent-pair-types
-open import foundation.disjunction
 open import foundation.disjoint-subtypes
-open import foundation.logical-equivalences
+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.propositions
+open import foundation.logical-equivalences
 open import foundation.powersets
-open import foundation.functoriality-dependent-pair-types
 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
@@ -135,25 +135,26 @@ module _
   is-prop-coproduct-disjoint-prop x =
     is-prop-all-elements-equal (all-elements-equal-coproduct-disjoint-prop x)
 
-  coproduct-disjoint-subtype : subtype (l2 ⊔ l3) X
-  coproduct-disjoint-subtype 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) (coproduct-disjoint-subtype x)
+    (x : X) → type-iff-Prop (A x ∨ B x) (subtype-coproduct-disjoint-subtype x)
   pr1 (iff-disjunction-coproduct-disjoint-subtype x) =
-    elim-disjunction (coproduct-disjoint-subtype x) inl inr
+    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 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)
-          ( coproduct-disjoint-subtype x)
+          ( subtype-coproduct-disjoint-subtype x)
           ( iff-disjunction-coproduct-disjoint-subtype x))
 
   equiv-union-coproduct-disjoint-subtype :
diff --git a/src/logic/complements-decidable-subtypes.lagda.md b/src/logic/complements-decidable-subtypes.lagda.md
index 29b4a182c2..ee474aa92e 100644
--- a/src/logic/complements-decidable-subtypes.lagda.md
+++ b/src/logic/complements-decidable-subtypes.lagda.md
@@ -11,14 +11,14 @@ open import foundation.complements-subtypes
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.decidable-subtypes
-open import foundation.equivalences
 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
-open import foundation.disjoint-subtypes
 open import foundation.negation
 open import foundation.postcomposition-functions
 open import foundation.powersets

From afe5116419eb62e5cbfe83e50df092fc04778973 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Mon, 24 Mar 2025 16:37:30 -0700
Subject: [PATCH 3/4] Apply suggestions from code review

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/unions-subtypes.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/foundation/unions-subtypes.lagda.md b/src/foundation/unions-subtypes.lagda.md
index dcce5de9a4..deb445f1c0 100644
--- a/src/foundation/unions-subtypes.lagda.md
+++ b/src/foundation/unions-subtypes.lagda.md
@@ -140,7 +140,7 @@ module _
     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)
+    (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) =
@@ -153,7 +153,7 @@ module _
     equiv-tot
       ( λ x →
         equiv-iff'
-          ( A x ∨ B x)
+          ( (A x) ∨ (B x))
           ( subtype-coproduct-disjoint-subtype x)
           ( iff-disjunction-coproduct-disjoint-subtype x))
 

From 4a5532076a3ea4a82705083cd7524fa1aa216770 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Thu, 27 Mar 2025 13:21:22 -0700
Subject: [PATCH 4/4] Apply suggestions from code review

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/disjoint-subtypes.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/disjoint-subtypes.lagda.md b/src/foundation/disjoint-subtypes.lagda.md
index 5b5df704da..a06fce3165 100644
--- a/src/foundation/disjoint-subtypes.lagda.md
+++ b/src/foundation/disjoint-subtypes.lagda.md
@@ -51,7 +51,7 @@ module _
       ( subtype-decidable-subtype B)
       ( subtype-decidable-subtype C)
 
-  disjoint-decidable-subtype : UU (l1 ⊔ l2 ⊔ l3)
+  is-disjoint-decidable-subtype : UU (l1 ⊔ l2 ⊔ l3)
   disjoint-decidable-subtype = type-Prop disjoint-decidable-subtype-Prop
 ```