Add base case coequalizers in Nat

1 files changed, 123 insertions, 0 deletions

diff --git a/Nat/Properties.agda b/Nat/Properties.agda
new file mode 100644
index 0000000..3e1e0b4
--- /dev/null
+++ b/Nat/Properties.agda
@@ -0,0 +1,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})
+--             ?
+--             ?
+--     }