blob: 7e855601d4271f901b3d387d8fc080858bce7421 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
{-# 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.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; 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 ₍_₎_≈_)
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
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 _ | _ = _
|
