I: 4: d: demonstrate injections are exactly monomorphisms in Setoidsi-4-b-2

1 files changed, 41 insertions, 0 deletions

diff --git a/src/CatTheory/Category/Instance/Properties/Setoids.agda b/src/CatTheory/Category/Instance/Properties/Setoids.agda
new file mode 100644
index 0000000..68e0062
--- /dev/null
+++ b/src/CatTheory/Category/Instance/Properties/Setoids.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --safe #-}
+
+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.Unit.Polymorphic using (⊤)
+open import Function.Equality using (_⟨$⟩_; cong)
+open import Function.Structures using (IsInjection)
+open import Relation.Binary.Bundles using (Setoid)
+
+open Setoid renaming (_≈_ to ₍_₎_≈_)
+
+module Monomorphisms {o l} where
+  open Category (Setoids o l)
+  open M (Setoids o l)
+
+  Mono⇒IsInjection : ∀ {A B : Setoid o l} {f : A ⇒ B} → Mono f → IsInjection (₍ A ₎_≈_) (₍ B ₎_≈_) (f ⟨$⟩_)
+  Mono⇒IsInjection {A} {B} {f} mono = record
+    { isCongruent = record
+      { cong = cong f
+      ; isEquivalence₁ = isEquivalence A
+      ; isEquivalence₂ = isEquivalence B
+      }
+    ; injective   = λ {x} {y} fx≈fy → mono {C = ⊤-setoid} (point x) (point y) (λ _ → fx≈fy) _
+    }
+    where
+    ⊤-setoid : Setoid o l
+    ⊤-setoid = record
+      { Carrier = ⊤
+      ; _≈_ = λ _ _ → ⊤
+      ; isEquivalence = _
+      }
+
+    point : Carrier A → ⊤-setoid ⇒ A
+    point x = record { _⟨$⟩_ = λ _ → x ; cong = λ _ → refl A }
+
+  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