blob: bae9774e8452b783d6f72a5e89a8bf23e69b5eab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.Monoidal using (module CocartesianMonoidal)
open import Categories.Category.Cocartesian.SymmetricMonoidal 𝒞 using (module CocartesianSymmetricMonoidal)
module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete) where
open FinitelyCocomplete finCo using (cocartesian)
open CocartesianMonoidal cocartesian using (+-monoidal) public
open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) public
|
