Equivalence between a type and the coproduct of a decidable subtype and its complement #1376
Conversation
Co-authored-by: Fredrik Bakke <[email protected]>
| disjoint-decidable-subtype-Prop : Prop (l1 ⊔ l2 ⊔ l3) | ||
| disjoint-decidable-subtype-Prop = |
There was a problem hiding this comment.
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
| 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)) |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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"?
There was a problem hiding this comment.
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".
There was a problem hiding this comment.
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
¬ (A ∧ B)(¬ A) ∨ (¬ B)(A ⇒ ¬ B)(A ⇒ ¬ B) ∨ (B ⇒ ¬ A)(¬ A ⇒ B)(¬ 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.
There was a problem hiding this comment.
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.
We could call them disjoint propositions since they are precisely disjoint subsets of the 1-element type? Otherwise, I suggest looking up some references.
Co-authored-by: Fredrik Bakke <[email protected]>
|
I'm marking this PR as a draft since it does not typecheck. |
No description provided.