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
|
{-# OPTIONS --without-K --safe #-}
module Nat.Properties where
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; #_; toℕ)
open import Data.Fin.Properties using (¬Fin0)
open import Data.Nat using (ℕ; s≤s)
open import Data.Product using (_,_; proj₁; proj₂; Σ-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.Nat using (Nat)
open import Categories.Diagram.Coequalizer Nat using (IsCoequalizer; Coequalizer)
open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct)
open import Coeq using (iterated-coequalizer)
open import FinMerge using (glue-iter; glue-unglue-once)
open import FinMerge.Properties using (lemma₂; merge-unmerge; unmerge-merge)
open import Util using (compare; less; equal; greater; _<_<_)
open Category Nat
makeZeroCoequalizer
: {B : ℕ}
→ (f g : 0 ⇒ B)
→ Coequalizer f g
makeZeroCoequalizer f g = record
{ arr = id
; isCoequalizer = record
{ equality = λ()
; coequalize = λ {_} {h} _ → h
; universal = λ _ → refl
; unique = λ h≈i∘id → Equiv.sym h≈i∘id
}
}
makeSimpleCoequalizer
: {B : ℕ}
→ (f g : 1 ⇒ B)
→ Coequalizer f g
makeSimpleCoequalizer {ℕ.zero} f g = ⊥-elim (¬Fin0 (f (# 0)))
makeSimpleCoequalizer {ℕ.suc B} f g = record
{ arr = proj₂ (glue-iter f g id)
; isCoequalizer = record
{ equality = λ { Fin.zero → lemma₂ f g }
; coequalize = λ {_} {h} h∘f≈h∘g → h ∘ proj₂ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0)))))
; universal = λ { {C} {h} {eq} → univ {C} {h} {eq} }
; unique = λ { {C} {h} {i} {eq} h≈i∘m → uniq {C} {h} {i} {eq} h≈i∘m }
}
}
where
univ
: {C : Obj} {h : ℕ.suc B ⇒ C} {eq : h ∘ f ≈ h ∘ g}
→ ∀ x
→ h x
≡ h ((proj₂ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0))))))
(proj₂ (glue-iter f g id) x))
univ {C} {h} {eq} x with compare (f ( # 0)) (g (# 0))
... | less (f0<g0 , s≤s g0≤n) =
sym (merge-unmerge (f0<g0 , g0≤n) h (eq (# 0)))
... | equal f0≡g0 = refl
... | greater (g0<f0 , s≤s f0≤n) =
sym (merge-unmerge (g0<f0 , f0≤n) h (sym (eq (# 0))))
uniq
: {C : Obj}
{h : ℕ.suc B ⇒ C}
{i : Fin (proj₁ (glue-iter f g id)) → Fin C}
{eq : h ∘ f ≈ h ∘ g}
→ (h≈i∘m : h ≈ i ∘ proj₂ (glue-iter f g id))
→ ∀ x
→ i x ≡ h (proj₂ (proj₂ (glue-unglue-once (compare (f (# 0)) (g (# 0))))) x)
uniq {C} {h} {i} {eq} h≈i∘m x with compare (f ( # 0)) (g (# 0))
... | less (f0<g0 , s≤s g0≤n) =
let
open ≡-Reasoning
m = proj₁ (proj₂ (glue-unglue-once (less (f0<g0 , s≤s g0≤n))))
u = proj₂ (proj₂ (glue-unglue-once (less (f0<g0 , s≤s g0≤n))))
in
begin
i x ≡⟨ cong i (sym (unmerge-merge (f0<g0 , g0≤n))) ⟩
i (m (u x)) ≡⟨ sym (h≈i∘m (u x)) ⟩
h (u x) ∎
... | equal f0≡g0 = sym (h≈i∘m x)
... | greater (g0<f0 , s≤s f0≤n) =
let
open ≡-Reasoning
m = proj₁ (proj₂ (glue-unglue-once (greater (g0<f0 , s≤s f0≤n))))
u = proj₂ (proj₂ (glue-unglue-once (greater (g0<f0 , s≤s f0≤n))))
in
begin
i x ≡⟨ cong i (sym (unmerge-merge (g0<f0 , f0≤n))) ⟩
i (m (u x)) ≡⟨ sym (h≈i∘m (u x)) ⟩
h (u x) ∎
split : {n : ℕ} → IsCoproduct {1} {n} {ℕ.suc n} (λ _ → Fin.zero) Fin.suc
split = record
{ [_,_] = λ { z _ Fin.zero → z Fin.zero
; _ s (Fin.suc x) → s x }
; inject₁ = λ { Fin.zero → refl }
; inject₂ = λ { _ → refl }
; unique = λ { h∘i₁≈f _ Fin.zero → (Equiv.sym h∘i₁≈f) Fin.zero
; h∘i₁≈f h∘i₂≈g (Fin.suc x) → (Equiv.sym h∘i₂≈g) x }
}
-- makeCoequalizer
-- : {A B : ℕ}
-- → (f g : A ⇒ B)
-- → Coequalizer f g
-- makeCoequalizer {ℕ.zero} f g = {! !}
-- makeCoequalizer {ℕ.suc A} f g = record
-- { arr = {! !}
-- ; isCoequalizer =
-- iterated-coequalizer
-- (λ _ → Fin.zero)
-- Fin.suc
-- f g
-- ? ?
-- (split {A})
-- ?
-- ?
-- }
|
