Remove extraneous up-to-iso argument

agda · Dec 7, 2024 · 1ac62b0 · 1ac62b0
1 parent 4aea83a
commit 1ac62b0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Categories/Diagram/Pushout/Properties.agda b/src/Categories/Diagram/Pushout/Properties.agda
@@ -39,8 +39,8 @@ module _ (p : Pushout f g) where
     using (unique′; id-unique; unique-diagram)
     public
 
-  up-to-iso : (p p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′
-  up-to-iso p p′ = op-≅⇒≅ (P′.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′))
+  up-to-iso : (p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′
+  up-to-iso p′ = op-≅⇒≅ (P′.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′))
 
   swap : Pushout g f
   swap = coPullback⇒Pushout (P′.swap pullback)