[Import] ...

jmougeot · jmougeot · commit 5760807ba3e9 · 2025-03-04T17:25:15.000-05:00
diff --git a/src/Foreign/Haskell.agda b/src/Foreign/Haskell.agda
@@ -8,7 +8,7 @@
 
 module Foreign.Haskell where
 
-open import Level
+open import Level using (Level; _⊔_)
 
 ------------------------------------------------------------------------
 -- Pairs
diff --git a/src/Foreign/Haskell/Either.agda b/src/Foreign/Haskell/Either.agda
@@ -8,7 +8,7 @@
 
 module Foreign.Haskell.Either where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 private
diff --git a/src/Foreign/Haskell/List/NonEmpty.agda b/src/Foreign/Haskell/List/NonEmpty.agda
@@ -8,7 +8,7 @@
 
 module Foreign.Haskell.List.NonEmpty where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.List.NonEmpty.Base as Data using (_∷_)
 open import Data.List using (List)
 
diff --git a/src/Foreign/Haskell/Maybe.agda b/src/Foreign/Haskell/Maybe.agda
@@ -8,7 +8,7 @@
 
 module Foreign.Haskell.Maybe where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Maybe.Base as Data using (just; nothing)
 
 private
diff --git a/src/Foreign/Haskell/Pair.agda b/src/Foreign/Haskell/Pair.agda
@@ -8,7 +8,7 @@
 
 module Foreign.Haskell.Pair where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Product.Base using (_×_; _,_)
 
 private
diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda
@@ -15,6 +15,8 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Function.Definitions
+  using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Inverseˡ
+        ; Inverseʳ; Surjective)
 open import Relation.Nullary.Negation.Core using (contraposition)
 
 import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda
@@ -16,7 +16,7 @@ module Function.Consequences.Setoid
   where
 
 open import Function.Definitions
-open import Relation.Nullary.Negation.Core
+open import Relation.Nullary.Negation.Core using (¬_)
 
 import Function.Consequences as C
 
diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda
@@ -12,7 +12,11 @@ open import Data.Product.Base as Product using (_,_)
 open import Function.Base using (_∘_; flip)
 open import Function.Bundles
 open import Function.Definitions
+  using (Congruent; Injective; Surjective; Bijective; Inverseˡ; Inverseʳ
+        ; Inverseᵇ)
 open import Function.Structures
+  using (IsCongruent; IsInjection; IsSurjection ; IsBijection; IsLeftInverse
+        ; IsRightInverse; IsInverse)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
diff --git a/src/Function/Construct/Constant.agda b/src/Function/Construct/Constant.agda
@@ -9,9 +9,9 @@
 module Function.Construct.Constant where
 
 open import Function.Base using (const)
-open import Function.Bundles
-import Function.Definitions as Definitions
-import Function.Structures as Structures
+open import Function.Bundles using (Func)
+import Function.Definitions as Definitions using (Congruent)
+import Function.Structures as Structures using (IsCongruent)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda
@@ -12,7 +12,11 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Function.Bundles
 import Function.Definitions as Definitions
+  using (Congruent; Injective; Surjective; Bijective; Inverseʳ; Inverseˡ
+        ; Inverseᵇ)
 import Function.Structures as Structures
+  using (IsCongruent; IsInjection; IsSurjection; IsBijection; IsLeftInverse
+        ; IsRightInverse; IsInverse)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
@@ -11,11 +11,13 @@ module Function.Construct.Symmetry where
 open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
 open import Function.Base using (_∘_)
 open import Function.Definitions
-  using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ; Congruent)
+  using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ
+        ; Congruent)
 open import Function.Structures
   using (IsBijection; IsCongruent; IsRightInverse; IsLeftInverse; IsInverse)
 open import Function.Bundles
-  using (Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⤖_; _⇔_; _↩_; _↪_; _↔_)
+  using (Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⤖_; _⇔_
+        ; _↩_; _↪_; _↔_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda
@@ -9,18 +9,16 @@
 module Function.Endo.Propositional {a} (A : Set a) where
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
-open import Algebra.Core
-import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
-import Algebra.Properties.Monoid.Mult as MonoidMultProperties
+open import Algebra.Core using (Op₁; Op₂)
+import Algebra.Definitions.RawMonoid as RawMonoidDefinitions using (_×_)
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties using (×-homo-+)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
   using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
 open Definitions using (Homomorphic₂)
-
 open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
-
 open import Function.Base using (id; _∘′_; _∋_; flip)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda
@@ -11,7 +11,6 @@ open import Relation.Binary.Bundles using (Setoid)
 module Function.Endo.Setoid {c e} (S : Setoid c e) where
 
 open import Agda.Builtin.Equality using (_≡_)
-
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
 import Algebra.Properties.Monoid.Mult as MonoidMultProperties
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
@@ -15,7 +15,6 @@ Use Function.Endo.Propositional instead."
 
 open import Algebra
 open import Algebra.Morphism; open Definitions
-
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
diff --git a/src/Function/Identity/Effectful.agda b/src/Function/Identity/Effectful.agda
@@ -8,12 +8,12 @@
 
 module Function.Identity.Effectful where
 
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Effect.Comonad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
+open import Effect.Comonad using (RawComonad)
 open import Function.Base using (id; _∘′_; _|>′_; _$′_; flip)
-open import Level
+open import Level using (Level; _⊔_)
 
 private
   variable
diff --git a/src/Function/Metric/Nat/Bundles.agda b/src/Function/Metric/Nat/Bundles.agda
@@ -17,12 +17,13 @@ open import Function.Base using (const)
 open import Level using (Level; suc; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
-open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence)
-
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isEquivalence)
 open import Function.Metric.Nat.Core using (DistanceFunction)
 open import Function.Metric.Nat.Structures
-open import Function.Metric.Bundles as Base
-  using (GeneralMetric)
+  using (IsProtoMetric; IsPreMetric; IsQuasiSemiMetric; IsSemiMetric
+        ; IsMetric; IsUltraMetric)
+open import Function.Metric.Bundles as Base using (GeneralMetric)
 
 ------------------------------------------------------------------------
 -- Proto-metric
diff --git a/src/Function/Metric/Nat/Core.agda b/src/Function/Metric/Nat/Core.agda
@@ -9,7 +9,7 @@
 module Function.Metric.Nat.Core where
 
 open import Data.Nat.Base using (ℕ)
-import Function.Metric.Core as Base
+import Function.Metric.Core as Base using (DistanceFunction)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Function/Metric/Nat/Definitions.agda b/src/Function/Metric/Nat/Definitions.agda
@@ -9,9 +9,9 @@
 module Function.Metric.Nat.Definitions where
 
 open import Algebra.Core using (Op₂)
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ; _≤_; _+_; _⊔_ ; _<_)
 open import Level using (Level)
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Function.Metric.Nat.Core
diff --git a/src/Function/Metric/Nat/Structures.agda b/src/Function/Metric/Nat/Structures.agda
@@ -13,10 +13,10 @@ open import Function.Base using (const)
 open import Level using (Level; suc)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
-
-open import Function.Metric.Nat.Core
-open import Function.Metric.Nat.Definitions
+open import Function.Metric.Nat.Core using (DistanceFunction)
 import Function.Metric.Structures as Base
+  using (IsGeneralMetric; IsProtoMetric; IsPreMetric; IsQuasiSemiMetric
+        ; IsSemiMetric)
 
 private
   variable
