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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Cartesian using (Cartesian)

-- Defines the following properties of a Category:
-- Cartesian.SymmetricMonoidal
--    a Cartesian category is Symmetric Monoidal if its induced monoidal structure is symmetric

module Categories.Category.Cartesian.SymmetricMonoidal {o β„“ e} (π’ž : Category o β„“ e) (cartesian : Cartesian π’ž) where

open import Data.Product using (_,_)

open Category π’ž
open Commutation π’ž
open HomReasoning

open import Categories.Category.BinaryProducts π’ž using (module BinaryProducts)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Monoidal using (Monoidal)
import Categories.Category.Monoidal.Symmetric as Sym

open import Categories.NaturalTransformation using (ntHelper)

private
  variable
    W X Y Z : Obj

open Cartesian cartesian using (products)
open CartesianMonoidal cartesian using (monoidal)
open Sym monoidal using (Symmetric; symmetricHelper)
open Monoidal monoidal using (_βŠ—β‚€_; _βŠ—β‚_; module associator)
open BinaryProducts products

private
  B : βˆ€ {X Y} β†’ X βŠ—β‚€ Y β‡’ Y βŠ—β‚€ X
  B = swap

hexagon : [ (X βŠ—β‚€ Y) βŠ—β‚€ Z β‡’ Y βŠ—β‚€ Z βŠ—β‚€ X ]⟨
            B  βŠ—β‚ id                    β‡’βŸ¨ (Y βŠ—β‚€ X) βŠ—β‚€ Z ⟩
            associator.from             β‡’βŸ¨ Y βŠ—β‚€ X βŠ—β‚€ Z ⟩
            id βŠ—β‚ B
          β‰ˆ associator.from             β‡’βŸ¨ X βŠ—β‚€ Y βŠ—β‚€ Z ⟩
            B                           β‡’βŸ¨ (Y βŠ—β‚€ Z) βŠ—β‚€ X ⟩
            associator.from
          ⟩
hexagon = begin
      id βŠ—β‚ swap ∘ assocΛ‘ ∘ swap βŠ—β‚ id                        β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congΚ³ ⟨⟩∘ ⟩
      id βŠ—β‚ swap ∘ assocΛ‘ ∘ ⟨ ⟨ Ο€β‚‚ ∘ π₁ , π₁ ∘ π₁ ⟩ , id ∘ Ο€β‚‚ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ assocˑ∘⟨⟩ ⟩
      id βŠ—β‚ swap ∘ ⟨ Ο€β‚‚ ∘ π₁ , ⟨ π₁ ∘ π₁ , id ∘ Ο€β‚‚ ⟩ ⟩          β‰ˆβŸ¨ β‚βˆ˜βŸ¨βŸ© ⟩
      ⟨ id ∘ Ο€β‚‚ ∘ π₁ , swap ∘ ⟨ π₁ ∘ π₁ , id ∘ Ο€β‚‚ ⟩ ⟩           β‰ˆβŸ¨ ⟨⟩-congβ‚‚ identityΛ‘ swap∘⟨⟩ ⟩
      ⟨ Ο€β‚‚ ∘ π₁ , ⟨ id ∘ Ο€β‚‚ , π₁ ∘ π₁ ⟩ ⟩                       β‰ˆβŸ¨ ⟨⟩-congΛ‘ (⟨⟩-congΚ³ identityΛ‘) ⟩
      ⟨ Ο€β‚‚ ∘ π₁ , ⟨ Ο€β‚‚ , π₁ ∘ π₁ ⟩ ⟩                            β‰ˆΛ˜βŸ¨ assocˑ∘⟨⟩ ⟩
      assocΛ‘ ∘ ⟨ ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ , π₁ ∘ π₁ ⟩                   β‰ˆΛ˜βŸ¨ refl⟩∘⟨ swap∘⟨⟩ ⟩
      assocˑ ∘ swap ∘ assocˑ                                    ∎

symmetric : Symmetric
symmetric = symmetricHelper record
  { braiding    = record
    { F⇒G = ntHelper record
      { Ξ·       = Ξ» _ β†’ swap
      ; commute = Ξ» _ β†’ swapβˆ˜β‚
      }
    ; F⇐G = ntHelper record
      { Ξ·       = Ξ» _ β†’ swap
      ; commute = Ξ» _ β†’ swapβˆ˜β‚
      }
    ; iso = Ξ» _ β†’ record
      { isoˑ = swap∘swap
      ; isoʳ = swap∘swap
      }
    }
  ; commutative = swap∘swap
  ; hexagon     = hexagon
  }