From a8735289bf749c3d08f40be3a26f29585c879f0d Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 3 Feb 2025 23:31:23 -0600
Subject: Show category of cospans is monoidal

---
 Category/Instance/Properties/FinitelyCocompletes.agda | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Category/Instance/Properties')

diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda
index 9f848f4..dedfa16 100644
--- a/Category/Instance/Properties/FinitelyCocompletes.agda
+++ b/Category/Instance/Properties/FinitelyCocompletes.agda
@@ -36,7 +36,9 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
   open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-)
   open Equiv
-  module -+- = Functor -+-
+
+  private
+    module -+- = Functor -+-
 
   +-resp-⊥
       : {(A , B) : 𝒞×𝒞.Obj}
-- 
cgit v1.2.3