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

@@ -58,12 +58,12 @@ instance-choice-Set :
   {l1 l2 : Level} (A : Set l1) → (type-Set A → Set l2) → UU (l1 ⊔ l2)
 instance-choice-Set A B = instance-choice (type-Set A) (type-Set ∘ B)
 
-level-AC-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-level-AC-Set l1 l2 =
+level-axiom-of-choice-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+level-axiom-of-choice-Set l1 l2 =
   (A : Set l1) (B : type-Set A → Set l2) → instance-choice-Set A B
 
-AC-Set : UUω
-AC-Set = {l1 l2 : Level} → level-AC-Set l1 l2
+axiom-of-choice-Set : UUω
+axiom-of-choice-Set = {l1 l2 : Level} → level-axiom-of-choice-Set l1 l2
 ```
 
 ### The axiom of choice
@@ -73,23 +73,23 @@ instance-choice₀ :
   {l1 l2 : Level} (A : Set l1) → (type-Set A → UU l2) → UU (l1 ⊔ l2)
 instance-choice₀ A = instance-choice (type-Set A)
 
-level-AC0 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-level-AC0 l1 l2 =
+level-axiom-of-choice : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+level-axiom-of-choice l1 l2 =
   (A : Set l1) (B : type-Set A → UU l2) → instance-choice₀ A B
 
-AC0 : UUω
-AC0 = {l1 l2 : Level} → level-AC0 l1 l2
+axiom-of-choice : UUω
+axiom-of-choice = {l1 l2 : Level} → level-axiom-of-choice l1 l2
 ```
 
 ## Properties
 
 ### Every type is set-projective if and only if the axiom of choice holds
 
 ```agda
-is-set-projective-AC0 :
-  {l1 l2 l3 : Level} → level-AC0 l2 (l1 ⊔ l2) →
+is-set-projective-axiom-of-choice :
+  {l1 l2 l3 : Level} → level-axiom-of-choice l2 (l1 ⊔ l2) →
   (X : UU l3) → is-set-projective l1 l2 X
-is-set-projective-AC0 ac X A B f h =
+is-set-projective-axiom-of-choice ac X A B f h =
   map-trunc-Prop
     ( ( map-Σ
         ( λ g → ((map-surjection f) ∘ g) ＝ h)
@@ -98,11 +98,11 @@ is-set-projective-AC0 ac X A B f h =
       ( section-is-split-surjective (map-surjection f)))
     ( ac B (fiber (map-surjection f)) (is-surjective-map-surjection f))
 
-AC0-is-set-projective :
+axiom-of-choice-is-set-projective :
   {l1 l2 : Level} →
   ({l : Level} (X : UU l) → is-set-projective (l1 ⊔ l2) l1 X) →
-  level-AC0 l1 l2
-AC0-is-set-projective H A B K =
+  level-axiom-of-choice l1 l2
+axiom-of-choice-is-set-projective H A B K =
   map-trunc-Prop
     ( map-equiv (equiv-Π-section-pr1 {B = B}) ∘ tot (λ g → htpy-eq))
     ( H ( type-Set A)
@@ -117,6 +117,10 @@ AC0-is-set-projective H A B K =
 - [Diaconescu's theorem](foundation.diaconescus-theorem.md), which states that
   the axiom of choice implies the law of excluded middle.
 
+## Table of choice principles
+
+{{#include tables/choice-principles.md}}
+
 ## References
 
 {{#bibliography}}

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

@@ -0,0 +1,74 @@
+# The axiom of countable choice
+
+```agda
+module foundation.axiom-of-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.axiom-of-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 the type `ℕ` of
+[natural numbers](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} → (ℕ → Set l) → UU l
+instance-countable-choice F =
+  ((n : ℕ) → is-inhabited (type-Set (F n))) →
+  is-inhabited ((n : ℕ) → type-Set (F n))
+```
+
+### The axiom of countable choice
+
+```agda
+level-countable-choice : (l : Level) → UU (lsuc l)
+level-countable-choice l = (F : ℕ → Set l) → instance-countable-choice F
+
+axiom-of-countable-choice : UUω
+axiom-of-countable-choice = {l : Level} → level-countable-choice l
+```
+
+## Properties
+
+### The axiom of choice for sets implies the axiom of countable choice
+
+```agda
+level-countable-choice-level-axiom-of-choice-Set :
+  {l : Level} → level-axiom-of-choice-Set lzero l → level-countable-choice l
+level-countable-choice-level-axiom-of-choice-Set ac-l = ac-l ℕ-Set
+
+countable-choice-axiom-of-choice-Set :
+  axiom-of-choice-Set → axiom-of-countable-choice
+countable-choice-axiom-of-choice-Set ac =
+  level-countable-choice-level-axiom-of-choice-Set ac
+```
+
+## Table of choice principles
+
+{{#include tables/choice-principles.md}}
+
+## 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,70 @@
+# 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
+```
+
+## Table of choice principles
+
+{{#include tables/choice-principles.md}}
+
+## External links
+
+- [Axiom of dependent choice](https://en.wikipedia.org/wiki/Axiom_of_dependent_choice)