A setoid satisfies choice if, and only if its equivalence relation is equality.

Epimorphism.agda

open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)

module Epimorphism where

  -- We characterize epimorphisms in setoids as precisely the surjective setoid maps

  -- Setoid preliminaries

  _%[_≈_] : ∀ {c ℓ} (B : Setoid c ℓ) (x y : Setoid.Carrier B) → Set ℓ
  _%[_≈_] = Setoid._≈_

  -- The setoid of propositions

  𝒫 : ∀ c → Setoid (suc c) c
  𝒫 c =
    record { Carrier = Set c
           ; _≈_ = λ P Q → (P → Q) × (Q → P)
           ; isEquivalence = record { refl = (λ x → x) , λ y → y
                                    ; sym = λ { (f , g) → g , f}
                                    ; trans = λ { (f , g) (u , v) → (λ x → u (f x)) , (λ y → g (v y))}
                                    }
           }

  -- Some observations about the setoid of setoids which we do not need

  SetoidLift : ∀ {c ℓ} c' ℓ' → Setoid c ℓ → Setoid (c ⊔ c') (ℓ ⊔ ℓ')
  SetoidLift c' ℓ' A
    =
    let record { Carrier = T ; _≈_ = _≈_ ; isEquivalence = record { refl = ρ ; sym = σ ; trans = τ }} = A in
    record { Carrier = Lift c' T
           ; _≈_ = λ { (lift x) (lift y) → Lift ℓ' (x ≈ y)}
           ; isEquivalence = record { refl = lift ρ
                                    ; sym = λ { {lift x} {lift y} (lift ξ) → lift (Setoid.sym A ξ)}
                                    ; trans = λ { {lift x} {lift y} {lift z} (lift ζ) (lift ξ) → lift (Setoid.trans A ζ ξ) }
                                    }
           }

  -- Isomorphism of setoids

  infix 3 _≅_

  record _≅_ {c₁ ℓ₁ c₂ ℓ₂} (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      iso : A ⟶ B
      inv : B ⟶ A
      iso-inv : ∀ y → Setoid._≈_ B (iso ⟨$⟩ (inv ⟨$⟩ y)) y
      inv-iso : ∀ x → Setoid._≈_ A (inv ⟨$⟩ (iso ⟨$⟩ x)) x

  ≅-Lift : ∀ {c ℓ c' ℓ'} {A : Setoid c ℓ} → A ≅ SetoidLift c' ℓ' A
  ≅-Lift {c} {ℓ} {c'} {ℓ'} {A} =
    record { iso = record { _⟨$⟩_ = lift ; cong = lift }
           ; inv = record { _⟨$⟩_ = lower ; cong = lower }
           ; iso-inv = λ _ → Setoid.refl (SetoidLift c' ℓ' A)
           ; inv-iso = λ _ → Setoid.refl A
           }

  open _≅_

  ≅-refl : ∀ {c ℓ} {A : Setoid c ℓ} → A ≅ A
  ≅-refl {A = A} =
    record { iso = id
           ; inv = id
           ; iso-inv = λ _ → Setoid.refl A
           ; inv-iso = λ _ → Setoid.refl A
           }

  ≅-sym : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ≅ B → B ≅ A
  ≅-sym ξ =
    record { iso = inv ξ
           ; inv = iso ξ
           ; iso-inv = inv-iso ξ
           ; inv-iso = iso-inv ξ
           }

  ≅-trans : ∀ {c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} {C : Setoid c₃ ℓ₃} →
              A ≅ B → B ≅ C → A ≅ C
  ≅-trans {A = A} {C = C} ζ ξ =
    record { iso = iso ξ ∘ iso ζ
           ; inv = inv ζ ∘ inv ξ
           ; iso-inv = λ _ → Setoid.trans C (cong (iso ξ) (iso-inv ζ _)) (iso-inv ξ _)
           ; inv-iso = λ x → Setoid.trans A (cong (inv ζ) (inv-iso ξ _)) (inv-iso ζ x)
           }

  cong-SetoidLift : ∀ {c ℓ c' ℓ'} {A B : Setoid c ℓ} → A ≅ B → SetoidLift c' ℓ' A ≅ SetoidLift c' ℓ' B
  cong-SetoidLift {c} {ℓ} {c'} {ℓ'} {A} {B} ξ = ≅-trans (≅-sym ≅-Lift) (≅-trans ξ ≅-Lift)

  -- The setoid of setoids

  𝒮 : ∀ (c ℓ : Level) → Setoid (suc c ⊔ suc ℓ) (c ⊔ ℓ)
  𝒮 c ℓ =
    record
      { Carrier = Setoid c ℓ
      ; _≈_ = _≅_
      ; isEquivalence = record { refl = ≅-refl ; sym = ≅-sym ; trans = ≅-trans }
      }

  -- Subsetoid (aplogies for silly notation but { and | are taken)

  𝕊 : ∀ {c ℓ k} (A : Setoid c ℓ) → (Setoid.Carrier A → Set k) → Setoid (c ⊔ k) ℓ
  𝕊 A P =
    record { Carrier = Σ _ P
           ; _≈_ = λ u v → A %[ fst u ≈ fst v ]
           ; isEquivalence =
                record { refl = λ {x} → Setoid.refl A
                       ; sym = Setoid.sym A
                       ; trans = Setoid.trans A } }

  𝕊-≅ : ∀ {c ℓ k₁ k₂} {A : Setoid c ℓ} {P : Setoid.Carrier A → Set k₁} {Q : Setoid.Carrier A → Set k₂} →
          (∀ {a} → P a → Q a) → (∀ {a} → Q a → P a) → 𝕊 A P ≅ 𝕊 A Q
  𝕊-≅ {A = A} f g =
    record { iso = record { _⟨$⟩_ = λ { (a , p) → a , f p} ; cong = λ ξ → ξ }
           ; inv = record { _⟨$⟩_ = λ { (a , q) → a , g q} ; cong = λ ξ → ξ }
           ; iso-inv = λ _ → Setoid.refl A
           ; inv-iso = λ _ → Setoid.refl A
           }

  surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂)
  surjective {B = B} f = ∀ y → Σ _ (λ x → B %[ f ⟨$⟩ x ≈ y ])

  epi : ∀ {c₁ ℓ₁ c₂ ℓ₂} c ℓ {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂ ⊔ suc c ⊔ suc ℓ)
  epi c ℓ {A = A} {B = B} f = ∀ (C : Setoid c ℓ) (g h : B ⟶ C) →
                                (∀ a → C %[  g ⟨$⟩ (f ⟨$⟩ a) ≈  h ⟨$⟩ (f ⟨$⟩ a) ]) → ∀ b → C %[ g ⟨$⟩ b ≈ h ⟨$⟩ b ]

  surjective⇒epi : ∀ {c₁ ℓ₁ c₂ ℓ₂ c ℓ} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (f : A ⟶ B) → surjective f → epi c ℓ f
  surjective⇒epi {B = B} f σ C g h ξ b =
     Setoid.trans C
       (Setoid.trans C
          (cong g (Setoid.sym B (snd (σ b)))) (ξ (fst (σ b))))
       (cong h (snd (σ b)))

  epi⇒surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (f : A ⟶ B) →
                     epi (suc (c₁ ⊔ ℓ₂)) (c₁ ⊔ ℓ₂) f → surjective f
  epi⇒surjective {c₁ = c₁} {ℓ₁ = ℓ₁} {c₂ = c₂} {ℓ₂ = ℓ₂} {A = A} {B = B} f ε b =
    fst aζ ,  Setoid.sym B (snd aζ)
    where
      g : B ⟶ 𝒫 (c₁ ⊔ ℓ₂)
      g = record { _⟨$⟩_ = λ b' → Lift c₁ (B %[ b ≈ b' ])
                 ; cong = λ ξ → (λ { (lift ζ) → lift (Setoid.trans B ζ ξ)}) , λ { (lift ζ) → lift (Setoid.trans B ζ (Setoid.sym B ξ)) }
                 }

      h : B ⟶ 𝒫 (c₁ ⊔ ℓ₂)
      h = record { _⟨$⟩_ = λ b' → (B %[ b ≈ b' ]) × Σ (Setoid.Carrier A) λ a → B %[ b' ≈ f ⟨$⟩ a ]
                 ; cong = λ ξ → (λ { (ζ , (a , θ)) → Setoid.trans B ζ ξ , a , (Setoid.trans B (Setoid.sym B ξ) θ)}) ,
                                 λ { (ζ , (a , θ)) → (Setoid.trans B ζ (Setoid.sym B ξ)) , (a , (Setoid.trans B ξ θ)) }
                 }

      gf≈hf : ∀ a → 𝒫 (c₁ ⊔ ℓ₂) %[ g ⟨$⟩ (f ⟨$⟩ a) ≈ h ⟨$⟩ (f ⟨$⟩ a) ]
      gf≈hf a = (λ { (lift ξ) → ξ , (a , (cong f (Setoid.refl A)))}) ,
                λ { (ξ , _) → lift ξ}

      g≈h : ∀ b → 𝒫 (c₁ ⊔ ℓ₂) %[ g ⟨$⟩ b ≈ h ⟨$⟩ b ]
      g≈h b = ε _ g h gf≈hf b

      aζ = snd (fst (g≈h b) (lift (Setoid.refl B)))

SetoidChoice.agda

-- Characterizations of setoids that satisfy the axiom of choice.
--
-- We define four properties of a setoid A:
--
-- (1) A satisfies the axiom of choice
-- (2) A is projective
-- (3) A is isomorphic to a type
-- (4) A has canonical elements
--
-- We show that (1) ⇔ (2)
--
-- We show that (2) ⇒ (3) when the carrier of A is an h-set.
-- We show that (3) ⇒ (4) ⇒ (1).
--
-- As a corrolary we conclude that the setoid of natural numbers satisfies choice.
-- (This is known as countable choice.)
--
-- Author: Andrej Bauer
-- January 6, 2022

open import Level
open import Relation.Binary
open import Data.Product
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)

module SetoidChoice where

  -- ===== Preliminaries =====

  -- A lemma about equality in dependent sums, is this in the standard library?

  Σ-≡ : ∀ {k ℓ} {A : Set k} {B : A → Set ℓ} {x y : A} {u : B x} {v : B y}
          (ξ : x ≡ y) → subst B ξ u ≡ v → (x , u) ≡ (y , v)
  Σ-≡ ≡-refl ≡-refl = ≡-refl

  -- the definition of h-sets

  is-set : ∀ {ℓ} → Set ℓ → Set ℓ
  is-set A = ∀ {x y : A} {p q : x ≡ y} → p ≡ q

  -- I could not find the definition of isomorphic setoids, so here it is

  record _≅_ {c₁ ℓ₁ c₂ ℓ₂} (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      iso : A ⟶ B
      inv : B ⟶ A
      iso-inv : ∀ y → Setoid._≈_ B (iso ⟨$⟩ (inv ⟨$⟩ y)) y
      inv-iso : ∀ x → Setoid._≈_ A (inv ⟨$⟩ (iso ⟨$⟩ x)) x

  ≅-refl : ∀ {c ℓ} {A : Setoid c ℓ} → A ≅ A
  ≅-refl {A = A} =
    record { iso = id
           ; inv = id
           ; iso-inv = λ _ → Setoid.refl A
           ; inv-iso = λ _ → Setoid.refl A }

  -- The definition of surjective setoid morphism

  surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂)
  surjective {B = B} f = ∀ y → Σ _ (λ x → Setoid._≈_ B (f ⟨$⟩ x) y)

  -- The definition of a split setoid morphism

  split : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂)
  split {A = A} {B = B} f = Σ (B ⟶ A) (λ g → ∀ y → Setoid._≈_ B (f ⟨$⟩ (g ⟨$⟩ y)) y)

  -- A binary relation on setoids A and B is a relation which respects equivalence
  -- (does this exist in the standard library).

  record SetoidRelation {c₁ ℓ₁ c₂ ℓ₂} k (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂ ⊔ suc k) where
    field
      rel : Setoid.Carrier A → Setoid.Carrier B → Set k
      rel-resp : ∀ {x₁ x₂ y₁ y₂} → Setoid._≈_ A x₁ x₂ → Setoid._≈_ B y₁ y₂ → rel x₁ y₁ → rel x₂ y₂


  module _ {c ℓ} (A : Setoid c ℓ) where
    open Setoid A
    open SetoidRelation

    -- ===== Notions of “A satisfies choice” =====

    -- A satisfies choice if every total relation has a choice morphism

    satisfies-choice : ∀ c' ℓ' r → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ' ⊔ suc r)
    satisfies-choice c' ℓ' r = ∀ (B : Setoid c' ℓ') (R : SetoidRelation r A B) →
                                 (∀ x → Σ (Setoid.Carrier B) (rel R x)) → Σ (A ⟶ B) (λ f → ∀ x → rel R x (f ⟨$⟩ x))

    -- A is projective if every surjection onto A is split

    projective : ∀ c' ℓ' → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ')
    projective c' ℓ' = ∀ (B : Setoid c' ℓ') (f : B ⟶ A) → surjective f → split f

    -- A has “canonical elements” if a function chooses (canonical) represenative from each equivalence class

    record canonical-elements : Set (c ⊔ ℓ) where
      field
        canon : Carrier → Carrier
        canon-≈ : ∀ x → canon x ≈ x
        canon-≡ : ∀ x y → x ≈ y → canon x ≡ canon y

    -- A is type-like if it is isomorhic to a setoid whose equivalence is propositional equality _≡_

    record type-like t : Set (suc c ⊔ ℓ ⊔ suc t) where
      field
        type-like-to : Set t
        type-like-≅ : A ≅ setoid type-like-to

    -- ===== Theorems ====

    -- A is projective iff it satisfies choice

    satisfies-choice⇒projective : ∀ c' ℓ' → satisfies-choice c' ℓ' ℓ -> projective c' ℓ'
    satisfies-choice⇒projective c' ℓ' ac B f s = ac _ R s
      where
        R : SetoidRelation ℓ A B
        R = record { rel = λ x y → f ⟨$⟩ y ≈ x
                   ; rel-resp = λ ζ ξ θ → trans (trans (cong f (Setoid.sym B ξ)) θ) ζ }

    projective⇒satisfies-choice : ∀ c' ℓ' → projective (c ⊔ ℓ ⊔ c') (ℓ ⊔ ℓ') → satisfies-choice c' ℓ' ℓ
    projective⇒satisfies-choice c' ℓ' p B R r =
                                u , λ x → rel-resp R (snd uθ x) (Setoid.refl B) (snd (snd (fst uθ ⟨$⟩ x)))
        where
        C = record { Carrier = Σ Carrier (λ x → Σ _ (rel R x))
                       ; _≈_ = λ u v → (fst u ≈ fst v) × Setoid._≈_ B (fst (snd u)) (fst (snd v))
                       ; isEquivalence =
                           record { refl = refl , (Setoid.refl B)
                                  ; sym = λ { (ζ , ξ) → sym ζ , Setoid.sym B ξ}
                                  ; trans = λ { (ζ₁ , ζ₂) (ξ₁ , ξ₂) → (trans ζ₁ ξ₁) , (Setoid.trans B ζ₂ ξ₂)}
                                  }
                   }

        uθ = p C
               (record { _⟨$⟩_ = fst ; cong = λ { (ζ , _) → ζ }})
               λ x → (x , r x) , refl

        u : A ⟶ B
        u = record { _⟨$⟩_ = λ x → fst (snd (fst uθ ⟨$⟩ x))
                   ; cong = λ ξ → snd (cong (fst uθ) ξ)
                   }

    -- If A is projective then it is type-like.
    -- Note that here we need the assumption that the carrier of A is a set.

    projective⇒type-like : is-set Carrier → projective c c → type-like c
    projective⇒type-like σ p =
      record { type-like-to = Σ Carrier (λ x → f ⟨$⟩ x ≡ x )
             ; type-like-≅ =
                 record { iso = record { _⟨$⟩_ = λ x → ( f ⟨$⟩ x , cong f (snd fθ x) )
                                       ; cong = λ ξ → Σ-≡ (cong f ξ) σ }
                        ; inv = record { _⟨$⟩_ = fst
                                       ; cong = λ { ≡-refl → refl } }
                        ; iso-inv = λ { (x , q) → Σ-≡ q σ }
                        ; inv-iso = snd fθ
                        }
             }

      where
        fθ = p (setoid Carrier)
               (record { _⟨$⟩_ = λ x → x ; cong = λ { ≡-refl → refl } })
               (λ y → y , refl)

        f : A ⟶ setoid Carrier
        f = fst fθ

    -- If A is type-like then it has canonical elements

    open canonical-elements

    type-like⇒canonical-elements : type-like c → canonical-elements
    type-like⇒canonical-elements
       record { type-like-to = T
              ; type-like-≅ = record { iso = f ; inv = g ; iso-inv = ζ ; inv-iso = ξ } }
       =
       record { canon = λ x → g ⟨$⟩ (f ⟨$⟩ x)
              ; canon-≈ = λ x → ξ x
              ; canon-≡ = λ x y ξ → ≡-cong (g ⟨$⟩_) (cong f ξ) }

    -- If A has canonical elements then it satisfies choice

    canonical-elements⇒satisfies-choice : ∀ {c' ℓ' r} → canonical-elements → satisfies-choice c' ℓ' r
    canonical-elements⇒satisfies-choice
      record { canon = c ; canon-≈ = c-≈ ; canon-≡ = c-≡ }
      B R r
      =  u , λ x →  rel-resp R (c-≈ x) (Setoid.reflexive B ≡-refl) (snd (r (c x)))

      where
        u : A ⟶ B
        u = record { _⟨$⟩_ = λ x → fst (r (c x))
                   ; cong = λ { ξ → Setoid.reflexive B (≡-cong (λ x → fst (r x)) (c-≡ _ _ ξ)) }}


  -- Corrolary: ℕ satisfies choice
  open import Data.Nat

  ℕ-choice : ∀ c ℓ r → satisfies-choice (setoid ℕ) c ℓ r
  ℕ-choice c ℓ r =
    canonical-elements⇒satisfies-choice
      (setoid ℕ)
      (type-like⇒canonical-elements (setoid ℕ)
         (record { type-like-to = ℕ ; type-like-≅ = ≅-refl }))