100 years of Zermelo's axiom of choice: What was the problem with it? (2006)

Summary

module mi.MartinLof2006 where open import Agda.Primitive using (Level ; _⊔_ ; lsuc) id : ∀ {𝓈} {S : Set 𝓈} → S → S id x = x infixr 9 _∘_ _∘_ : ∀ {𝓈 𝓉 𝓊} {S : Set 𝓈} {T : S → Set 𝓉} {U : ∀ {x} → T x → Set 𝓊} (f : ∀ {x} (y : T x) → U y) (g : ∀ x → T x) (x : S) → U (g x) (f ∘ g) x = f (g x) Relation : ∀ {𝓈} (S : Set 𝓈) ℓ → Set _ Relation S ℓ = S → S → Set ℓ Reflexive : ∀ {𝓈 ℓ} {S : Set 𝓈} (_∼_ : Relation S ℓ) → Set _ Reflexive _∼_ = ∀ {x} → x ∼ x Symmetric : ∀ {𝓈 ℓ} {S : Set 𝓈} (_∼_ : Relation S ℓ) → Set _ Symmetric _∼_ = ∀ {x y} → x ∼ y → y ∼ x Transitive : ∀ {𝓈 ℓ} {S : Set 𝓈} (_∼_ : Relation S ℓ) → Set _ Transitive _∼_ = ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z record Equivalence {𝓈} (S : Set 𝓈) ℯ : Set (𝓈 ⊔ lsuc ℯ) where field _≍_ : Relation S ℯ ≍-refl : Reflexive _≍_ ≍-sym : Symmetric _≍_ ≍-trans : Transitive _≍_ open Equivalence {{...}} open import Agda.Builtin.Equality using (refl) renaming (_≡_ to Id) sym : ∀ {𝓈} {S : Set 𝓈} → Symmetric {S = S} Id sym refl = refl trans : ∀ {𝓈} {S : Set 𝓈} → Transitive {S = S} Id trans refl h = h Id-≍ : ∀ {𝓈} {S : Set 𝓈} → Equivalence S _ Id-≍ = record { _≍_ = Id ; ≍-refl = refl ; ≍-sym = sym ; ≍-trans = trans } cong : ∀ {𝓈 𝓉} {S : Set 𝓈} {T : Set 𝓉} (f : S → T) {x y : S} → Id x y → Id (f x) (f y) cong f refl = refl Id→≍ : ∀ {𝓈 ℯ} {S : Set 𝓈} {x y : S} {{≍S : Equivalence S ℯ}} → Id x y → x ≍ y Id→≍ refl = ≍-refl open import Agda.Builtin.Sigma using (_,_ ; fst ; snd) renaming (Σ to ∃) infix 2 ∃-syntax syntax ∃-syntax S (λ x → T) = ∃[ x ⦂ S ] T ∃-syntax : ∀ {𝓈 𝓉} (S : Set 𝓈) (T : S → Set 𝓉) → Set _ ∃-syntax = ∃ infixr 2 _∧_ _∧_ : ∀ {𝓈 𝓉} (S : Set 𝓈) (T : Set 𝓉) → Set _ S ∧ T = ∃[ _ ⦂ S ] T infix 2 ∃!-syntax syntax ∃!-syntax S (λ x → T) = ∃![ x ⦂ S ] T ∃!-syntax : ∀ {𝓈 𝓉 ℯ} (S : Set 𝓈) (T : S → Set 𝓉) {{≍S : Equivalence S ℯ}} → Set _ ∃!-syntax S T = ∃[ x ⦂ S ] T x ∧ ∀ {y} → T y → x ≍ y infix 1 _↔_ _↔_ : ∀ {𝓈 𝓉} (S : Set 𝓈) (T : Set 𝓉) → Set _ S ↔ T = (S → T) ∧ (T → S) ↔-refl : ∀ {𝓈} → Reflexive {S = Set 𝓈} _↔_ ↔-refl = id , id ↔-sym : ∀ {𝓈...