From b2b2bdaa75406451174f0873cfd355e7511abd9a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Nov 2025 08:17:33 -0600
Subject: Add Circ symmetric monoidal functor

---
 Functor/Monoidal/Instance/Nat/Circ.agda | 87 +++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 Functor/Monoidal/Instance/Nat/Circ.agda

diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda
new file mode 100644
index 0000000..9d38127
--- /dev/null
+++ b/Functor/Monoidal/Instance/Nat/Circ.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; 0ℓ; suc)
+
+module Functor.Monoidal.Instance.Nat.Circ where
+
+import Categories.Object.Monoid as MonoidObject
+import Data.Permutation.Sort as ↭-Sort
+import Function.Reasoning as →-Reasoning
+
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+open import Category.Monoidal.Instance.Nat using (Nat,+,0)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Cartesian using (Cartesian)
+open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Functor using (_∘F_)
+open BinaryProducts products using (-×-)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Functor using (Functor)
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Circuit using (Circuit; Circuitₛ; mkCircuit; mkCircuitₛ; _≈_; mk≈; map)
+open import Data.Circuit.Gate using (Gates)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function using (_⟶ₛ_; Func; _⟨$⟩_; _∘_; id)
+open import Functor.Instance.Nat.Circ {suc 0ℓ} using (Circ; module Multiset∘Edge)
+open import Functor.Instance.Nat.Edge {suc 0ℓ} using (Edge)
+open import Function.Construct.Setoid using (_∙_)
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
+open import Functor.Instance.FreeCMonoid {suc 0ℓ} {suc 0ℓ} using (FreeCMonoid)
+
+Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ
+Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian }
+
+open import Functor.Monoidal.Construction.MultisetOf
+     {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (BagOf,++,[])
+
+open Lax using (SymmetricMonoidalFunctor)
+
+module BagOf,++,[] = SymmetricMonoidalFunctor BagOf,++,[]
+
+open SymmetricMonoidalFunctor
+
+ε⇒ : SingletonSetoid ⟶ₛ Circuitₛ 0
+ε⇒ = mkCircuitₛ ∙ BagOf,++,[].ε
+
+open Cocartesian Nat-Cocartesian using (-+-)
+
+open Func
+
+η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m)
+η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (BagOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y))
+η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (BagOf,++,[].⊗-homo.η (n , m)) (x , y))
+
+⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-)
+⊗-homomorphism = ntHelper record
+    { η = λ (n , m) → η {n} {m}
+    ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (BagOf,++,[].⊗-homo.commute (f , g) {X , Y}) }
+    }
+
+Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
+Circ,⊗,ε .F = Circ
+Circ,⊗,ε .isBraidedMonoidal = record
+    { isMonoidal = record
+        { ε = ε⇒
+        ; ⊗-homo = ⊗-homomorphism
+        ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} →
+                  mk≈ (BagOf,++,[].associativity {n} {m} {o} {(x , y) , z}) }
+        ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (BagOf,++,[].unitaryˡ {n} {_ , x}) }
+        ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (BagOf,++,[].unitaryʳ {n} {x , _}) }
+        }
+    ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} →
+        mk≈ (BagOf,++,[].braiding-compat {n} {m} {x , y}) }
+    }
-- 
cgit v1.2.3