Adjust universe levels

3 files changed, 22 insertions, 30 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)
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