From 584abc089280cfe82e7dff54a67008dcc39dae0d Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 9 Dec 2024 13:41:43 -0600
Subject: [PATCH] Add predicate form for pushouts

---
 src/Categories/Diagram/Duality.agda | 16 +++++++++-------
 src/Categories/Diagram/Pushout.agda | 20 +++++++++++---------
 2 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/Categories/Diagram/Duality.agda b/src/Categories/Diagram/Duality.agda
index 9cec440e..aa1423e7 100644
--- a/src/Categories/Diagram/Duality.agda
+++ b/src/Categories/Diagram/Duality.agda
@@ -76,13 +76,15 @@ coEqualizer⇒Coequalizer e = record
 
 coPullback⇒Pushout : Pullback f g → Pushout f g
 coPullback⇒Pushout p = record
-  { i₁              = p₁
-  ; i₂              = p₂
-  ; commute         = commute
-  ; universal       = universal
-  ; universal∘i₁≈h₁ = p₁∘universal≈h₁
-  ; universal∘i₂≈h₂ = p₂∘universal≈h₂
-  ; unique-diagram  = unique-diagram
+  { i₁        = p₁
+  ; i₂        = p₂
+  ; isPushout = record
+    { commute         = commute
+    ; universal       = universal
+    ; universal∘i₁≈h₁ = p₁∘universal≈h₁
+    ; universal∘i₂≈h₂ = p₂∘universal≈h₂
+    ; unique-diagram  = unique-diagram
+    }
   }
   where open Pullback p
 
diff --git a/src/Categories/Diagram/Pushout.agda b/src/Categories/Diagram/Pushout.agda
index ddb84b37..8a89699f 100644
--- a/src/Categories/Diagram/Pushout.agda
+++ b/src/Categories/Diagram/Pushout.agda
@@ -6,10 +6,6 @@ module Categories.Diagram.Pushout {o ℓ e} (C : Category o ℓ e) where
 
 open Category C
 open HomReasoning
-open Equiv
-
-open import Categories.Morphism.Reasoning C as Square
-  renaming (glue to glue-square) hiding (id-unique)
 
 open import Level
 
@@ -18,11 +14,7 @@ private
     A B E X Y Z : Obj
     f g h j : A ⇒ B
 
-record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
-  field
-    {Q} : Obj
-    i₁  : Y ⇒ Q
-    i₂  : Z ⇒ Q
+record IsPushout {Q : Obj} (f : X ⇒ Y) (g : X ⇒ Z) (i₁ : Y ⇒ Q) (i₂ : Z ⇒ Q) : Set (o ⊔ ℓ ⊔ e) where
 
   field
     commute         : i₁ ∘ f ≈ i₂ ∘ g
@@ -39,3 +31,13 @@ record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
     unique-diagram
       (j∘i₁≈h₁ ○ ⟺ universal∘i₁≈h₁)
       (j∘i₂≈h₂ ○ ⟺ universal∘i₂≈h₂)
+
+record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    {Q} : Obj
+    i₁  : Y ⇒ Q
+    i₂  : Z ⇒ Q
+    isPushout : IsPushout f g i₁ i₂
+
+  open IsPushout isPushout public