From 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 5 Nov 2025 08:11:48 -0600 Subject: Adjust universe levels --- Functor/Instance/Nat/Circ.agda | 22 +++++++++++----------- Functor/Instance/Nat/Edge.agda | 20 ++++++-------------- Functor/Instance/Nat/System.agda | 10 +++++----- 3 files changed, 22 insertions(+), 30 deletions(-) (limited to 'Functor/Instance') 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 -- cgit v1.2.3