From 8a832a39547c21a0cde9cd3671f0368cd35c26c0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 19 Sep 2024 12:34:28 -0500 Subject: Add decorated cospans --- Category/Cocomplete/Finitely/SymmetricMonoidal.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 Category/Cocomplete/Finitely/SymmetricMonoidal.agda (limited to 'Category/Cocomplete/Finitely/SymmetricMonoidal.agda') diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda new file mode 100644 index 0000000..26813eb --- /dev/null +++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) + +module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where + +open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete) +open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) + + +module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where + + open FinitelyCocomplete finCo using (cocartesian) + open CocartesianMonoidal cocartesian using (+-monoidal) public + open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) public -- cgit v1.2.3