From c3982b7fd9561fec34e60b28c0f20f03e9926f81 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 25 Apr 2024 17:38:21 -0500
Subject: Define coequalizers and pushouts in Nat

---
 Coeq.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Coeq.agda')

diff --git a/Coeq.agda b/Coeq.agda
index ad21587..1414dad 100644
--- a/Coeq.agda
+++ b/Coeq.agda
@@ -28,7 +28,7 @@ open Category Nat
     open Coproduct (IsCoproduct⇒Coproduct coprod)
     open HomReasoning
 
-iterated-coequalizer
+coequalizer-on-coproduct
     : {A B A+B C Q₁ Q₂ : Obj}
     → (i₁ : A ⇒ A+B)
     → (i₂ : B ⇒ A+B)
@@ -39,7 +39,7 @@ iterated-coequalizer
     → IsCoequalizer (f ∘ i₁) (g ∘ i₁) q₁
     → IsCoequalizer (q₁ ∘ f ∘ i₂) (q₁ ∘ g ∘ i₂) q₂
     → IsCoequalizer f g (q₂ ∘ q₁)
-iterated-coequalizer {C = C} {Q₁} {Q₂} i₁ i₂ f g q₁ q₂ coprod coeq₁ coeq₂ = record
+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)
-- 
cgit v1.2.3