{-# OPTIONS --without-K --safe #-}
 
open import Categories.Category.Monoidal.Bundle
  using (BraidedMonoidalCategory)
 
module Categories.Functor.Monoidal.Braided {o o′ ℓ ℓ′ e e′}
  (C : BraidedMonoidalCategory o ℓ e) (D : BraidedMonoidalCategory o′ ℓ′ e′)
  where
 
open import Level
open import Data.Product using (_,_)
 
open import Categories.Category using (module Commutation)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)
 
open NaturalIsomorphism
 
private
  module C = BraidedMonoidalCategory C
  module D = BraidedMonoidalCategory D
 
module Lax where
 
  -- Lax braided monoidal functors.
 
  record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F
 
    field
      isMonoidal : IsMonoidalFunctor C.monoidalCategory D.monoidalCategory F
 
    open IsMonoidalFunctor isMonoidal public
    open D
    open Commutation D.U
 
    -- coherence condition
 
    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.η (X , Y)              ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.η (Y , X)
                        ⟩
 
  record BraidedMonoidalFunctor : 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
 
  -- Strong braided monoidal functors.
 
  record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F
 
    field
      isStrongMonoidal : IsStrongMonoidalFunctor C.monoidalCategory
                                                 D.monoidalCategory F
 
    open IsStrongMonoidalFunctor isStrongMonoidal public
    open D
    open Commutation D.U
 
    -- coherence condition
 
    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.⇒.η (X , Y)            ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.⇒.η (Y , X)
                        ⟩
 
    isLaxBraidedMonoidal : Lax.IsBraidedMonoidalFunctor F
    isLaxBraidedMonoidal = record
      { isMonoidal      = isMonoidal
      ; braiding-compat = braiding-compat
      }
 
  record BraidedMonoidalFunctor : 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 }
 
    laxBraidedMonoidalFunctor : Lax.BraidedMonoidalFunctor
    laxBraidedMonoidalFunctor = record { isBraidedMonoidal = isLaxBraidedMonoidal }