diff options
| -rw-r--r-- | Nat/Properties.agda | 123 |
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}) +-- ? +-- ? +-- } |