Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A setoid satisfies choice if, and only if its equivalence relation is equality.
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
= 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 ζ₂ ξ₂)}
}
}
= 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
= 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 }))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment