Generalize coequalizer result to arbitrary category

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))