Additional variants on choice

references.bib

@@ -928,3 +928,15 @@ @article{BauerTaylor2009
   doi = {10.1017/S0960129509007695},
   url = {PaulTaylor.EU/ASD/dedras/},
   amsclass = {03F60, 06E15, 18C20, 26E40, 54D45, 65G40}}
+
+@article{Bridges2000,
+  author = {Bridges, Douglas and Richman, Fred and Schuster, Peter},
+  title = {A Weak Countable Choice Principle},
+  journal = {Proceedings of the American Mathematical Society},
+  publisher = {American Mathematical Society},
+  year = 2000,
+  volume = 128,
+  pages = {2749--2752},
+  doi = {10.1090/S0002-9939-00-05327-2},
+  url = {https://www.ams.org/journals/proc/2000-128-09/S0002-9939-00-05327-2/}
+}

src/foundation.lagda.md

@@ -29,6 +29,9 @@ open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
 open import foundation.arithmetic-law-product-and-pi-decompositions public
 open import foundation.automorphisms public
 open import foundation.axiom-of-choice public
+open import foundation.axiom-of-countable-choice public
+open import foundation.axiom-of-dependent-choice public
+open import foundation.axiom-of-weak-countable-choice public
 open import foundation.bands public
 open import foundation.base-changes-span-diagrams public
 open import foundation.bicomposition-functions public
@@ -493,6 +496,7 @@ open import foundation.unordered-tuples-of-types public
 open import foundation.vectors-set-quotients public
 open import foundation.vertical-composition-spans-of-spans public
 open import foundation.weak-function-extensionality public
+open import foundation.weak-law-of-excluded-middle public
 open import foundation.weak-limited-principle-of-omniscience public
 open import foundation.weakly-constant-maps public
 open import foundation.whiskering-higher-homotopies-composition public

src/foundation/axiom-of-choice.lagda.md

@@ -7,6 +7,10 @@ module foundation.axiom-of-choice where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.equality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.axiom-of-countable-choice
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.functoriality-propositional-truncation
@@ -112,6 +116,16 @@ AC0-is-set-projective H A B K =
         ( id))
 ```
 
+### The axiom of choice for sets implies the axiom of countable choice
+
+```agda
+level-ACω-AC-Set : {l : Level} → level-AC-Set lzero l → level-ACω l
+level-ACω-AC-Set ac-l = ac-l ℕ-Set
+
+ACω-AC-Set : AC-Set → ACω
+ACω-AC-Set ac = level-ACω-AC-Set ac
+```
+
 ## See also
 
 - [Diaconescu's theorem](foundation.diaconescus-theorem.md), which states that

src/foundation/axiom-of-countable-choice.lagda.md

@@ -0,0 +1,82 @@
+# The axiom of countable choice
+
+```agda
+module foundation.axiom-of-countable-choice where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.axiom-of-weak-countable-choice
+open import foundation.function-types
+open import foundation.inhabited-types
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "axiom of countable choice" WD="axiom of countable choice" WDID=Q1000116 Agda=ACω}}
+asserts that for every family of [inhabited](foundation.inhabited-types.md)
+types `F` indexed by [`ℕ`](elementary-number-theory.natural-numbers.md), the
+type of sections of that family `(n : ℕ) → B n` is inhabited.
+
+## Definition
+
+### Instances of choice
+
+```agda
+instance-countable-choice : {l : Level} → (ℕ → UU l) → UU l
+instance-countable-choice F =
+  ((n : ℕ) → is-inhabited (F n)) → is-inhabited ((n : ℕ) → F n)
+```
+
+### The axiom of countable choice
+
+```agda
+instance-countable-choice-Set :
+  {l : Level} → (ℕ → Set l) → UU l
+instance-countable-choice-Set F =
+  instance-countable-choice (type-Set ∘ F)
+
+level-ACω : (l : Level) → UU (lsuc l)
+level-ACω l = (F : ℕ → Set l) → instance-countable-choice-Set F
+
+ACω : UUω
+ACω = {l : Level} → level-ACω l
+```
+
+## Properties
+
+### The axiom of countable choice implies the axiom of weak countable choice
+
+```agda
+instance-weak-countable-choice-instance-countable-choice :
+  {l : Level} → (F : ℕ → UU l) →
+  instance-countable-choice F → instance-weak-countable-choice F
+instance-weak-countable-choice-instance-countable-choice F cc inhab-F _ =
+  cc inhab-F
+
+instance-weak-countable-choice-instance-countable-choice-Set :
+  {l : Level} → (F : ℕ → Set l) →
+  instance-countable-choice-Set F → instance-weak-countable-choice-Set F
+instance-weak-countable-choice-instance-countable-choice-Set F =
+  instance-weak-countable-choice-instance-countable-choice (type-Set ∘ F)
+
+level-WCC-level-ACω : {l : Level} → level-ACω l → level-WCC l
+level-WCC-level-ACω acω-l F =
+  instance-weak-countable-choice-instance-countable-choice-Set F (acω-l F)
+
+WCC-ACω : ACω → WCC
+WCC-ACω acω = level-WCC-level-ACω acω
+```
+
+## External links
+
+- [Axiom of countable choice](https://ncatlab.org/nlab/show/countable+choice) at
+  nLab

src/foundation/axiom-of-dependent-choice.lagda.md

@@ -0,0 +1,66 @@
+# The axiom of dependent choice
+
+```agda
+module foundation.axiom-of-dependent-choice where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-relations
+open import foundation.existential-quantification
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Statement
+
+The
+{{#concept "axiom of dependent choice" WD="axiom of dependent choice" WDID=Q3303153}}
+asserts that for every [inhabited](foundation.inhabited-types.md)
+[set](foundation.sets.md) `A` and
+[binary relation](foundation.binary-relations.md) `R` on `A`, such that for
+every `a : A`, `∃ A (λ b → R a b)`, there is a sequence `f : ℕ → A` with
+`R (f n) (f (succ-ℕ n))` for every `n`.
+
+### Instances of dependent choice
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Set l1) (H : is-inhabited (type-Set A))
+  (R : Relation-Prop l2 (type-Set A))
+  (total-R : (a : type-Set A) → exists (type-Set A) (R a))
+  where
+
+  instance-dependent-choice-Prop : Prop (l1 ⊔ l2)
+  instance-dependent-choice-Prop =
+    ∃ (ℕ → type-Set A) (λ f → Π-Prop ℕ (λ n → R (f n) (f (succ-ℕ n))))
+
+  instance-dependent-choice : UU (l1 ⊔ l2)
+  instance-dependent-choice = type-Prop instance-dependent-choice-Prop
+```
+
+### The axiom of dependent choice
+
+```agda
+level-ADC : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2))
+level-ADC l1 l2 =
+  (A : Set l1) (H : is-inhabited (type-Set A)) →
+  (R : Relation-Prop l2 (type-Set A))
+  (total-R : (a : type-Set A) → exists (type-Set A) (R a)) →
+  instance-dependent-choice A H R total-R
+
+ADC : UUω
+ADC = {l1 l2 : Level} → level-ADC l1 l2
+```
+
+## External links
+
+- [Axiom of dependent choice](https://en.wikipedia.org/wiki/Axiom_of_dependent_choice)

src/foundation/axiom-of-weak-countable-choice.lagda.md

@@ -0,0 +1,119 @@
+# The axiom of weak countable choice
+
+```agda
+module foundation.axiom-of-weak-countable-choice where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.equality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.law-of-excluded-middle
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The {{#concept "axiom of weak countable choice" Agda=WCC}} asserts that for
+every family of [inhabited](foundation.inhabited-types.md) types `F` indexed by
+[`ℕ`](elementary-number-theory.natural-numbers.md), where for at most one `n`,
+`F n` is not [contractible](foundation.contractible-types.md), the type of
+sections of that family `(n : ℕ) → B n` is inhabited. This axiom was introduced
+in {{#cite Bridges2000}}.
+
+## Definitions
+
+### Instances of weak countable choice
+
+```agda
+instance-weak-countable-choice : {l : Level} → (ℕ → UU l) → UU l
+instance-weak-countable-choice F =
+  ( (n : ℕ) → is-inhabited (F n)) →
+  ( (m n : ℕ) →
+    m ≠ n →
+    type-Prop (is-contr-Prop (F m) ∨ is-contr-Prop (F n))) →
+  is-inhabited ((n : ℕ) → F n)
+```
+
+### The axiom of weak countable choice
+
+```agda
+instance-weak-countable-choice-Set :
+  {l : Level} → (ℕ → Set l) → UU l
+instance-weak-countable-choice-Set F =
+  instance-weak-countable-choice (type-Set ∘ F)
+
+level-WCC : (l : Level) → UU (lsuc l)
+level-WCC l = (F : ℕ → Set l) → instance-weak-countable-choice-Set F
+
+WCC : UUω
+WCC = {l : Level} → level-WCC l
+```
+
+## Properties
+
+### The law of excluded middle implies weak countable choice
+
+```agda
+wcc-lem : {l : Level} → LEM l → level-WCC l
+wcc-lem {l} lem F inhab-F contr-le
+  with lem (∃ ℕ (λ n → ¬' (is-contr-Prop (type-Set (F n)))))
+... | inr none-non-contractible =
+  unit-trunc-Prop
+    ( λ n →
+      rec-coproduct
+        ( center)
+        ( ex-falso ∘ none-non-contractible ∘ intro-exists n)
+        ( lem (is-contr-Prop (type-Set (F n)))))
+... | inl one-not-contractible =
+  elim-exists
+    ( claim)
+    ( λ n not-contractible-Fn →
+      rec-trunc-Prop
+        ( claim)
+        ( λ elem-Fn →
+          unit-trunc-Prop
+            ( λ m →
+              rec-coproduct
+                ( λ m=n → tr (type-Set ∘ F) (inv m=n) elem-Fn)
+                ( λ m≠n →
+                  center
+                    ( map-right-unit-law-disjunction-is-empty-Prop
+                      ( is-contr-Prop (type-Set (F m)))
+                      ( is-contr-Prop (type-Set (F n)))
+                      ( not-contractible-Fn)
+                      ( contr-le m n m≠n)))
+                ( has-decidable-equality-ℕ m n)))
+        ( inhab-F n))
+    ( one-not-contractible)
+    where
+    claim : Prop l
+    claim = is-inhabited-Prop ((n : ℕ) → type-Set (F n))
+```
+
+## External links
+
+- [Weak countable choice](https://ncatlab.org/nlab/show/countable+choice#WCC) at
+  nLab
+
+## References
+
+{{#bibliography}}

src/foundation/law-of-excluded-middle.lagda.md

@@ -7,14 +7,13 @@ module foundation.law-of-excluded-middle where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.negation
+open import foundation.propositions
 open import foundation.universe-levels
 
-open import foundation-core.decidable-propositions
-open import foundation-core.negation
-open import foundation-core.propositions
-
 open import univalent-combinatorics.2-element-types
 ```
 
@@ -58,3 +57,7 @@ abstract
   no-global-decidability {l} d =
     is-not-decidable-type-2-Element-Type (λ X → d (pr1 X))
 ```
+
+## External links
+
+- [Excluded middle](https://ncatlab.org/nlab/show/excluded+middle) at nLab