{-# OPTIONS --without-K --safe #-}
 
-- Definition of Monoidal Category
 
-- Big design decision that differs from the previous version:
-- Do not go through "Functor.Power" to encode variables and work
-- at the level of NaturalIsomorphisms, instead work at the object/morphism
-- level, via the more direct _⊗₀_ _⊗₁_ _⊗- -⊗_.
-- The original design needed quite a few contortions to get things working,
-- but these are simply not needed when working directly with the morphisms.
--
-- Smaller design decision: export some items with long names
-- (unitorˡ, unitorʳ and associator), but internally work with the more classical
-- short greek names (λ, ρ and α respectively).
 
module Categories.Category.Monoidal where
 
open import Categories.Category.Monoidal.Core public
open import Categories.Category.Monoidal.Bundle public