From a408cbee9abbe2dbeee09bd36afc678efe7b6557 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 10 Jul 2026 17:21:14 -0700
Subject: Use latest agda-categories

---
 Functor/Instance/Cospan/Stack.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Functor/Instance/Cospan/Stack.agda')

diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda
index b72219b..568b99d 100644
--- a/Functor/Instance/Cospan/Stack.agda
+++ b/Functor/Instance/Cospan/Stack.agda
@@ -43,8 +43,7 @@ id⊗id≈id {A} {B} = record
   where
     open Morphism U using (module ≅)
     open HomReasoning
-    open 𝒞 using (+-η; []-cong₂)
-    open coproduct {A} {B} using (i₁; i₂)
+    open 𝒞 using (i₁; i₂; +-η; []-cong₂)
     from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id
     from∘f≈f = begin
         id ∘ [ i₁ ∘ id , i₂ ∘ id ]  ≈⟨ identityˡ ⟩
-- 
cgit v1.2.3