From dc3b799d6f9cdd4fb0b2b32f323b7128ccc14a80 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 24 Aug 2024 12:59:59 -0500
Subject: Generalize coequalizer result to arbitrary category

---
 Cospan.agda | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'Cospan.agda')

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
-- 
cgit v1.2.3