Additional variants on choice #1317
Conversation
|
I suppose I also ought to add dependent choice. |
There was a problem hiding this comment.
The omniscience principles in terms of booleans should still be included, but under a different name, i.e. bool-LLPO here. It is a useful fact that these are equivalent
There was a problem hiding this comment.
With all the usages, it seems to me like that implies we want a file somewhere that describes the relationship between decidable subtypes of N and boolean sequences, since that'll get reused for many of the variations on LPO. I'm not sure where that ought to go -- thoughts?
There was a problem hiding this comment.
Do you mean the equivalence bool ≃ Decidable-Prop l? That is formalized in foundation.decidable-propositions, although I agree a little more exposition could be nice.
|
Very nice pull request! Maybe it would be nice to have a table in |
Co-authored-by: Egbert Rijke <[email protected]>
…iscience-principles
Done. |
|
WLPO => LLPO turns out to have some other prerequisites -- unique choice, I think? I'll come back to it. |
| WLEM-LEM : LEM → WLEM | ||
| WLEM-LEM lem = level-WLEM-LEM lem | ||
| ``` | ||
|
|
There was a problem hiding this comment.
Could you also record that this is equivalent to De Morgan's law, please?
There was a problem hiding this comment.
Please add logic.de-morgans-law to this list
|
|
||
| ## Definition | ||
|
|
||
| ### Instances of choice |
There was a problem hiding this comment.
| ### Instances of choice | |
| ### Instances of countable choice |
| ## Statement | ||
|
|
||
| The | ||
| {{#concept "axiom of dependent choice" WD="axiom of dependent choice" WDID=Q3303153}} |
There was a problem hiding this comment.
| {{#concept "axiom of dependent choice" WD="axiom of dependent choice" WDID=Q3303153}} | |
| {{#concept "axiom of dependent choice" WD="axiom of dependent choice" WDID=Q3303153 Agda=axiom-of-dependent-choice}} |
| instance-dependent-choice A H R total-R | ||
|
|
||
| ADC : UUω | ||
| ADC = {l1 l2 : Level} → level-ADC l1 l2 |
There was a problem hiding this comment.
Following the naming of axiom-of-choice, this should be called axiom-of-dependent-choice.
| level-WCC : (l : Level) → UU (lsuc l) | ||
| level-WCC l = (F : ℕ → Set l) → instance-weak-countable-choice-Set F | ||
|
|
||
| WCC : UUω |
There was a problem hiding this comment.
axiom-of-weak-countable-choice
| ### The law of excluded middle implies weak countable choice | ||
|
|
||
| ```agda | ||
| wcc-lem : {l : Level} → LEM l → level-WCC l |
There was a problem hiding this comment.
While you're at it, could you refactor the definition of LEM such that we have level-LEM also?
|
This PR seems to be unfinished, so I'm converting it to a draft. |
Overhauling all the variations on choice and omniscience, notably including following up on a suggestion from @fredrik-bakke to rewrite the existing omniscience principles in terms of decidable types.
I haven't finished the entire set of implications -- I'm missing WLEM => WLPO and WLPO => LLPO -- but I'll follow up with those soon.