I: 5: a: characterise epimorphisms of Setoids

Note that whilst the decidability argument might look suspicious, it can be
provided trivially assuming the law of excluded middle.

1 files changed, 100 insertions, 1 deletions

diff --git a/src/CatTheory/Category/Instance/Properties/Setoids.agda b/src/CatTheory/Category/Instance/Properties/Setoids.agda
index 68e0062..7e85560 100644
--- a/src/CatTheory/Category/Instance/Properties/Setoids.agda
+++ b/src/CatTheory/Category/Instance/Properties/Setoids.agda
@@ -5,10 +5,21 @@ module CatTheory.Category.Instance.Properties.Setoids where
 open import Categories.Category using (Category)
 open import Categories.Category.Instance.Setoids
 import Categories.Morphism as M
+open import Data.Bool using (if_then_else_)
+open import Data.Empty using (⊥-elim)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Product using (∃; _,_)
 open import Data.Unit.Polymorphic using (⊤)
+open import Function using () renaming (id to idf)
 open import Function.Equality using (_⟨$⟩_; cong)
-open import Function.Structures using (IsInjection)
+open import Function.Structures using (IsInjection; IsSurjection)
 open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+import Relation.Binary.Reasoning.Setoid as Reasoning
+open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary.Construct.Add.Point
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
+open import Relation.Unary using (Decidable)
 
 open Setoid renaming (_≈_ to ₍_₎_≈_)
 
@@ -39,3 +50,91 @@ module Monomorphisms {o l} where
   IsInjection⇒Mono : ∀ {A B : Setoid o l} {f : A ⇒ B} → IsInjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_) → Mono f
   IsInjection⇒Mono {A} {B} {f} isInjection g₁ g₂ f∘g₁≈f∘g₂ x≈y = injective (f∘g₁≈f∘g₂ x≈y)
     where open IsInjection isInjection
+
+module Epimorphisms {o l} where
+  open Category (Setoids o l)
+  open M (Setoids o l)
+
+  IsSujection⇒Epi : ∀ {A B : Setoid o l} {f : A ⇒ B} → IsSurjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_) → Epi f
+  IsSujection⇒Epi {A} {B} {f} isSurjection {C} g₁ g₂ g₁∘f≈g₂∘f {x} {y} x≈y with surjective x
+    where open IsSurjection isSurjection
+  ... | a , fa≈x = begin
+    g₁ ⟨$⟩ x         ≈˘⟨ cong g₁ fa≈x ⟩
+    g₁ ⟨$⟩ (f ⟨$⟩ a) ≈⟨  g₁∘f≈g₂∘f (refl A) ⟩
+    g₂ ⟨$⟩ (f ⟨$⟩ a) ≈⟨  cong g₂ fa≈x ⟩
+    g₂ ⟨$⟩ x         ≈⟨  cong g₂ x≈y ⟩
+    g₂ ⟨$⟩ y         ∎
+    where open Reasoning C
+
+  Epi⇒IsSurjection : ∀ {A B : Setoid o l} {f : A ⇒ B} →
+                     Decidable (λ y → ∃ λ x → ₍ B ₎ f ⟨$⟩ x ≈ y) →
+                     Epi f →
+                     IsSurjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_)
+  Epi⇒IsSurjection {A} {B} {f} image? epi = record
+    { isCongruent = record
+      { cong = cong f
+      ; isEquivalence₁ = isEquivalence A
+      ; isEquivalence₂ = isEquivalence B
+      }
+    ; surjective = λ y → toWitness (imageTrue y)
+    }
+    where
+    _≈∙_ : Pointed (Carrier B) → Pointed (Carrier B) → Set l
+    [ x ] ≈∙ [ y ] = ₍ B ₎ x ≈ y
+    [ x ] ≈∙ ∙     = ⊥
+    ∙     ≈∙ [ y ] = ⊥
+    ∙     ≈∙ ∙     = ⊤
+
+    ≈∙-refl : Reflexive _≈∙_
+    ≈∙-refl {[ x ]} = refl B
+    ≈∙-refl {∙}     = _
+
+    ≈∙-sym : Symmetric _≈∙_
+    ≈∙-sym {[ x ]} {[ y ]} x≈y = sym B x≈y
+    ≈∙-sym {∙}     {∙}     _   = _
+
+    ≈∙-trans : Transitive _≈∙_
+    ≈∙-trans {[ x ]} {[ y ]} {[ z ]} x≈y y≈z = trans B x≈y y≈z
+    ≈∙-trans {∙}     {∙}     {∙}     _   _   = _
+
+    -- Need these levels or we cannot use epi.
+    -- Otherwise, use Relation.Binary.Contruct.Add.Point.Equality.
+    C : Setoid o l
+    C = record
+      { _≈_ = _≈∙_
+      ; isEquivalence = record
+        { refl = λ {x} → ≈∙-refl {x}
+        ; sym = λ {x} {y} → ≈∙-sym {x} {y}
+        ; trans = λ {x} {y} {z} → ≈∙-trans {x} {y} {z}
+        }
+      }
+
+    g₁ : B ⇒ C
+    g₁ = record { _⟨$⟩_ = [_] ; cong = idf }
+
+    g₂ : B ⇒ C
+    g₂ = record
+      { _⟨$⟩_ = map
+      ; cong = λ i≈j → map-cong i≈j
+      }
+      where
+      map = λ y → if does (image? y) then [ y ] else ∙
+
+      map-cong : ∀ {i j} → ₍ B ₎ i ≈ j → ₍ C ₎ map i ≈ map j
+      map-cong {i} {j} i≈j with image? i | image? j
+      ... | yes _          | yes _          = i≈j
+      ... | yes (a , fa≈i) | no ¬fx≈j       = ⊥-elim (¬fx≈j (a , trans B fa≈i i≈j))
+      ... | no ¬fx≈i       | yes (b , fb≈j) = ⊥-elim (¬fx≈i (b , trans B fb≈j (sym B i≈j)))
+      ... | no _           | no _           = _
+
+    g₁∘f≈g₂∘f : g₁ ∘ f ≈ g₂ ∘ f
+    g₁∘f≈g₂∘f {x} {y} x≈y with image? (f ⟨$⟩ y)
+    ... | yes _      = cong f x≈y
+    ... | no ¬∃fz≈fy = ⊥-elim (¬∃fz≈fy (y , refl B))
+
+    g₁≈g₂ : g₁ ≈ g₂
+    g₁≈g₂ = epi g₁ g₂ g₁∘f≈g₂∘f
+
+    imageTrue : ∀ y → True (image? y)
+    imageTrue y with image? y | g₁≈g₂ {y} (refl B)
+    ... | yes _ | _ = _