diff options
| -rw-r--r-- | Category/Monoidal/Instance/Nat.agda | 68 |
1 files changed, 51 insertions, 17 deletions
diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda index 9f1b990..24b30a6 100644 --- a/Category/Monoidal/Instance/Nat.agda +++ b/Category/Monoidal/Instance/Nat.agda @@ -3,16 +3,14 @@ module Category.Monoidal.Instance.Nat where open import Level using (0ℓ) -open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal) +open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian) -open CartesianMonoidal using () renaming (monoidal to ×-monoidal) -open CocartesianMonoidal using (+-monoidal) -open MonoidalCategory +import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal Natop-Cartesian : Cartesian Natop Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian @@ -20,18 +18,54 @@ Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian Natop-Cocartesian : Cocartesian Natop Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian -Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ -Nat,+,0 .U = Nat -Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian +module Monoidal where -Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ -Nat,×,1 .U = Nat -Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + open MonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) -Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ -Natop,+,0 .U = Natop -Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian -Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ -Natop,×,1 .U = Natop -Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + + Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + + Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + +module Symmetric where + + open SymmetricMonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) + open CartesianSymmetricMonoidal using () renaming (symmetric to ×-symmetric) + open CocartesianSymmetricMonoidal using (+-symmetric) + + Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian + + Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + Nat,×,1 .symmetric = ×-symmetric Nat Nat-Cartesian + + Natop,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + Natop,+,0 .symmetric = ×-symmetric Natop Natop-Cartesian + + Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian + +open Symmetric public |