Adjust universe levels

12 files changed, 118 insertions, 114 deletions

diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 46c4e18..77d6b72 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -2,20 +2,22 @@
 
 open import Level using (Level)
 
-module Data.Circuit {c ℓ : Level} where
+module Data.Circuit {ℓ : Level} where
 
 open import Data.Circuit.Gate using (Gates)
 
 import Data.List as List
-import Data.Hypergraph {c} {ℓ} Gates as Hypergraph
+import Data.Hypergraph {ℓ} Gates as Hypergraph
 
 open import Data.Fin using (Fin)
 open import Data.Nat using (ℕ)
-open import Function using (Func; _⟶ₛ_)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺)
+open import Function using (Func; _⟶ₛ_; _∘_)
+open import Relation.Binary using (Setoid)
 
 open Func
-open Hypergraph using (List∘Edgeₛ)
+
+open Hypergraph using (Multiset∘Edgeₛ)
 open Hypergraph
   using (_≈_ ; mk≈ ; module Edge)
   renaming
@@ -33,6 +35,8 @@ map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges)
 discrete : (n : ℕ) → Circuit n
 discrete n = mkCircuit []
 
+open Edge using (Edgeₛ)
+
 mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m
 mapₛ f .to = map f
-mapₛ f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edge.map f) x≈y)
+mapₛ {n} {m} f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edgeₛ n) (Edgeₛ m) (cong (Edge.mapₛ f)) x≈y)
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index ff92d0e..770c500 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -1,18 +1,18 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ)
 open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Level using (Level; 0ℓ)
 
-module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
+module Data.Hypergraph {ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.List.Relation.Binary.Pointwise as PW
 import Function.Reasoning as →-Reasoning
 import Relation.Binary.PropositionalEquality as ≡
-import Data.Hypergraph.Edge HL as Hyperedge
+import Data.Hypergraph.Edge {ℓ} HL as Hyperedge
 import Data.List.Relation.Binary.Permutation.Propositional as List-↭
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
 
 open import Data.List using (List; map)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-refl; ↭-sym; ↭-trans)
 open import Data.Nat using (ℕ)
 open import Data.String using (String; unlines)
 open import Function using (_∘_; _⟶ₛ_; Func)
@@ -22,13 +22,15 @@ module Edge = Hyperedge
 open Edge using (Edge; Edgeₛ)
 
 -- A hypergraph is a list of edges
-record Hypergraph (v : ℕ) : Set c where
+record Hypergraph (v : ℕ) : Set ℓ where
   constructor mkHypergraph
   field
     edges : List (Edge v)
 
 module _ {v : ℕ} where
 
+  open ↭ (Edgeₛ v) using (_↭_; ↭-refl; ↭-sym; ↭-trans)
+
   show : Hypergraph v → String
   show (mkHypergraph e) = unlines (map Edge.show e)
 
@@ -55,7 +57,7 @@ module _ {v : ℕ} where
   ≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂)
 
 -- The setoid of labeled hypergraphs with v nodes
-Hypergraphₛ : ℕ → Setoid c ℓ
+Hypergraphₛ : ℕ → Setoid ℓ ℓ
 Hypergraphₛ v = record
     { Carrier = Hypergraph v
     ; _≈_ = _≈_
@@ -68,15 +70,11 @@ Hypergraphₛ v = record
 
 open Func
 
-List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
-List∘Edgeₛ = PW.setoid ∘ Edgeₛ
+open ↭ using (↭-setoid)
+
+Multiset∘Edgeₛ : (n : ℕ) → Setoid ℓ ℓ
+Multiset∘Edgeₛ = ↭-setoid ∘ Edgeₛ
 
-mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
+mkHypergraphₛ : {n : ℕ} → Multiset∘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
+mkHypergraphₛ {n} .cong = mk≈
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 1e24559..5c22a04 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -2,7 +2,8 @@
 
 open import Data.Hypergraph.Label using (HypergraphLabel)
 
-module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+open import Level using (Level; 0ℓ)
+module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.Vec as Vec
 import Data.Vec.Relation.Binary.Equality.Cast as VecCast
@@ -15,13 +16,15 @@ open import Data.String using (String; _<+>_)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
 open import Relation.Binary using (Setoid; IsEquivalence)
+open import Function using (_⟶ₛ_; Func)
 
 module HL = HypergraphLabel HL
 
 open HL using (Label; cast; cast-is-id)
 open Vec using (Vec)
+open Func
 
-record Edge (v : ℕ) : Set where
+record Edge (v : ℕ) : Set ℓ where
   constructor mkEdge
   field
     {arity} : ℕ
@@ -42,7 +45,7 @@ open VecCast using (_≈[_]_)
 module _ {v : ℕ} where
 
   -- an equivalence relation on edges with v nodes
-  record _≈_ (E E′ : Edge v) : Set where
+  record _≈_ (E E′ : Edge v) : Set ℓ where
     constructor mk≈
     module E = Edge E
     module E′ = Edge E′
@@ -92,5 +95,9 @@ module _ {v : ℕ} where
     rewrite cast-is-id ≡.refl l
     rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
 
-Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
+Edgeₛ : (v : ℕ) → Setoid ℓ ℓ
 Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} }
+
+mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
+mapₛ f .to = map f
+mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (VecCast.≈-cong′ (Vec.map f) ≡p)
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
index c23d33a..ca95002 100644
--- a/Data/Hypergraph/Label.agda
+++ b/Data/Hypergraph/Label.agda
@@ -4,22 +4,22 @@ module Data.Hypergraph.Label where
 open import Data.Castable using (IsCastable)
 open import Data.Nat.Base using (ℕ)
 open import Data.String using (String)
-open import Level using (Level; suc)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary using (Rel; IsDecTotalOrder)
 open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
 open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 
-record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+record HypergraphLabel : Set₁ where
 
   field
-    Label : ℕ → Set ℓ
+    Label : ℕ → Set
     showLabel : (n : ℕ) → Label n → String
     isCastable : IsCastable Label
-    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    _[_≤_] : (n : ℕ) → Rel (Label n) 0ℓ
     isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
 
-  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+  decTotalOrder : (n : ℕ) → DecTotalOrder 0ℓ 0ℓ 0ℓ
   decTotalOrder n = record
       { Carrier = Label n
       ; _≈_ = _≡_
@@ -27,10 +27,10 @@ record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
       ; isDecTotalOrder = isDecTotalOrder n
       }
 
-  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+  _[_<_] : (n : ℕ) → Rel (Label n) 0ℓ
   _[_<_] n =  _<_ (decTotalOrder n)
 
-  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+  strictTotalOrder : (n : ℕ) → StrictTotalOrder 0ℓ 0ℓ 0ℓ
   strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
 
   open IsCastable isCastable public
diff --git a/Data/System.agda b/Data/System.agda
index 0361369..cecdfcd 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
-
+open import Level using (Level; 0ℓ; suc)
 module Data.System {ℓ : Level} where
 
 import Function.Construct.Identity as Id
@@ -11,7 +10,7 @@ open import Data.Circuit.Value using (Value)
 open import Data.Nat.Base using (ℕ)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
 open import Data.System.Values Value using (Values; _≋_; module ≋)
-open import Level using (Level; _⊔_; 0ℓ; suc)
+open import Level using (Level; 0ℓ; suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid)
 open import Function.Base using (_∘_)
@@ -20,10 +19,10 @@ open import Function.Construct.Setoid using (_∙_)
 
 open Func
 
-record System (n : ℕ) : Set (suc ℓ) where
+record System (n : ℕ) : Set₁ where
 
   field
-    S : Setoid ℓ ℓ
+    S : Setoid 0ℓ 0ℓ
     fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
     fₒ : ∣ S ⇒ₛ Values n ∣
 
@@ -66,7 +65,7 @@ module _ {n : ℕ} where
   ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s))
   ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s))
 
-  System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
+  System-Preorder : Preorder (suc 0ℓ) (suc 0ℓ) ℓ
   System-Preorder = record
       { Carrier = System n
       ; _≈_ = _≡_
@@ -82,5 +81,5 @@ module _ (n : ℕ) where
 
   open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
 
-  Systemₛ : Setoid (suc ℓ) ℓ
+  Systemₛ : Setoid (suc 0ℓ) ℓ
   Systemₛ = InducedEquivalence
diff --git a/DecorationFunctor/Hypergraph/Labeled.agda b/DecorationFunctor/Hypergraph/Labeled.agda
index 083ff80..33a7a89 100644
--- a/DecorationFunctor/Hypergraph/Labeled.agda
+++ b/DecorationFunctor/Hypergraph/Labeled.agda
@@ -1,6 +1,8 @@
 {-# OPTIONS --without-K --safe #-}
 
-module DecorationFunctor.Hypergraph.Labeled where
+open import Level using (Level; 0ℓ; lift)
+
+module DecorationFunctor.Hypergraph.Labeled {c ℓ : Level} where
 
 import Categories.Morphism as Morphism
 
@@ -37,32 +39,30 @@ open import Data.Fin.Properties
     )
 open import Data.Nat using (ℕ; _+_)
 open import Data.Product.Base using (_,_; Σ)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_])
 open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive)
-open import Data.Unit using (tt)
 open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid)
 
 open import Function.Base using (_∘_; id; const; case_of_; case_returning_of_)
-open import Function.Bundles using (Func; Inverse; _↔_; mk↔)
+open import Function.Bundles using (Func; Inverse; _↔_; mk↔; _⟶ₛ_)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
 
-open import Level using (0ℓ; lift)
-
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality using (_≗_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app)
 open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong; dcong₂; subst-∘; subst-subst; sym-cong; subst-subst-sym; trans-cong; cong-∘; trans-reflʳ)
 open import Relation.Nullary.Negation.Core using (¬_)
 
-open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open Cartesian (Setoids-Cartesian {c} {ℓ}) using (products)
 open Cocartesian Nat-Cocartesian using (coproducts)
 open FinitelyCocompleteCategory Nat-FinitelyCocomplete
     using ()
     renaming (symmetricMonoidalCategory to Nat-smc)
-open Morphism (Setoids 0ℓ 0ℓ) using (_≅_)
+open import Category.Monoidal.Instance.Nat using (Nat,+,0)
+open Morphism (Setoids c ℓ) using (_≅_)
 open Lax using (SymmetricMonoidalFunctor)
 
 open BinaryProducts products using (-×-)
@@ -70,7 +70,7 @@ open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc)
 
 open import Data.Circuit.Gate using (Gate; cast-gate; cast-gate-trans; cast-gate-is-id; subst-is-cast-gate)
 
-record Hypergraph (v : ℕ) : Set where
+record Hypergraph (v : ℕ) : Set c where
 
   field
     h : ℕ
@@ -78,7 +78,7 @@ record Hypergraph (v : ℕ) : Set where
     j : (e : Fin h) → Fin (a e) → Fin v
     l : (e : Fin h) → Gate (a e)
 
-record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where
+record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set ℓ where
 
   open Hypergraph H public
   open Hypergraph H′ renaming (h to h′; a to a′; j to j′; l to l′) public
@@ -183,7 +183,7 @@ Hypergraph-same-trans ≡H₁ ≡H₂ = record
     ≗l₂ : (e : Fin (h ≡H₁)) → cast-gate _ (l′ ≡H₁ (to ≡H₁ e)) ≡ cast-gate _ (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e)))
     ≗l₂ e = trans (cong (cast-gate _) (≗l ≡H₂ (to ≡H₁ e))) (cast-gate-trans _ (sym (≗a ≡H₁ e)) (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e))))
 
-Hypergraph-setoid : ℕ → Setoid 0ℓ 0ℓ
+Hypergraph-setoid : ℕ → Setoid c ℓ
 Hypergraph-setoid p = record
     { Carrier = Hypergraph p
     ; _≈_ = Hypergraph-same
@@ -217,7 +217,7 @@ Hypergraph-same-cong f ≡H = record
   where
     open Hypergraph-same ≡H
 
-Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraph-setoid n) (Hypergraph-setoid m)
+Hypergraph-Func : (Fin n → Fin m) → Hypergraph-setoid n ⟶ₛ Hypergraph-setoid m
 Hypergraph-Func f = record
     { to = map-nodes f
     ; cong = Hypergraph-same-cong f
@@ -249,9 +249,9 @@ homomorphism {n} {m} {o} {H} f g = record
   where
     open Hypergraph-same Hypergraph-same-refl
 
-F : Functor Nat (Setoids 0ℓ 0ℓ)
+F : Functor Nat (Setoids c ℓ)
 F = record
-    { F₀ = Hypergraph-setoid
+    { F₀ = λ n → Hypergraph-setoid n
     ; F₁ = Hypergraph-Func
     ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} }
     ; homomorphism = λ { {f = f} {g = g} → homomorphism f g }
@@ -268,7 +268,7 @@ empty-hypergraph = record
     ; l = λ ()
     }
 
-ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Hypergraph-setoid 0)
+ε : SingletonSetoid {c} {ℓ} ⟶ₛ Hypergraph-setoid 0
 ε = record
     { to = const empty-hypergraph
     ; cong = const Hypergraph-same-refl
@@ -430,7 +430,7 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record
     ; sym-commute = λ { (f , g) {H₁ , H₂} → Hypergraph-same-sym (commute {H₁ = H₁} {H₂ = H₂} f g) }
     }
   where
-    η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m))
+    η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m)
     η = record
         { to = λ { (H₁ , H₂) → together H₁ H₂ }
         ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
@@ -551,7 +551,7 @@ n+0↔n n = record
     to∘from : (x : Fin n) → to (from x) ≡ x
     to∘from x rewrite splitAt-↑ˡ n x 0 = refl
 
-unitaryʳ : Hypergraph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H
+unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H
 unitaryʳ {n} {H} = record
     { ↔h = h+0↔h
     ; ≗a = ≗a
@@ -658,8 +658,8 @@ braiding {n} {m} {H₁} {H₂} = record
     ≗l e | inj₁ e₁ rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = sym (cast-gate-is-id refl (H₁.l e₁))
     ≗l e | inj₂ e₂ rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = sym (cast-gate-is-id refl (H₂.l e₂))
 
-hypergraph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ})
-hypergraph = record
+Circ : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
+Circ = record
     { F = F
     ; isBraidedMonoidal = record
         { isMonoidal = record
@@ -676,20 +676,20 @@ hypergraph = record
         }
     }
   where
-    η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m))
+    η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m)
     η = record
         { to = λ { (H₁ , H₂) → together H₁ H₂ }
         ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
         }
 
-module F = SymmetricMonoidalFunctor hypergraph
+module F = SymmetricMonoidalFunctor Circ
 
 open Gate
 
-and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3)
+and-gate : SingletonSetoid {c} {ℓ} ⟶ₛ F.₀ 3
 and-gate = record
-    { to = λ { (lift tt) → and-graph }
-    ; cong = λ { (lift tt) → Hypergraph-same-refl }
+    { to = λ _ → and-graph
+    ; cong = λ _ → Hypergraph-same-refl
     }
   where
     and-graph : Hypergraph 3
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)
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index f8d47c2..5de8f84 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -1,8 +1,9 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Level using (Level; 0ℓ)
 
-module Functor.Instance.Nat.Edge (HL : HypergraphLabel) where
+module Functor.Instance.Nat.Edge {ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.Vec as Vec
 import Data.Vec.Properties as VecProps
@@ -11,10 +12,9 @@ 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ₛ; map; _≈_)
+open import Data.Hypergraph.Edge {ℓ} HL as Edge using (Edgeₛ; map; mapₛ; _≈_)
 open import Data.Nat using (ℕ)
-open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive)
-open import Level using (0ℓ)
+open import Data.Vec.Relation.Binary.Equality.Cast using (≈-reflexive)
 open import Function using (id; _∘_; Func; _⟶ₛ_)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
@@ -26,14 +26,6 @@ open Edge._≈_
 open Func
 open Functor
 
-Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
-Edge₁ f .to = map f
-Edge₁ f .cong x≈y = record
-    { ≡arity = ≡arity x≈y
-    ; ≡label = ≡label x≈y
-    ; ≡ports = ≈-cong′ (Vec.map f) (≡ports x≈y)
-    }
-
 map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e
 map-id .≡arity = ≡.refl
 map-id .≡label = HL.≈-reflexive ≡.refl
@@ -59,9 +51,9 @@ map-resp-≗ f≗g .≡arity = ≡.refl
 map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl
 map-resp-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e))
 
-Edge : Functor Nat (Setoids 0ℓ 0ℓ)
+Edge : Functor Nat (Setoids ℓ ℓ)
 Edge .F₀ = Edgeₛ
-Edge .F₁ = Edge₁
+Edge .F₁ = mapₛ
 Edge .identity = map-id
 Edge .homomorphism = map-∘ _ _
 Edge .F-resp-≈ = map-resp-≗
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
index 730f90d..00451ad 100644
--- a/Functor/Instance/Nat/System.agda
+++ b/Functor/Instance/Nat/System.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Functor.Instance.Nat.System {ℓ} where
+module Functor.Instance.Nat.System where
 
+open import Level using (suc; 0ℓ)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor.Core using (Functor)
@@ -9,14 +10,13 @@ open import Data.Circuit.Value using (Value)
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_,_; _×_)
-open import Data.System using (System; ≤-System; Systemₛ)
+open import Data.System {suc 0ℓ} using (System; ≤-System; Systemₛ)
 open import Data.System.Values Value using (module ≋)
 open import Function.Bundles using (Func; _⟶ₛ_)
 open import Function.Base using (id; _∘_)
 open import Function.Construct.Setoid using (_∙_)
 open import Functor.Instance.Nat.Pull using (Pull₁; Pull-resp-≈)
 open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomorphism; Push-resp-≈)
-open import Level using (suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
 -- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
@@ -29,7 +29,7 @@ open Functor
 private
   variable A B C : ℕ
 
-map : (Fin A → Fin B) → System {ℓ} A → System B
+map : (Fin A → Fin B) → System A → System B
 map f X = record
     { S = S
     ; fₛ = fₛ ∙ Pull₁ f
@@ -88,7 +88,7 @@ System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f
     both f≗g .≗-fₛ i s = cong fₛ (Pull-resp-≈ f≗g {i})
     both {f} {g} f≗g .≗-fₒ s = Push-resp-≈ f≗g
 
-Sys : Functor Nat (Setoids (suc ℓ) ℓ)
+Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ))
 Sys .F₀ = Systemₛ
 Sys .F₁ = System₁
 Sys .identity = id-x≤x , x≤id-x
diff --git a/Functor/Monoidal/Construction/ListOf.agda b/Functor/Monoidal/Construction/ListOf.agda
index 476939e..23c6ba8 100644
--- a/Functor/Monoidal/Construction/ListOf.agda
+++ b/Functor/Monoidal/Construction/ListOf.agda
@@ -8,9 +8,9 @@ open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
 open import Level using (Level)
 
 module Functor.Monoidal.Construction.ListOf
-    {o ℓ e : Level}
+    {o o′ ℓ ℓ′ e e′ : Level}
     {𝒞 : CocartesianCategory o ℓ e}
-    {S : MonoidalCategory o ℓ e}
+    {S : MonoidalCategory o′ ℓ′ e′}
     (let module 𝒞 = CocartesianCategory 𝒞)
     (let module S = MonoidalCategory S)
     (G : Functor 𝒞.U S.U)
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda
index 6862b84..eca7b3a 100644
--- a/Functor/Monoidal/Construction/MultisetOf.agda
+++ b/Functor/Monoidal/Construction/MultisetOf.agda
@@ -10,9 +10,9 @@ open import Category.Construction.CMonoids using (CMonoids)
 open import Level using (Level)
 
 module Functor.Monoidal.Construction.MultisetOf
-    {o ℓ e : Level}
+    {o o′ ℓ ℓ′ e e′ : Level}
     {𝒞 : CocartesianCategory o ℓ e}
-    {S : SymmetricMonoidalCategory o ℓ e}
+    {S : SymmetricMonoidalCategory o′ ℓ′ e′}
     (let module 𝒞 = CocartesianCategory 𝒞)
     (let module S = SymmetricMonoidalCategory S)
     (G : Functor 𝒞.U S.U)
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
index 1b3bb34..d86588f 100644
--- a/Functor/Monoidal/Instance/Nat/System.agda
+++ b/Functor/Monoidal/Instance/Nat/System.agda
@@ -1,25 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; suc)
-
-module Functor.Monoidal.Instance.Nat.System {ℓ : Level} where
+module Functor.Monoidal.Instance.Nat.System where
 
 open import Function.Construct.Identity using () renaming (function to Id)
 import Function.Construct.Constant as Const
 
+open import Level using (0ℓ; suc; Level)
+
 open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0)
 open import Categories.Category.Instance.Nat using (Natop)
-open import Category.Instance.Setoids.SymmetricMonoidal {suc ℓ} {ℓ} using (Setoids-×)
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
 open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Data.Circuit.Value using (Value)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
-open import Data.System {ℓ} using (Systemₛ; System; ≤-System)
+open import Data.System {suc 0ℓ} using (Systemₛ; System; ≤-System)
 open import Data.System.Values Value using (Values; _≋_; module ≋)
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Data.Vec.Functional using ([])
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
-open import Functor.Instance.Nat.System {ℓ} using (Sys; map)
+open import Functor.Instance.Nat.System using (Sys; map)
 open import Function.Base using (_∘_)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Function.Construct.Setoid using (setoid)
@@ -36,12 +36,12 @@ module _ where
   discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid)
   discrete .fₒ = Const.function SingletonSetoid (Values 0) []
 
-Sys-ε : SingletonSetoid {suc ℓ} {ℓ} ⟶ₛ Systemₛ 0
+Sys-ε : SingletonSetoid {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0
 Sys-ε = Const.function SingletonSetoid (Systemₛ 0) discrete
 
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open Cartesian (Setoids-Cartesian {suc ℓ} {ℓ}) using (products)
+open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open BinaryProducts products using (-×-)
 open import Categories.Functor using (_∘F_)
@@ -216,12 +216,14 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
   where
     open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
     open BinaryProducts 0ℓ-products using (assocˡ)
-    open Cartesian (Setoids-Cartesian {ℓ} {ℓ}) using () renaming (products to prod)
+    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
     open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ)
     module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
+    Pull,++,[]B : BraidedMonoidalFunctor
+    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
     module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
 
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (associativity-inv)
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (associativity-inv)
 
     module X = System X
     module Y = System Y
@@ -238,7 +240,7 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
     ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
     }
   where
-    open Cartesian (Setoids-Cartesian {ℓ} {ℓ}) using () renaming (products to prod)
+    open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
     open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ)
     open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
     open BinaryProducts 0ℓ-products using (×-assoc; assocˡ; assocʳ)
@@ -323,7 +325,7 @@ Sys-unitaryʳ-≥ {n} X = record
     { ⇒S = < Id X.S , Const.function X.S SingletonSetoid tt >ₛ
     ; ≗-fₛ = λ i s →
         cong
-            (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {ℓ} {ℓ})) ∙ Id (Values n) ×-function ε⇒)
+            (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {suc 0ℓ} {0ℓ})) ∙ Id (Values n) ×-function ε⇒)
             sym-split-unitaryʳ
             {s , tt}
     ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt}
@@ -371,8 +373,9 @@ Sys-braiding-compat-≤ {n} {m} X Y = record
     module X = System X
     module Y = System Y
     module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
-    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (braiding-compat-inv)
+    Pull,++,[]B : BraidedMonoidalFunctor
+    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
     open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
     module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]
 
@@ -389,8 +392,9 @@ Sys-braiding-compat-≥ {n} {m} X Y = record
     module X = System X
     module Y = System Y
     module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
-    module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
-    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[].braidedMonoidalFunctor using (braiding-compat-inv)
+    Pull,++,[]B : BraidedMonoidalFunctor
+    Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
+    open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
     open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax)
     module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[]