{-# OPTIONS --without-K --safe #-}

module Category.Monoidal.Instance.Nat where

open import Level using (0ℓ)
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)
open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian)

import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal

Natop-Cartesian : Cartesian Natop
Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian

Natop-Cocartesian : Cocartesian Natop
Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian

module Monoidal where

  open MonoidalCategory
  open CartesianMonoidal using () renaming (monoidal to ×-monoidal)
  open CocartesianMonoidal using (+-monoidal)

  Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ
  Nat,+,0 .U = Nat
  Nat,+,0 .monoidal = +-monoidal Nat-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-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-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-Cocartesian
  Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian

open Symmetric public