From 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Aug 2026 19:08:47 -0500 Subject: Show category of maps is monoidal --- Category/Semiadditive.agda | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'Category/Semiadditive.agda') diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 05ce264..86b5585 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -13,6 +13,7 @@ open import Categories.Category.CMonoidEnriched using (CM-Category) open import Categories.Category.Cartesian 𝒞 using (Cartesian) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Cocartesian 𝒞 using (Cocartesian) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) @@ -176,6 +177,3 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { initial = initial ; coproducts = binaryCoproducts } - - open CartesianMonoidal cartesian using (monoidal) public - open CartesianSymmetricMonoidal cartesian using (symmetric) public -- cgit v1.2.3