diff options
Diffstat (limited to 'Functor/Instance/Nat/Circ.agda')
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda index d5bcc9b..09bc495 100644 --- a/Functor/Instance/Nat/Circ.agda +++ b/Functor/Instance/Nat/Circ.agda @@ -2,9 +2,9 @@ open import Level using (Level; _⊔_; 0ℓ) -module Functor.Instance.Nat.Circ {c ℓ : Level} where +module Functor.Instance.Nat.Circ {ℓ : Level} where -open import Data.Circuit {c} {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ) +open import Data.Circuit {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ) open import Data.Nat using (ℕ) open import Relation.Binary using (Setoid) open import Function using (Func) @@ -13,20 +13,20 @@ 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) +open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge) +open import Functor.Instance.Multiset using (Multiset) -List∘Edge : Functor Nat (Setoids 0ℓ 0ℓ) -List∘Edge = List ∘F Edge +Multiset∘Edge : Functor Nat (Setoids ℓ ℓ) +Multiset∘Edge = Multiset ∘F Edge -module List∘Edge = Functor List∘Edge +module Multiset∘Edge = Functor Multiset∘Edge open Func open Functor -Circ : Functor Nat (Setoids c ℓ) +Circ : Functor Nat (Setoids ℓ ℓ) 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) +Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity +Circ .homomorphism = cong mkCircuitₛ Multiset∘Edge.homomorphism +Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g) |