From dc3b799d6f9cdd4fb0b2b32f323b7128ccc14a80 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 24 Aug 2024 12:59:59 -0500 Subject: Generalize coequalizer result to arbitrary category --- Coeq.agda | 100 +++++++++++++++++++++------------------------------- Cospan.agda | 3 -- Nat/Properties.agda | 17 +++------ 3 files changed, 45 insertions(+), 75 deletions(-) diff --git a/Coeq.agda b/Coeq.agda index 1414dad..19523b0 100644 --- a/Coeq.agda +++ b/Coeq.agda @@ -1,79 +1,59 @@ {-# OPTIONS --without-K --safe #-} -module Coeq where - open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat) -open import Categories.Diagram.Coequalizer Nat using (IsCoequalizer) -open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct) +module Coeq {o ℓ e} (C : Category o ℓ e) where -open Category Nat +open import Categories.Diagram.Coequalizer C using (IsCoequalizer) +open import Categories.Object.Coproduct C using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct) +open import Categories.Morphism.Reasoning.Core C using (pullˡ; pushˡ; extendˡ; extendʳ; assoc²') +open import Function using (_$_) --- TODO: any category -≈-i₁-i₂ - : {A B A+B C : Obj} - → {i₁ : A ⇒ A+B} - → {i₂ : B ⇒ A+B} - → (f g : A+B ⇒ C) - → IsCoproduct i₁ i₂ - → f ∘ i₁ ≈ g ∘ i₁ - → f ∘ i₂ ≈ g ∘ i₂ - → f ≈ g -≈-i₁-i₂ f g coprod ≈₁ ≈₂ = begin - f ≈⟨ Equiv.sym g-η ⟩ - [ f ∘ i₁ , f ∘ i₂ ] ≈⟨ []-cong₂ ≈₁ ≈₂ ⟩ - [ g ∘ i₁ , g ∘ i₂ ] ≈⟨ g-η ⟩ - g ∎ - where - open Coproduct (IsCoproduct⇒Coproduct coprod) - open HomReasoning +open Category C coequalizer-on-coproduct : {A B A+B C Q₁ Q₂ : Obj} - → (i₁ : A ⇒ A+B) - → (i₂ : B ⇒ A+B) - → (f g : A+B ⇒ C) - → (q₁ : C ⇒ Q₁) - → (q₂ : Q₁ ⇒ Q₂) + → {i₁ : A ⇒ A+B} + → {i₂ : B ⇒ A+B} + → {f g : A+B ⇒ C} + → {q₁ : C ⇒ Q₁} + → {q₂ : Q₁ ⇒ Q₂} → IsCoproduct i₁ i₂ → IsCoequalizer (f ∘ i₁) (g ∘ i₁) q₁ → IsCoequalizer (q₁ ∘ f ∘ i₂) (q₁ ∘ g ∘ i₂) q₂ → IsCoequalizer f g (q₂ ∘ q₁) -coequalizer-on-coproduct {C = C} {Q₁} {Q₂} i₁ i₂ f g q₁ q₂ coprod coeq₁ coeq₂ = record - { equality = ≈-i₁-i₂ - (q₂ ∘ q₁ ∘ f) - (q₂ ∘ q₁ ∘ g) - coprod - (∘-resp-≈ʳ {g = q₂} X₁.equality) - X₂.equality - ; coequalize = λ {Q} {q} q∘f≈q∘g → let module X = Cocone {Q} {q} q∘f≈q∘g in X.u₂ - ; universal = λ {Q} {q} {q∘f≈q∘g} → let module X = Cocone {Q} {q} q∘f≈q∘g in X.q≈u₂∘q₂∘q₁ - ; unique = λ {Q} {q} {i} {q∘f≈q∘g} q≈i∘q₂∘q₁ → - let module X = Cocone {Q} {q} q∘f≈q∘g in X.q≈i∘q₂∘q₁⇒i≈u₂ q≈i∘q₂∘q₁ +coequalizer-on-coproduct {C = C} {Q₁} {Q₂} {f = f} {g} {q₁} {q₂} coprod coeq₁ coeq₂ = record + { equality = assoc ○ equality ○ sym-assoc + ; coequalize = λ eq → Cocone.u₂ eq + ; universal = λ { {eq = eq} → Cocone.univ eq } + ; unique = λ { {eq = eq} h≈i∘q₂∘q₁ → Cocone.uniq eq h≈i∘q₂∘q₁ } } where + open HomReasoning module X₁ = IsCoequalizer coeq₁ module X₂ = IsCoequalizer coeq₂ - module Cocone {Q : Obj} {q : C ⇒ Q} (q∘f≈q∘g : q ∘ f ≈ q ∘ g) where - open HomReasoning + open Coproduct (IsCoproduct⇒Coproduct coprod) using (g-η; [_,_]; unique; i₁; i₂) + on-i₁ : (q₂ ∘ q₁ ∘ f) ∘ i₁ ≈ (q₂ ∘ q₁ ∘ g) ∘ i₁ + on-i₁ = assoc²' ○ refl⟩∘⟨ X₁.equality ○ Equiv.sym assoc²' + on-i₂ : (q₂ ∘ q₁ ∘ f) ∘ i₂ ≈ (q₂ ∘ q₁ ∘ g) ∘ i₂ + on-i₂ = assoc²' ○ X₂.equality ○ Equiv.sym assoc²' + equality : q₂ ∘ q₁ ∘ f ≈ q₂ ∘ q₁ ∘ g + equality = begin + q₂ ∘ q₁ ∘ f ≈⟨ unique on-i₁ on-i₂ ⟨ + [ (q₂ ∘ q₁ ∘ g) ∘ i₁ , (q₂ ∘ q₁ ∘ g) ∘ i₂ ] ≈⟨ g-η ⟩ + q₂ ∘ q₁ ∘ g ∎ + module Cocone {Q : Obj} {h : C ⇒ Q} (eq : h ∘ f ≈ h ∘ g) where u₁ : Q₁ ⇒ Q - u₁ = X₁.coequalize (∘-resp-≈ˡ q∘f≈q∘g) - q≈u₁∘q₁ : q ≈ u₁ ∘ q₁ - q≈u₁∘q₁ = X₁.universal - u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ : u₁ ∘ q₁ ∘ f ∘ i₂ ≈ u₁ ∘ q₁ ∘ g ∘ i₂ - u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ = begin - u₁ ∘ q₁ ∘ f ∘ i₂ ≈⟨ ∘-resp-≈ˡ (Equiv.sym q≈u₁∘q₁) ⟩ - q ∘ f ∘ i₂ ≈⟨ ∘-resp-≈ˡ q∘f≈q∘g ⟩ - q ∘ g ∘ i₂ ≈⟨ ∘-resp-≈ˡ q≈u₁∘q₁ ⟩ - u₁ ∘ q₁ ∘ g ∘ i₂ ∎ + u₁ = X₁.coequalize (extendʳ eq) u₂ : Q₂ ⇒ Q - u₂ = X₂.coequalize u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ - u₁≈u₂∘q₂ : u₁ ≈ u₂ ∘ q₂ - u₁≈u₂∘q₂ = X₂.universal - q≈u₂∘q₂∘q₁ : q ≈ u₂ ∘ q₂ ∘ q₁ - q≈u₂∘q₂∘q₁ = begin - q  ≈⟨ q≈u₁∘q₁ ⟩ - u₁ ∘ q₁ ≈⟨ ∘-resp-≈ˡ u₁≈u₂∘q₂ ⟩ + u₂ = X₂.coequalize $ begin + u₁ ∘ q₁ ∘ f ∘ i₂ ≈⟨ pullˡ (Equiv.sym X₁.universal) ⟩ + h ∘ f ∘ i₂ ≈⟨ extendʳ eq ⟩ + h ∘ g ∘ i₂ ≈⟨ pushˡ X₁.universal ⟩ + u₁ ∘ q₁ ∘ g ∘ i₂ ∎ + univ : h ≈ u₂ ∘ q₂ ∘ q₁ + univ = begin + h  ≈⟨ X₁.universal ⟩ + u₁ ∘ q₁ ≈⟨ pushˡ X₂.universal ⟩ u₂ ∘ q₂ ∘ q₁ ∎ - q≈i∘q₂∘q₁⇒i≈u₂ : {i : Q₂ ⇒ Q} → q ≈ i ∘ q₂ ∘ q₁ → i ≈ u₂ - q≈i∘q₂∘q₁⇒i≈u₂ q≈i∘q₂∘q₁ = X₂.unique (Equiv.sym (X₁.unique q≈i∘q₂∘q₁)) + uniq : {i : Q₂ ⇒ Q} → h ≈ i ∘ q₂ ∘ q₁ → i ≈ u₂ + uniq h≈i∘q₂∘q₁ = X₂.unique (Equiv.sym (X₁.unique (h≈i∘q₂∘q₁ ○ sym-assoc))) diff --git a/Cospan.agda b/Cospan.agda index f3bb5f5..3c5296d 100644 --- a/Cospan.agda +++ b/Cospan.agda @@ -110,9 +110,6 @@ glue-i₂ p₁ p₂ = swap (glue (swap p₁) (swap p₂)) up-to-iso : (p p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′ up-to-iso p p′ = op-≅⇒≅ (Pb.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′)) -id-unique : (p : Pushout f g) → (Pushout.universal p) (Pushout.commute p) ≈ id -id-unique p = Equiv.sym (Pushout.unique p identityˡ identityˡ) - pushout-f-id : Pushout f id pushout-f-id {_} {_} {f} = record { i₁ = id diff --git a/Nat/Properties.agda b/Nat/Properties.agda index a6fb060..6e04346 100644 --- a/Nat/Properties.agda +++ b/Nat/Properties.agda @@ -16,7 +16,7 @@ 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 Coeq Nat 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; _<_<_) @@ -107,17 +107,10 @@ 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 + ; isCoequalizer = coequalizer-on-coproduct + split + Q₁.isCoequalizer + Q₂.isCoequalizer } where simpleCoeq : Coequalizer (λ _ → f (# 0)) (λ _ → g (# 0)) -- cgit v1.2.3