Home

選択公理

module foundations.axiom-of-choice where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.proposition
open import foundations.set
open import foundations.sigma-type
open import foundations.propositional-truncation

private variable
  ℓ ℓ′ ℓ″ : Level

module _
  (X : Type ℓ) (isSetX : isSet X)
  (A : X → Type ℓ′) (isSetA : ∀ x → isSet (A x))
  (P : (x : X) → A x → Type ℓ″) (isPropP : ∀ x a → isProp (P x a))
  (trunc : PropTrunc) where
  open PropTrunc trunc

  AC : Type (ℓ ⊔ ℓ′ ⊔ ℓ″)
  AC =
    ((x : X) → ∥ (Σ[ a ∈ A x ] P x a ) ∥)
    → ∥ (Σ[ f ∈ ((x : X) → A x) ] ((x : X) → P x (f x))) ∥

module _
  (X : Type ℓ) (isSetX : isSet X)
  (Y : X → Type ℓ′) (isSetY : ∀ x → isSet (Y x))
  (trunc : PropTrunc) where
  open PropTrunc trunc

  AC′ : Type (ℓ ⊔ ℓ′)
  AC′ = ((x : X) → ∥ Y x ∥) → ∥ ((x : X) → Y x) ∥

  globalChoice→AC′ : (∀ {ℓ} → {A : Type ℓ} → ∥ A ∥ → A) → AC′
  globalChoice→AC′ gc f = ∣ (λ x → gc (f x)) ∣