{-# 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