Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 5 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions src/foundation/complements-subtypes.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
```
26 changes: 26 additions & 0 deletions src/foundation/disjoint-subtypes.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Comment on lines +48 to +49
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be called is-disjoint-prop-decidable-subtype, correspondinly, disjoint-subtype-Prop should be called is-disjoint-prop-subtype, sorry that I didn't catch that last time

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
Expand All @@ -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)
```
62 changes: 62 additions & 0 deletions src/foundation/unions-subtypes.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Comment on lines +122 to +131
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This result should be derived from the corresponding result for disjunctions of propositions: if ¬ (A ∧ B) then A + B is a proposition and equivalent to A ∨ B

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does that exist anywhere? Is there a good name for that concept? I looked around and thought about it, but I don't even know what to call e.g. ¬ (A ∧ B). "Incompatible propositions"? "Contradictory"?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, good question. I'm not sure I know a name for this. We have exclusive sum and exclusive disjunction, which are about different kinds of disjunctions "without the intersection", but nothing about the negation of the conjunction specifically. We also have files on de Morgan's law, which is about how ¬ (A ∧ B) relates to (¬ A) ∨ (¬ B), but I can't recall seeing another name for it than "the negation of the conjunction".

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All in all, there are a few candidates for "incompatible" or "contradictory" or "mutually exclusive propositions" — I'm not sure what follows from what. What comes to mind is

  1. ¬ (A ∧ B)
  2. (¬ A) ∨ (¬ B)
  3. (A ⇒ ¬ B)
  4. (A ⇒ ¬ B) ∨ (B ⇒ ¬ A)
  5. (¬ A ⇒ B)
  6. (¬ A ⇒ B) ∨ (¬ B ⇒ A)

Maybe some of these are silly conditions, and maybe some of them are wrong. The point is there might be many nonequivalent conditions here, and that's worthwhile to keep in mind when we name one of them.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right. The reason I didn't write the generalization is because this specific form, at least, has a clear and unambiguous name: disjointness is unambiguously the right term for subtypes. I agree there's something more general to say, but in the absence of a clear name for the more general thing, I'm hesitant to just throw some name we may not like into this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could call them disjoint propositions since they are precisely disjoint subsets of the 1-element type? Otherwise, I suggest looking up some references.


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
```
35 changes: 35 additions & 0 deletions src/logic/complements-decidable-subtypes.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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))
```
Loading