Redefine circuit functor

2 files changed, 121 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ₘ)
diff --git a/Functor/Properties.agda b/Functor/Properties.agda
new file mode 100644
index 0000000..1bd3ba6
--- /dev/null
+++ b/Functor/Properties.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Properties where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category using (Category; _[_,_])
+open import Level using (Level)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Categories.Morphism using (_≅_)
+open import Categories.Functor using (Functor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Data.Product using (Σ-syntax; _,_)
+
+module _
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    {𝒟 : Category o′ ℓ′ e′}
+  where
+
+  module 𝒞 = Category 𝒞
+  module 𝒟 = Category 𝒟
+
+  define-by-pw-iso
+      : (F : Functor 𝒞 𝒟)
+        (G₀ : 𝒞.Obj → 𝒟.Obj)
+      → (let module F = Functor F)
+      → ((X : 𝒞.Obj) → 𝒟 [ F.₀ X ≅ G₀ X ])
+      → Σ[ G ∈ Functor 𝒞 𝒟 ] F ≃ G
+  define-by-pw-iso F G₀ α = G , F≃G
+    where
+      open Functor
+      module F = Functor F
+      open 𝒟
+      open _≅_
+      open HomReasoning
+      open ⇒-Reasoning 𝒟
+
+      G-homo
+          : {X Y Z : 𝒞.Obj}
+          → (f : 𝒞 [ X , Y ])
+          → (g : 𝒞 [ Y , Z ])
+          → from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X)
+          ≈ (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X)
+      G-homo {X} {Y} {Z} f g = begin
+          from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X)                           ≈⟨ extendʳ (pushʳ F.homomorphism) ⟩
+          (from (α Z) ∘ F.₁ g) ∘ F.₁ f ∘ to (α X)                         ≈⟨ extendˡ (pushˡ (insertʳ (isoˡ (α Y)))) ⟩
+          (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) ∎
+
+      G-resp-≈
+        : {X Y : 𝒞.Obj}
+        → {f g : 𝒞 [ X , Y ]}
+        → f 𝒞.≈ g
+        → from (α Y) ∘ F.₁ f ∘ to (α X)
+        ≈ from (α Y) ∘ F.₁ g ∘ to (α X)
+      G-resp-≈ f≈g = refl⟩∘⟨ F.F-resp-≈ f≈g ⟩∘⟨refl
+
+      G-identity : {X : 𝒞.Obj} → from (α X) ∘ F.₁ 𝒞.id ∘ to (α X) ≈ id
+      G-identity {X} = refl⟩∘⟨ (F.identity ⟩∘⟨refl ○ identityˡ) ○ isoʳ (α X)
+
+      G : Functor 𝒞 𝒟
+      G .F₀ = G₀
+      G .F₁ {X} {Y} f = from (α Y) ∘ F.₁ f ∘ to (α X)
+      G .identity {X} = G-identity
+      G .homomorphism {f = f} {g} = G-homo f g
+      G .F-resp-≈ = G-resp-≈
+
+      commute : {X Y : 𝒞.Obj} (f : 𝒞 [ X , Y ]) → from (α Y) ∘ F.F₁ f ≈ (from (α Y) ∘ F.₁ f ∘ to (α X)) ∘ from (α X)
+      commute {X} {Y} f = pushʳ (insertʳ (isoˡ (α X)))
+
+      F≃G : F ≃ G
+      F≃G = niHelper record
+          { η = λ X → from (α X)
+          ; η⁻¹ = λ X → to (α X)
+          ; commute = commute
+          ; iso = λ X → iso (α X)
+          }