Redefine circuit functor

1 files changed, 44 insertions, 20 deletions

diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
index 36d726d..88a6ec6 100644
--- a/Functor/Instance/Nat/Circ.agda
+++ b/Functor/Instance/Nat/Circ.agda
@@ -1,32 +1,56 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; _⊔_; 0ℓ)
+open import Level using (Level)
 
 module Functor.Instance.Nat.Circ {ℓ : Level} where
 
-open import Data.Circuit {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ)
-open import Data.Nat using (ℕ)
-open import Relation.Binary using (Setoid)
-open import Function using (Func)
-open import Categories.Functor using (Functor; _∘F_)
-open import Categories.Category.Instance.Setoids using (Setoids)
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
+
 open import Categories.Category.Instance.Nat using (Nat)
-open import Data.Fin using (Fin)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×)
+open import Data.Circuit using (mk≈)
+open import Data.Circuit {ℓ} using (Circuitₛ; mkCircuitₛ; edgesₛ)
 open import Data.Circuit.Gate using (Gates)
+open import Data.Nat using (ℕ)
+open import Data.Opaque.Multiset using (Multisetₛ)
+open import Data.Product using (proj₁; proj₂; Σ-syntax)
+open import Functor.Free.Instance.CMonoid using (Free)
 open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge)
-open import Functor.Instance.Multiset using (Multiset)
+open import Functor.Properties using (define-by-pw-iso)
+
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Category.Construction.CMonoids.Properties Setoids-×.symmetric using (transport-by-iso)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid)
+
+Edges : Functor Nat CMonoids
+Edges = Free ∘F Edge
+
+module Edges = Functor Edges
+module Edge = Functor Edge
+
+opaque
+  unfolding Multisetₛ
+  Edges≅Circₛ : (n : ℕ) → Setoids-×.U [ Multisetₛ (Edge.₀ n) ≅ Circuitₛ n ]
+  Edges≅Circₛ n = record
+      { from = mkCircuitₛ
+      ; to = edgesₛ
+      ; iso = record
+          { isoˡ = ↭.↭-refl (Edge.₀ n)
+          ; isoʳ = mk≈ (↭.↭-refl (Edge.₀ n))
+          }
+      }
 
-Multiset∘Edge : Functor Nat (Setoids ℓ ℓ)
-Multiset∘Edge = Multiset ∘F Edge
+private
+  Edges≅ : (n : ℕ) → Σ[ M ∈ CommutativeMonoid ] CMonoids [ Edges.₀ n ≅ M ]
+  Edges≅ n = transport-by-iso (Edges.₀ n) (Edges≅Circₛ n)
 
-module Multiset∘Edge = Functor Multiset∘Edge
+Circuitₘ : ℕ → CommutativeMonoid
+Circuitₘ n = proj₁ (Edges≅ n)
 
-open Func
-open Functor
+Edges≅Circₘ : (n : ℕ) → CMonoids [ Edges.₀ n ≅ Circuitₘ n ]
+Edges≅Circₘ n = proj₂ (Edges≅ n)
 
-Circ : Functor Nat (Setoids ℓ ℓ)
-Circ .F₀ = Circuitₛ
-Circ .F₁ = mapₛ
-Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity
-Circ .homomorphism {f = f} {g = g} = cong mkCircuitₛ (Multiset∘Edge.homomorphism {f = f} {g = g})
-Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g)
+Circ : Functor Nat CMonoids
+Circ = proj₁ (define-by-pw-iso Edges Circuitₘ Edges≅Circₘ)