aboutsummaryrefslogtreecommitdiff
path: root/Functor/Instance/Nat/Pull.agda
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-01-13 17:33:54 -0600
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2026-01-13 17:33:54 -0600
commit1a5e78031311da07917d8ec752c65f367096a6fe (patch)
treeacdd027f83fa4402da98fe2b7b41f90424870a3d /Functor/Instance/Nat/Pull.agda
parent3bf15830058dab0baca2b8518e4fe1c4a7363e45 (diff)
Move values module
Diffstat (limited to 'Functor/Instance/Nat/Pull.agda')
-rw-r--r--Functor/Instance/Nat/Pull.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
index c2a06c6..52f50f1 100644
--- a/Functor/Instance/Nat/Pull.agda
+++ b/Functor/Instance/Nat/Pull.agda
@@ -16,7 +16,7 @@ open import Data.Monoid using (fromMonoid)
open import Data.Nat.Base using (ℕ)
open import Data.Product using (_,_)
open import Data.Setoid using (∣_∣; _⇒ₛ_)
-open import Data.System.Values Monoid using (Values; _⊕_; module Object)
+open import Data.Values Monoid using (Values; _⊕_; module Object)
open import Data.Unit using (⊤; tt)
open import Function.Base using (id; _∘_)
open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)