From f7afdb1823fe8d785849f817d022efa100007560 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 23 Apr 2025 10:09:32 -0500
Subject: Category of decorated cospans is symmetric monoidal

---
 Category/Cocomplete/Finitely/Bundle.agda | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Category/Cocomplete/Finitely/Bundle.agda')

diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
index 74f434f..8af8633 100644
--- a/Category/Cocomplete/Finitely/Bundle.agda
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -28,6 +28,7 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
       ; monoidal = monoidal
       ; symmetric = symmetric
       }
+  {-# INJECTIVE_FOR_INFERENCE symmetricMonoidalCategory #-}
 
   cocartesianCategory : CocartesianCategory o ℓ e
   cocartesianCategory = record
-- 
cgit v1.2.3