diff options
Diffstat (limited to 'Functor/Instance/Nat/Circ.agda')
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 32 |
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) |