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

open import Categories.Category.Monoidal.Bundle
  using (SymmetricMonoidalCategory)

module Categories.Functor.Monoidal.Symmetric {o o′ ℓ ℓ′ e e′}
  (C : SymmetricMonoidalCategory o ℓ e) (D : SymmetricMonoidalCategory o′ ℓ′ e′)
  where

open import Level
open import Data.Product using (_,_)

open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal

private
  module C = SymmetricMonoidalCategory C renaming (braidedMonoidalCategory to B)
  module D = SymmetricMonoidalCategory D renaming (braidedMonoidalCategory to B)

import Categories.Functor.Monoidal.Braided C.B D.B as Braided

module Lax where
  open Braided.Lax

  -- Lax symmetric monoidal functors are just lax braided monoidal
  -- functors between symmetric monoidal categories.

  record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                 : Functor C.U D.U
      isBraidedMonoidal : IsBraidedMonoidalFunctor F

    open Functor F public
    open IsBraidedMonoidalFunctor isBraidedMonoidal public

    monoidalFunctor : MonoidalFunctor C.monoidalCategory D.monoidalCategory
    monoidalFunctor = record { isMonoidal = isMonoidal }

module Strong where
  open Braided.Strong

  -- Strong symmetric monoidal functors are just strong braided
  -- monoidal functors between symmetric monoidal categories.

  record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                 : Functor C.U D.U
      isBraidedMonoidal : IsBraidedMonoidalFunctor F

    open Functor F public
    open IsBraidedMonoidalFunctor isBraidedMonoidal public

    monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory D.monoidalCategory
    monoidalFunctor = record { isStrongMonoidal = isStrongMonoidal }

    laxSymmetricMonoidalFunctor : Lax.SymmetricMonoidalFunctor
    laxSymmetricMonoidalFunctor = record
      { isBraidedMonoidal = isLaxBraidedMonoidal }