-
Notifications
You must be signed in to change notification settings - Fork 82
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
base: master
Are you sure you want to change the base?
Changes from 5 commits
6758305
bd9a1b9
68bdd00
afe5116
2b4c943
4a55320
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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)) | ||
Comment on lines
+122
to
+131
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe 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
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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 | ||
``` |
There was a problem hiding this comment.
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 calledis-disjoint-prop-subtype
, sorry that I didn't catch that last time