Data/WiringDiagram/Monoidal/Symmetric.agda


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

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

open import Categories.Category using (Category)
open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
open import Level using (Level)

module Data.WiringDiagram.Monoidal.Symmetric
    {o ℓ e : Level}
    {𝒞 : Category o ℓ e}
    (S : SemiadditiveDagger 𝒞)
  where

open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Data.WiringDiagram.Monoidal.Braided S using (swap∘swap-⧈; DWD-Braided; BWD-Braided)
open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal)

DWD-Symmetric : Symmetric DWD-Monoidal
DWD-Symmetric = record
    { braided = DWD-Braided
    ; commutative = swap∘swap-⧈
    }

BWD-Symmetric : Symmetric BWD-Monoidal
BWD-Symmetric = record
    { braided = BWD-Braided
    ; commutative = swap∘swap-⧈
    }