Instantly share code, notes, and snippets.

# andrejbauer/Epimorphism.agda

Last active January 26, 2023 20:44
Show Gist options
• Save andrejbauer/65ee1ae98167e6411e512d3e5a36c086 to your computer and use it in GitHub Desktop.
A setoid satisfies choice if, and only if its equivalence relation is equality.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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)))
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 -- 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 }))