Skip to content

Instantly share code, notes, and snippets.

@JacquesCarette

JacquesCarette/Epimorphism.agda

Forked from andrejbauer/Epimorphism.agda
Last active January 13, 2022 04:22
Show Gist options
  • Save JacquesCarette/bb5ad3d42e6cfac010899dad54497c21 to your computer and use it in GitHub Desktop.
Save JacquesCarette/bb5ad3d42e6cfac010899dad54497c21 to your computer and use it in GitHub Desktop.
Download ZIP
A setoid satisfies choice if, and only if its equivalence relation is equality.
Raw
Epimorphism.agda
open import Level using (Level; suc; _⊔_; Lift; lift; lower)
open import Relation.Binary using (Setoid)
open import Data.Product using (_×_; swap; zip; ∃; map₂; proj₁; proj₂)
open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)
open import Function.Equality hiding (setoid; flip)
open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_)
import Relation.Binary.Reasoning.Setoid as SetoidR
module Epimorphism where
-- We characterize epimorphisms in setoids as precisely the surjective setoid maps
-- Setoid preliminaries
∣_∣ : ∀ {c ℓ} (B : Setoid c ℓ) → Set c
∣_∣ = Setoid.Carrier
-- The setoid of propositions
𝒫 : ∀ c → Setoid (suc c) c
𝒫 c =
record { Carrier = Set c
; _≈_ = λ P Q → (P → Q) × (Q → P)
; isEquivalence = record { refl = id→ , id→
; sym = swap
; trans = zip (flip _∘→_) _∘→_
}
}
-- Some observations about the setoid of setoids which we do not need
SetoidLift : ∀ {c ℓ} c' ℓ' → Setoid c ℓ → Setoid (c ⊔ c') (ℓ ⊔ ℓ')
SetoidLift c' ℓ' A =
record { Carrier = Lift c' ∣ A ∣
; _≈_ = λ x y → Lift ℓ' (lower x ≈ lower y)
; isEquivalence = record { refl = lift refl
; sym = λ ξ → lift (Setoid.sym A (lower ξ))
; trans = λ ζ ξ → lift (Setoid.trans A (lower ζ) (lower ξ))
}
}
where
open Setoid A
-- Isomorphism of setoids
infix 3 _≅_
record _≅_ {c₁ ℓ₁ c₂ ℓ₂} (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
private
module A = Setoid A
module B = Setoid B
field
iso : A ⟶ B
inv : B ⟶ A
iso-inv : ∀ y → iso ⟨$⟩ (inv ⟨$⟩ y) B.≈ y
inv-iso : ∀ x → inv ⟨$⟩ (iso ⟨$⟩ x) A.≈ 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 = iso∘inv
; inv-iso = inv∘iso
}
where
module C = Setoid C
module A = Setoid A
iso∘inv : (c : ∣ C ∣ ) → iso ξ ∘ iso ζ ⟨$⟩ (inv ζ ∘ inv ξ ⟨$⟩ c) C.≈ c
iso∘inv _ = begin
iso ξ ∘ iso ζ ⟨$⟩ (inv ζ ∘ inv ξ ⟨$⟩ _) ≈⟨ cong (iso ξ) (iso-inv ζ _) ⟩
iso ξ ∘ inv ξ ⟨$⟩ _ ≈⟨ iso-inv ξ _ ⟩
_ ∎
where open SetoidR C
inv∘iso : (a : ∣ A ∣ ) → inv ζ ∘ inv ξ ⟨$⟩ (iso ξ ∘ iso ζ ⟨$⟩ a) A.≈ a
inv∘iso _ = begin
inv ζ ∘ inv ξ ⟨$⟩ (iso ξ ∘ iso ζ ⟨$⟩ _) ≈⟨ cong (inv ζ) (inv-iso ξ _) ⟩
inv ζ ∘ iso ζ ⟨$⟩ _ ≈⟨ inv-iso ζ _ ⟩
_ ∎
where open SetoidR A
cong-SetoidLift : ∀ {c ℓ c' ℓ'} {A B : Setoid c ℓ} → A ≅ B → SetoidLift c' ℓ' A ≅ SetoidLift c' ℓ' B
cong-SetoidLift ξ = ≅-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 ℓ) → (∣ A ∣ → Set k) → Setoid (c ⊔ k) ℓ
𝕊 A P =
record { Carrier = ∃ P
; _≈_ = λ u v → fst u ≈ fst v
; isEquivalence = record { refl = refl ; sym = sym ; trans = trans } }
where open Setoid 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 { _⟨$⟩_ = map₂ f ; cong = id→ }
; inv = record { _⟨$⟩_ = map₂ g ; cong = id→ }
; iso-inv = λ _ → refl
; inv-iso = λ _ → refl
}
where open Setoid A using (refl)
surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂)
surjective {B = B} f = ∀ y → ∃ (λ x → f ⟨$⟩ x ≈ y) where open Setoid B
epi : ∀ {c₁ ℓ₁ c₂ ℓ₂} c ℓ {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂ ⊔ suc c ⊔ suc ℓ)
epi c ℓ {B = B} f = ∀ (C : Setoid c ℓ) (g h : B ⟶ C) → let open Setoid C in
(∀ a → g ⟨$⟩ (f ⟨$⟩ a) ≈ h ⟨$⟩ (f ⟨$⟩ a)) → ∀ b → 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 =
let (a , fa≈b) = σ b in
begin
g ⟨$⟩ b ≈⟨ cong g (Setoid.sym B fa≈b) ⟩
g ⟨$⟩ (f ⟨$⟩ a) ≈⟨ ξ (fst (σ b)) ⟩
h ⟨$⟩ (f ⟨$⟩ a) ≈⟨ cong h fa≈b ⟩
h ⟨$⟩ b ∎
where open SetoidR C
epi⇒surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (f : A ⟶ B) →
epi _ _ f → surjective f
epi⇒surjective {c₁ = c₁} {ℓ₁ = ℓ₁} {c₂ = c₂} {ℓ₂ = ℓ₂} {A = A} {B = B} f ε b =
fst aζ , Setoid.sym B (snd aζ)
where
module B = Setoid B
_○_ = Setoid.trans B
⟺ = Setoid.sym B
g : B ⟶ 𝒫 (c₁ ⊔ ℓ₂)
g ._⟨$⟩_ b' = Lift c₁ (b B.≈ b')
g .cong ξ .fst ζ = lift (lower ζ ○ ξ)
g .cong ξ .snd ζ = lift (lower ζ ○ ⟺ ξ)
h : B ⟶ 𝒫 (c₁ ⊔ ℓ₂)
h ._⟨$⟩_ b' = b B.≈ b' × Σ ∣ A ∣ λ a → b' B.≈ f ⟨$⟩ a
h .cong ξ .fst (ζ , (a , θ)) = ζ ○ ξ , a , ⟺ ξ ○ θ
h .cong ξ .snd (ζ , (a , θ)) = ζ ○ ⟺ ξ , a , ξ ○ θ
gf≈hf : ∀ a → let open Setoid (𝒫 (c₁ ⊔ ℓ₂)) in g ⟨$⟩ (f ⟨$⟩ a) ≈ h ⟨$⟩ (f ⟨$⟩ a)
gf≈hf a .fst ξ = lower ξ , a , cong f (Setoid.refl A)
gf≈hf a .snd = lift ∘→ proj₁
g≈h : ∀ b → let open Setoid (𝒫 (c₁ ⊔ ℓ₂)) in g ⟨$⟩ b ≈ h ⟨$⟩ b
g≈h b = ε _ g h gf≈hf b
aζ = snd (fst (g≈h b) (lift (Setoid.refl B)))
Raw
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
-- This version has been edited by Jacques Carette, January 10--12.
-- It is not meant to be 'better', but rather an experiment with writing things
-- somewhat differently. And it's still a WIP.
open import Level
open import Relation.Binary
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Data.Product.Properties
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)
open import Function.Inverse as FI hiding (id; sym)
open import Function.Bundles using (module Inverse)
import Relation.Binary.Reasoning.Setoid as SetoidR
module SetoidChoice where
-- ===== Preliminaries =====
-- Setoid Utilities
∣_∣ : ∀ {c ℓ} → Setoid c ℓ → Set c
∣_∣ = Setoid.Carrier
[_][_≈_] : ∀ {c ℓ} → (C : Setoid c ℓ) → (x y : ∣ C ∣) → Set ℓ
[_][_≈_] = Setoid._≈_
-- the definition of h-sets
is-set : ∀ {ℓ} → Set ℓ → Set ℓ
is-set A = ∀ {x y : A} {p q : x ≡ y} → p ≡ q
_≅_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} (A : Setoid c₁ ℓ₁) (B : Setoid c₂ ℓ₂) → Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂)
_≅_ = Inverse
-- 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₂} → [ A ][ x₁ ≈ x₂ ] → [ B ][ y₁ ≈ y₂ ] → rel x₁ y₁ → rel x₂ y₂
record RelTo {c ℓ c' ℓ' r} {A : Setoid c ℓ} {B : Setoid c' ℓ'} (R : SetoidRelation r A B) (a : ∣ A ∣ ) : Set (c ⊔ c' ⊔ ℓ ⊔ ℓ' ⊔ r) where
constructor relat
field
pt : ∣ B ∣
relTo : SetoidRelation.rel R a pt
f-rel : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → SetoidRelation ℓ₂ A B
f-rel {B = B} f .SetoidRelation.rel a b = [ B ][ f ⟨$⟩ a ≈ b ]
f-rel {A = A} {B = B} f .SetoidRelation.rel-resp {a₁} {a₂} {b₁} {b₂} a₁≈a₂ b₁≈b₂ fa₁≈b₁ = begin
f ⟨$⟩ a₂ ≈⟨ cong f (Setoid.sym A a₁≈a₂) ⟩
f ⟨$⟩ a₁ ≈⟨ fa₁≈b₁ ⟩
b₁ ≈⟨ b₁≈b₂ ⟩
b₂ ∎
where open SetoidR B
f⁻¹-rel : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → B ⟶ A → SetoidRelation ℓ₁ A B
f⁻¹-rel {A = A} f .SetoidRelation.rel a b = [ A ][ f ⟨$⟩ b ≈ a ]
f⁻¹-rel {A = A} {B = B} f .SetoidRelation.rel-resp {a₁} {a₂} {b₁} {b₂} a₁≈a₂ b₁≈b₂ fa₁≈b₁ = begin
f ⟨$⟩ b₂ ≈⟨ cong f (Setoid.sym B b₁≈b₂) ⟩
f ⟨$⟩ b₁ ≈⟨ fa₁≈b₁ ⟩
a₁ ≈⟨ a₁≈a₂ ⟩
a₂ ∎
where open SetoidR A
-- A SetoidRelation induces a Setoid
record relWitness {c₁ ℓ₁ c₂ ℓ₂ k} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (R : SetoidRelation k A B) : Set (c₁ ⊔ c₂ ⊔ k ) where
constructor relW
open SetoidRelation R
field
a∈A : ∣ A ∣
b∈B : ∣ B ∣
related : rel a∈A b∈B
open relWitness
RelSetoid : ∀ {c₁ ℓ₁ c₂ ℓ₂ k} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → SetoidRelation k A B → Setoid (c₁ ⊔ c₂ ⊔ k) (ℓ₁ ⊔ ℓ₂)
RelSetoid R .Setoid.Carrier = relWitness R
RelSetoid {A = A} {B} R .Setoid._≈_ w₁ w₂ = [ A ][ w₁ .a∈A ≈ w₂ .a∈A ] × [ B ][ w₁ .b∈B ≈ w₂ .b∈B ]
RelSetoid {A = A} {B} R .Setoid.isEquivalence = record { refl = Setoid.refl A , Setoid.refl B
; sym = Data.Product.map (Setoid.sym A) (Setoid.sym B)
; trans = Data.Product.zip (Setoid.trans A) (Setoid.trans B) }
-- 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 → [ B ][ f ⟨$⟩ x ≈ y ]
-- Note how surjective as above is not a well-behaved SetoidRelation? Fixing that:
surjective′ : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂)
surjective′ {B = B} f = ∀ y → RelTo (f-rel f) y
-- The definition of a split setoid morphism
record split {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} (f : A ⟶ B) : Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
constructor splits
field
f⁻¹ : B ⟶ A
right-inv : ∀ y → [ B ][ f ⟨$⟩ (f⁻¹ ⟨$⟩ y) ≈ y ]
open split
module _ {c ℓ} (A : Setoid c ℓ) where
open Setoid A
open SetoidRelation
private
_○_ = trans
⟺ = sym
-- ===== 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 → RelTo 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 =
let sc = ac _ (f⁻¹-rel f) rt in splits (fst sc) (snd sc)
where
rt : ∀ b → RelTo (f⁻¹-rel f) b
rt b = let (a , fa≈b) = s b in relat a fa≈b
projective⇒satisfies-choice : ∀ c' ℓ' → projective (c ⊔ ℓ ⊔ c') (ℓ ⊔ ℓ') → satisfies-choice c' ℓ' ℓ
projective⇒satisfies-choice c' ℓ' p B R r =
u , λ x → rel-resp R (right-inv uθ x) (Setoid.refl B) (related (f⁻¹ uθ ⟨$⟩ x))
where
C = RelSetoid R
uθ = p C
(record { _⟨$⟩_ = a∈A ; cong = fst })
λ x → relW x (RelTo.pt (r x)) (RelTo.relTo (r x)) , refl
u : A ⟶ B
u = record { _⟨$⟩_ = λ x → b∈B (f⁻¹ uθ ⟨$⟩ x)
; cong = λ ξ → snd (cong (f⁻¹ 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
{ to = record { _⟨$⟩_ = λ x → (f ⟨$⟩ x , cong f (right-inv fθ x))
; cong = λ ξ → Σ-≡,≡↔≡ .Inverse.f (cong f ξ , σ) }
; from = record { _⟨$⟩_ = fst
; cong = λ i≡j → reflexive (≡-cong fst i≡j) }
; inverse-of = record { left-inverse-of = right-inv fθ
; right-inverse-of = λ eq → Σ-≡,≡↔≡ .Inverse.f (snd eq , σ) }
}
}
where
fθ = p (setoid Carrier)
(record { _⟨$⟩_ = λ x → x ; cong = λ { ≡-refl → refl } })
(λ y → y , refl)
f : A ⟶ setoid Carrier
f = f⁻¹ 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 { to = f ; from = g ; inverse-of = record {left-inverse-of = ξ ; right-inverse-of = _ } } }
=
record { canon = λ x → g ⟨$⟩ (f ⟨$⟩ x)
; canon-≈ = ξ
; canon-≡ = λ _ _ ξ → ≡-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) (RelTo.relTo (r (c x)))
where
u : A ⟶ B
u = record { _⟨$⟩_ = λ x → RelTo.pt (r (c x))
; cong = λ { ξ → Setoid.reflexive B (≡-cong (λ x → RelTo.pt (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-≅ = FI.id }))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment