The axiom of dependent choice

Content created by Louis Wasserman.

Created on 2025-08-01.
Last modified on 2025-08-01.

module foundation.axiom-of-dependent-choice where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.axiom-of-choice
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.inhabited-types
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.universe-levels

Idea

The axiom of dependent choice asserts that for every entire binary relation R on an inhabited type A, there exists f : ℕ → A such that for all n : ℕ , R (f n) (f (succ-ℕ n)).

Definition

module _
  {l1 : Level} (A : Set l1) (inhabited-A : is-inhabited (type-Set A))
  {l2 : Level} (R : Relation l2 (type-Set A))
  (H : is-entire-Relation R)
  where

  instance-ADC : UU (l1 ⊔ l2)
  instance-ADC =
    is-inhabited (Σ (ℕ → type-Set A) (λ f → (n : ℕ) → R (f n) (f (succ-ℕ n))))

level-ADC : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
level-ADC l1 l2 =
  (A : Set l1) (inhabited-A : is-inhabited (type-Set A)) →
  (R : Relation l2 (type-Set A)) (H : is-entire-Relation R) →
  instance-ADC A inhabited-A R H

ADC : UUω
ADC = {l1 l2 : Level} → level-ADC l1 l2

Properties

The axiom of choice implies the axiom of dependent choice

level-ADC-level-AC0 : {l1 l2 : Level} → level-AC0 l1 (l1 ⊔ l2) → level-ADC l1 l2
level-ADC-level-AC0 ac0 A inhabited-A R entire-R =
  let
    open
      do-syntax-trunc-Prop
        ( is-inhabited-Prop
          ( Σ (ℕ → type-Set A) (λ f → (n : ℕ) → R (f n) (f (succ-ℕ n)))))
  in do
    f ← ac0 A (λ a → Σ (type-Set A) (R a)) entire-R
    a₀ ← inhabited-A
    let g = ind-ℕ a₀ (λ _ → pr1 ∘ f)
    unit-trunc-Prop (g , pr2 ∘ f ∘ g)

ADC-AC0 : AC0 → ADC
ADC-AC0 ac0 = level-ADC-level-AC0 ac0

See also

Recent changes