Add Circ functormain

1 files changed, 32 insertions, 0 deletions

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)