blob: 2b66d19f1ae7d8b97bc0b32a02d3f84d42ca6784 (
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 𝒞 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
|
