{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Cartesian using (Cartesian)
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
}