Adjust universe levels

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)