{-# OPTIONS --without-K --safe #-} module Categories.Category.Monoidal.Structure where open import Level open import Categories.Category open import Categories.Category.Monoidal.Core open import Categories.Category.Monoidal.Braided open import Categories.Category.Monoidal.Symmetric record MonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where field U : Category o ℓ e monoidal : Monoidal U module U = Category U module monoidal = Monoidal monoidal open U public open monoidal public record BraidedMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where field U : Category o ℓ e monoidal : Monoidal U braided : Braided monoidal module U = Category U module monoidal = Monoidal monoidal module braided = Braided braided monoidalCategory : MonoidalCategory o ℓ e monoidalCategory = record { U = U ; monoidal = monoidal } open U public open braided public record SymmetricMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where field U : Category o ℓ e monoidal : Monoidal U symmetric : Symmetric monoidal module U = Category U module monoidal = Monoidal monoidal module symmetric = Symmetric symmetric braidedMonoidalCategory : BraidedMonoidalCategory o ℓ e braidedMonoidalCategory = record { U = U ; monoidal = monoidal ; braided = symmetric.braided } open U public open symmetric public open BraidedMonoidalCategory braidedMonoidalCategory public using (monoidalCategory)