andrejbauer/Epimorphism.agda

## 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 }))
	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)))
	-- 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 }))