diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 08:11:48 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 08:11:48 -0600 |
| commit | 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 (patch) | |
| tree | 18e541e617682773e76041166cd516d9fe9dd668 /Functor/Instance/Nat/System.agda | |
| parent | 0ce2b2ee7bc6f37473de60d801391dd3ff2dc024 (diff) | |
Adjust universe levels
Diffstat (limited to 'Functor/Instance/Nat/System.agda')
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 10 |
1 files changed, 5 insertions, 5 deletions
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 |