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
|
{-# 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; Coprod)
open import Categories.Diagram.Coequalizer Nat using (IsCoequalizer; Coequalizer)
open import Categories.Diagram.Pushout Nat using (Pushout)
open import Categories.Diagram.Pushout.Properties Nat using (Coproduct×Coequalizer⇒Pushout)
open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct)
open import Coeq using (coequalizer-on-coproduct)
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 = 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} = ⊥-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 }
}
-- Coequalizers for Nat
Coeq : {A B : ℕ} (f g : A ⇒ B) → Coequalizer f g
Coeq {ℕ.zero} _ _ = makeZeroCoequalizer
Coeq {ℕ.suc A} f g = record
{ arr = Q₂.arr ∘ Q₁.arr
; isCoequalizer =
coequalizer-on-coproduct
(λ _ → Fin.zero)
Fin.suc
f
g
Q₁.arr
Q₂.arr
split
Q₁.isCoequalizer
Q₂.isCoequalizer
}
where
simpleCoeq : Coequalizer (λ _ → f (# 0)) (λ _ → g (# 0))
simpleCoeq = makeSimpleCoequalizer
module Q₁ = Coequalizer simpleCoeq
recursiveCoeq : Coequalizer (Q₁.arr ∘ f ∘ Fin.suc) (Q₁.arr ∘ g ∘ Fin.suc)
recursiveCoeq = Coeq _ _
module Q₂ = Coequalizer recursiveCoeq
-- Pushouts for Nat
Push : {A B C : ℕ} (f : A ⇒ B) (g : A ⇒ C) → Pushout f g
Push {A} {B} {C} f g =
Coproduct×Coequalizer⇒Pushout B+C (Coeq (B+C.i₁ ∘ f) (B+C.i₂ ∘ g))
where
B+C : Coproduct B C
B+C = Coprod B C
module B+C = Coproduct B+C
|
