From 1a5e78031311da07917d8ec752c65f367096a6fe Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 13 Jan 2026 17:33:54 -0600 Subject: Move values module --- Functor/Instance/Nat/Push.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Functor/Instance/Nat/Push.agda') diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda index c417ebf..c5becb4 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -15,7 +15,7 @@ open import Data.Fin.Preimage using (preimage; preimage-cong₁) open import Data.Nat using (ℕ) open import Data.Setoid using (∣_∣; _⇒ₛ_) open import Data.Subset.Functional using (⁅_⁆) -open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup) +open import Data.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup) open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (_∙_) -- cgit v1.2.3