Add Circ functormain

5 files changed, 69 insertions, 12 deletions

diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 0be86f9..09dfb2e 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -12,15 +12,16 @@ open import Data.Fin using (Fin)
 open import Data.Hypergraph {c} {ℓ} Gates
   using
     ( Hypergraph
-    ; mkHypergraph
     ; Hypergraphₛ
+    ; mkHypergraphₛ
+    ; List∘Edgeₛ
     ; module Edge
-    ; normalize
+    ; mkHypergraph
     ; _≈_
     ; mk≈
     )
 open import Data.Nat using (ℕ)
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary using (Setoid)
 open import Function.Bundles using (Func; _⟶ₛ_)
 
 open List using (List)
@@ -35,6 +36,9 @@ map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges)
 Circuitₛ : ℕ → Setoid c (c ⊔ ℓ)
 Circuitₛ = Hypergraphₛ
 
+mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n
+mkCircuitₛ = mkHypergraphₛ
+
 open Func
 open Edge.Sort using (sort)
 
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index 2e8498c..18a259b 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -6,9 +6,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel)
 
 module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
 
+import Data.List.Relation.Binary.Pointwise as PW
+import Data.Hypergraph.Edge HL as HypergraphEdge
+import Function.Reasoning as →-Reasoning
+import Relation.Binary.PropositionalEquality as ≡
+
 open import Data.Hypergraph.Base {c} HL public
 open import Data.Hypergraph.Setoid {c} {ℓ} HL public
-
-import Data.Hypergraph.Edge HL as HypergraphEdge
+open import Data.Nat using (ℕ)
+open import Function using (_∘_; _⟶ₛ_; Func)
+open import Level using (0ℓ)
+open import Relation.Binary using (Setoid)
 
 module Edge = HypergraphEdge
+
+open Edge using (Edgeₛ; ≈-Edge⇒≡)
+open Func
+
+List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
+List∘Edgeₛ = PW.setoid ∘ Edgeₛ
+
+mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
+mkHypergraphₛ .to = mkHypergraph
+mkHypergraphₛ {n} .cong ≋-edges = ≋-edges
+    |> PW.map ≈-Edge⇒≡
+    |> PW.Pointwise-≡⇒≡
+    |> ≡.cong mkHypergraph
+    |> Setoid.reflexive (Hypergraphₛ n)
+  where
+    open →-Reasoning
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 7d0fa7c..ee32393 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -25,8 +25,7 @@ open import Data.String using (String; _<+>_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
-open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
-open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence)
 open import Relation.Nullary using (¬_)
 
 
@@ -89,7 +88,6 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
     module i≈j = ≈-Edge i≈j
     module j≈k = ≈-Edge j≈k
 
-open import Relation.Binary using (IsEquivalence)
 ≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
 ≈-Edge-IsEquivalence = record
     { refl = ≈-Edge-refl
@@ -345,3 +343,6 @@ open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) publ
 
 module Sort {v} = ListSort (decTotalOrder {v})
 open Sort using (sort) public
+
+Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
+Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} }
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
new file mode 100644
index 0000000..0f18c4c
--- /dev/null
+++ b/Functor/Instance/Nat/Circ.agda
@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; 0ℓ)
+
+module Functor.Instance.Nat.Circ {c ℓ : Level} where
+
+open import Data.Circuit {c} {ℓ} 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)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Data.Fin using (Fin)
+open import Data.Circuit.Gate using (Gates)
+open import Functor.Instance.Nat.Edge Gates using (Edge)
+open import Functor.Instance.List using (List)
+
+List∘Edge : Functor Nat (Setoids 0ℓ 0ℓ)
+List∘Edge = List ∘F Edge
+
+module List∘Edge = Functor List∘Edge
+
+open Func
+open Functor
+
+Circ : Functor Nat (Setoids c (c ⊔ ℓ))
+Circ .F₀ = Circuitₛ
+Circ .F₁ = mapₛ
+Circ .identity = cong mkCircuitₛ List∘Edge.identity
+Circ .homomorphism = cong mkCircuitₛ List∘Edge.homomorphism
+Circ .F-resp-≈ f≗g = cong mkCircuitₛ (List∘Edge.F-resp-≈ f≗g)
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index ee54f2e..618807d 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -11,7 +11,7 @@ open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge)
+open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ)
 open import Data.Nat using (ℕ)
 open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive)
 open import Level using (0ℓ)
@@ -27,9 +27,6 @@ open Functor
 open Setoid
 open ≈-Edge
 
-Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
-Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} }
-
 Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
 Edge₁ f .to = map f
 Edge₁ f .cong x≈y = record