diff --git a/CHANGELOG.md b/CHANGELOG.md index 804bcbd8c8..24fb3493a4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,6 +30,12 @@ Non-backwards compatible changes Other major improvements ------------------------ +Minor improvements +------------------ +The size of the dependency graph for many modules has been +reduced. This may lead to speed ups for first-time loading of some +modules. + Deprecated modules ------------------ diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 5c10a9e4cc..29490cbd0c 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -14,7 +14,10 @@ open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (Symmetric; Total) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; cong₂; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid) open import Relation.Unary using (Pred) open import Algebra.Core diff --git a/src/Algebra/Definitions/RawSemiring.agda b/src/Algebra/Definitions/RawSemiring.agda index 01aebc2d18..b1819d856d 100644 --- a/src/Algebra/Definitions/RawSemiring.agda +++ b/src/Algebra/Definitions/RawSemiring.agda @@ -8,7 +8,7 @@ open import Algebra.Bundles using (RawSemiring) open import Data.Sum.Base using (_⊎_) -open import Data.Nat using (ℕ; zero; suc) +open import Data.Nat.Base using (ℕ; zero; suc) open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda index 5583f22a5b..96e6b69103 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda @@ -6,7 +6,8 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra.Lattice +open import Algebra.Lattice using (BooleanAlgebra; isBooleanAlgebraʳ; + isDistributiveLatticeʳʲᵐ) module Algebra.Lattice.Properties.BooleanAlgebra.Expression {b} (B : BooleanAlgebra b b) @@ -14,10 +15,8 @@ module Algebra.Lattice.Properties.BooleanAlgebra.Expression open BooleanAlgebra B -open import Effect.Applicative as Applicative -open import Effect.Monad open import Data.Fin.Base using (Fin) -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Data.Vec.Base as Vec using (Vec) import Data.Vec.Effectful as Vec @@ -25,8 +24,11 @@ import Function.Identity.Effectful as Identity open import Data.Vec.Properties using (lookup-map) open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW using (Pointwise; ext) +open import Effect.Applicative as Applicative open import Function.Base using (_∘_; _$_; flip) -open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) import Relation.Binary.Reflection as Reflection -- Expressions made up of variables and the operations of a boolean @@ -68,7 +70,7 @@ module Naturality (f : Applicative.Morphism A₁ A₂) where - open ≡.≡-Reasoning + open ≡-Reasoning open Applicative.Morphism f open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁) open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂) diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index eefb5f40ab..9ce8836bd4 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -25,7 +25,8 @@ import Relation.Binary.Reflection as Reflection import Relation.Nullary.Decidable as Dec import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) open import Relation.Nullary.Decidable using (Dec) module Algebra.Solver.IdempotentCommutativeMonoid diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda index 7a70fb8cfc..962abd6ebc 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda @@ -9,7 +9,7 @@ module Algebra.Solver.IdempotentCommutativeMonoid.Example where -open import Relation.Binary.PropositionalEquality using (_≡_) +import Algebra.Solver.IdempotentCommutativeMonoid as ICM-Solver open import Data.Bool.Base using (_∨_) open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid) @@ -17,8 +17,9 @@ open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid) open import Data.Fin.Base using (zero; suc) open import Data.Vec.Base using ([]; _∷_) -open import Algebra.Solver.IdempotentCommutativeMonoid - ∨-idempotentCommutativeMonoid +open import Relation.Binary.PropositionalEquality.Core using (_≡_) + +open ICM-Solver ∨-idempotentCommutativeMonoid test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ x test a b c = let _∨_ = _⊕_ in diff --git a/src/Codata/Sized/Cofin.agda b/src/Codata/Sized/Cofin.agda index a7f74afb5f..e04be324de 100644 --- a/src/Codata/Sized/Cofin.agda +++ b/src/Codata/Sized/Cofin.agda @@ -8,15 +8,15 @@ module Codata.Sized.Cofin where -open import Size -open import Codata.Sized.Thunk +open import Size using (∞) +open import Codata.Sized.Thunk using (force) open import Codata.Sized.Conat as Conat using (Conat; zero; suc; infinity; _ℕ<_; sℕ≤s; _ℕ≤infinity) open import Codata.Sized.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s) -open import Data.Nat.Base -open import Data.Fin.Base as Fin hiding (fromℕ; fromℕ<; toℕ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc) open import Function.Base using (_∋_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) ------------------------------------------------------------------------ -- The type diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda index 13823bef75..4a91a903a2 100644 --- a/src/Data/Container/Combinator/Properties.agda +++ b/src/Data/Container/Combinator/Properties.agda @@ -9,16 +9,15 @@ module Data.Container.Combinator.Properties where open import Axiom.Extensionality.Propositional using (Extensionality) -open import Data.Container.Core +open import Data.Container.Core using (Container; ⟦_⟧) open import Data.Container.Combinator -open import Data.Container.Relation.Unary.Any open import Data.Empty using (⊥-elim) open import Data.Product.Base as P using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry) open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_]) open import Function.Base as F using (_∘′_) -open import Function.Bundles +open import Function.Bundles using (_↔_; mk↔ₛ′) open import Level using (_⊔_; lower) -open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; cong) -- I have proved some of the correctness statements under the -- assumption of functional extensionality. I could have reformulated diff --git a/src/Data/Container/Indexed/Combinator.agda b/src/Data/Container/Indexed/Combinator.agda index 825d173db7..bc5bd194c7 100644 --- a/src/Data/Container/Indexed/Combinator.agda +++ b/src/Data/Container/Indexed/Combinator.agda @@ -9,7 +9,8 @@ module Data.Container.Indexed.Combinator where open import Axiom.Extensionality.Propositional using (Extensionality) -open import Data.Container.Indexed +open import Data.Container.Indexed using (Container; _◃_/_; ⟦_⟧; + Command; Response; ◇; next) open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Product.Base as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_) @@ -18,10 +19,10 @@ open import Data.Sum.Relation.Unary.All as All using (All) open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_) open import Function.Bundles using (mk↔ₛ′) open import Function.Indexed.Bundles using (_↔ᵢ_) -open import Level +open import Level using (Level; _⊔_) open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂) renaming (_⟨×⟩_ to _⟪×⟫_; _⟨⊙⟩_ to _⟪⊙⟫_; _⟨⊎⟩_ to _⟪⊎⟫_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≗_; refl; cong) private diff --git a/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda index a1fc21f44e..eecd3af3d3 100644 --- a/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda @@ -8,13 +8,15 @@ module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where -open import Axiom.Extensionality.Propositional -open import Data.Container.Indexed.Core +open import Axiom.Extensionality.Propositional using (Extensionality) +open import Data.Container.Indexed.Core using (Container; ⟦_⟧) open import Data.Container.Indexed.Relation.Binary.Pointwise + using (Pointwise) open import Data.Product.Base using (_,_; Σ-syntax; -,_) open import Level using (Level; _⊔_) -open import Relation.Binary -open import Relation.Binary.PropositionalEquality as P +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; subst; cong) private variable @@ -28,13 +30,13 @@ module _ where refl : (∀ i → Reflexive (R i)) → Reflexive (Pointwise C R o) - refl R-refl = P.refl , λ p → R-refl _ + refl R-refl = ≡.refl , λ p → R-refl _ sym : (∀ i → Symmetric (R i)) → Symmetric (Pointwise C R o) - sym R-sym (P.refl , f) = P.refl , λ p → R-sym _ (f p) + sym R-sym (≡.refl , f) = ≡.refl , λ p → R-sym _ (f p) trans : (∀ i → Transitive (R i)) → Transitive (Pointwise C R o) - trans R-trans (P.refl , f) (P.refl , g) = P.refl , λ p → R-trans _ (f p) (g p) + trans R-trans (≡.refl , f) (≡.refl , g) = ≡.refl , λ p → R-trans _ (f p) (g p) -- If propositional equality is extensional, then `Eq _≡_` and `_≡_` coincide. Eq⇒≡ : {C : Container I O ℓˢ ℓᵖ} {X : I → Set ℓˣ} {R : (i : I) → Rel (X i) ℓᵉ} @@ -42,4 +44,4 @@ Eq⇒≡ : {C : Container I O ℓˢ ℓᵖ} {X : I → Set ℓˣ} {R : (i : I) Extensionality ℓᵖ ℓˣ → Pointwise C (λ (i : I) → _≡_ {A = X i}) o xs ys → xs ≡ ys -Eq⇒≡ ext (P.refl , f≈f′) = cong -,_ (ext f≈f′) +Eq⇒≡ ext (≡.refl , f≈f′) = cong -,_ (ext f≈f′) diff --git a/src/Data/Container/Membership.agda b/src/Data/Container/Membership.agda index 3ace9cdc06..6a04f397e8 100644 --- a/src/Data/Container/Membership.agda +++ b/src/Data/Container/Membership.agda @@ -10,10 +10,10 @@ module Data.Container.Membership where open import Level using (_⊔_) open import Relation.Unary using (Pred) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_) -open import Data.Container.Core -open import Data.Container.Relation.Unary.Any +open import Data.Container.Core using (Container; ⟦_⟧) +open import Data.Container.Relation.Unary.Any using (◇) module _ {s p} {C : Container s p} {x} {X : Set x} where diff --git a/src/Data/Container/Morphism/Properties.agda b/src/Data/Container/Morphism/Properties.agda index 39471b5e48..ca2e4e5b55 100644 --- a/src/Data/Container/Morphism/Properties.agda +++ b/src/Data/Container/Morphism/Properties.agda @@ -12,7 +12,7 @@ open import Level using (_⊔_; suc) open import Function.Base as F using (_$_) open import Data.Product.Base using (∃; proj₁; proj₂; _,_) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≗_) open import Data.Container.Core open import Data.Container.Morphism diff --git a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda index 978bfc55e4..9bdf815092 100644 --- a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda @@ -8,9 +8,10 @@ module Data.Container.Relation.Binary.Pointwise.Properties where -open import Axiom.Extensionality.Propositional -open import Data.Container.Core +open import Axiom.Extensionality.Propositional using (Extensionality) +open import Data.Container.Core using (Container; ⟦_⟧) open import Data.Container.Relation.Binary.Pointwise + using (Pointwise; _,_) open import Data.Product.Base using (_,_; Σ-syntax; -,_) open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda index 601d922a56..6e643a6031 100644 --- a/src/Data/Container/Relation/Unary/Any/Properties.agda +++ b/src/Data/Container/Relation/Unary/Any/Properties.agda @@ -8,23 +8,25 @@ module Data.Container.Relation.Unary.Any.Properties where -open import Level -open import Algebra +open import Algebra.Bundles using (CommutativeSemiring) open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂) open import Data.Product.Properties using (Σ-≡,≡→≡) open import Data.Product.Function.NonDependent.Propositional using (_×-cong_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) -open import Function.Base -open import Function.Bundles +open import Function.Base using (_∘_; _∘′_; id; flip; _$_) +open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse) open import Function.Properties.Inverse using (↔-refl) open import Function.Properties.Inverse.HalfAdjointEquivalence using (_≃_; ↔⇒≃) open import Function.Related.Propositional as Related using (Related; SK-sym) open import Function.Related.TypeIsomorphisms + using (×-⊎-commutativeSemiring; ∃∃↔∃∃; Σ-assoc; ×-comm) +open import Level using (Level; _⊔_) open import Relation.Unary using (Pred ; _∪_ ; _∩_) open import Relation.Binary.Core using (REL) -open import Relation.Binary.PropositionalEquality as ≡ +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≗_; refl) +open import Relation.Binary.PropositionalEquality.Properties as ≡ private module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 97ca14015b..398c1a3966 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -7,8 +7,13 @@ {-# OPTIONS --cubical-compatible --safe #-} {-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726) -open import Data.Fin.Base -open import Data.Fin.Properties +module Data.Fin.Induction where + +open import Data.Fin.Base using (Fin; zero; suc; _<_; toℕ; inject₁; + _≥_; _>_; fromℕ; _≺_) +open import Data.Fin.Properties using (toℕ-inject₁; ≤-refl; <-cmp; + toℕ≤n; toℕ-injective; toℕ-fromℕ; toℕ-lower₁; inject₁-lower₁; + pigeonhole; ≺⇒<′) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s) open import Data.Nat.Properties using (n<1+n; ≤⇒≯) import Data.Nat.Induction as ℕ @@ -18,8 +23,9 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_) import Data.Vec.Relation.Unary.Linked.Properties as Linked open import Function.Base using (flip; _$_) -open import Induction -open import Induction.WellFounded as WF +open import Induction using (RecStruct) +open import Induction.WellFounded as WF using (WellFounded; WfRec; + module Subrelation) open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (StrictPartialOrder) @@ -30,13 +36,12 @@ import Relation.Binary.Construct.Flip.Ord as Ord import Relation.Binary.Construct.NonStrictToStrict as ToStrict import Relation.Binary.Construct.On as On open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; subst; trans; cong) open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred) -module Data.Fin.Induction where - private variable ℓ : Level diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 3fa0ebf92f..794b93f76b 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -9,10 +9,10 @@ module Data.Fin.Permutation where open import Data.Bool.Base using (true; false) -open import Data.Empty using (⊥-elim) -open import Data.Fin.Base -open import Data.Fin.Patterns -open import Data.Fin.Properties +open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) +open import Data.Fin.Patterns using (0F) +open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn; + punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0) import Data.Fin.Permutation.Components as PC open import Data.Nat.Base using (ℕ; suc; zero) open import Data.Product.Base using (_,_; proj₂) @@ -20,7 +20,7 @@ open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′) open import Function.Construct.Composition using (_↔-∘_) open import Function.Construct.Identity using (↔-id) open import Function.Construct.Symmetry using (↔-sym) -open import Function.Definitions +open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ) open import Function.Properties.Inverse using (↔⇒↣) open import Function.Base using (_∘_) open import Level using (0ℓ) @@ -28,8 +28,10 @@ open import Relation.Binary.Core using (Rel) open import Relation.Nullary using (does; ¬_; yes; no) open import Relation.Nullary.Decidable using (dec-yes; dec-no) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary.PropositionalEquality - using (_≡_; _≢_; refl; sym; trans; subst; →-to-⟶; cong; cong₂; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning private @@ -241,7 +243,7 @@ module _ (π : Permutation (suc m) (suc n)) where lift₀-remove p (suc i) = punchOut-zero (πʳ (suc i)) p where punchOut-zero : ∀ {i} (j : Fin (suc n)) {neq} → i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j - punchOut-zero 0F {neq} p = ⊥-elim (neq p) + punchOut-zero 0F {neq} p = contradiction p neq punchOut-zero (suc j) refl = refl ↔⇒≡ : Permutation m n → m ≡ n diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index d345018778..2d2f34deb7 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -9,15 +9,19 @@ module Data.Fin.Permutation.Components where open import Data.Bool.Base using (Bool; true; false) -open import Data.Fin.Base +open import Data.Fin.Base using (Fin; suc; opposite; toℕ) open import Data.Fin.Properties + using (_≟_; opposite-prop; opposite-involutive; opposite-suc) open import Data.Nat.Base as ℕ using (zero; suc; _∸_) open import Data.Product.Base using (proj₂) open import Function.Base using (_∘_) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (does; _because_; yes; no) open import Relation.Nullary.Decidable using (dec-true; dec-false) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Algebra.Definitions using (Involutive) open ≡-Reasoning diff --git a/src/Data/Fin/Permutation/Transposition/List.agda b/src/Data/Fin/Permutation/Transposition/List.agda index 4da8f08d37..3d14d36b05 100644 --- a/src/Data/Fin/Permutation/Transposition/List.agda +++ b/src/Data/Fin/Permutation/Transposition/List.agda @@ -8,7 +8,7 @@ module Data.Fin.Permutation.Transposition.List where -open import Data.Fin.Base +open import Data.Fin.Base using (Fin; suc) open import Data.Fin.Patterns using (0F) open import Data.Fin.Permutation as P hiding (lift₀) import Data.Fin.Permutation.Components as PC @@ -16,8 +16,10 @@ open import Data.List.Base using (List; []; _∷_; map) open import Data.Nat.Base using (ℕ; suc; zero) open import Data.Product.Base using (_×_; _,_) open import Function.Base using (_∘_) -open import Relation.Binary.PropositionalEquality - using (_≡_; sym; cong; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; sym; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning private diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 6243e016eb..a1db966f92 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -40,8 +40,10 @@ open import Relation.Binary.Bundles using (Preorder; Setoid; DecSetoid; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) open import Relation.Binary.Structures using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) -open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + using (module ≡-Reasoning) open import Relation.Nullary.Decidable as Dec using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Negation.Core using (¬_; contradiction) diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 769c20ce06..03467dcee7 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -11,8 +11,10 @@ module Data.Fin.Subset.Properties where import Algebra.Definitions as AlgebraicDefinitions import Algebra.Structures as AlgebraicStructures import Algebra.Lattice.Structures as AlgebraicLatticeStructures -open import Algebra.Bundles -open import Algebra.Lattice.Bundles +open import Algebra.Bundles using (Magma; Semigroup; Monoid; Band; + CommutativeMonoid; IdempotentCommutativeMonoid) +open import Algebra.Lattice.Bundles using (Semilattice; Lattice; + DistributiveLattice; BooleanAlgebra) import Algebra.Lattice.Properties.Lattice as L import Algebra.Lattice.Properties.DistributiveLattice as DL import Algebra.Lattice.Properties.BooleanAlgebra as BA @@ -25,7 +27,7 @@ open import Data.Nat.Base hiding (∣_-_∣) import Data.Nat.Properties as ℕ open import Data.Product as Product using (∃; ∄; _×_; _,_; proj₁) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) -open import Data.Vec.Base +open import Data.Vec.Base using (Vec; []; _∷_; here; there) open import Data.Vec.Properties open import Function.Base using (_∘_; const; id; case_of_) open import Function.Bundles using (_⇔_; mk⇔) @@ -36,7 +38,10 @@ open import Relation.Binary.Structures open import Relation.Binary.Bundles using (Preorder; Poset; StrictPartialOrder; DecStrictPartialOrder) open import Relation.Binary.Definitions as B hiding (Decidable; Empty) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; subst; _≢_; sym) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning; isEquivalence) open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred; Decidable; Satisfiable) diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index ce5ff3e27c..179f806a22 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -9,16 +9,17 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Fin.Substitution.Lemmas +open import Data.Fin.Substitution.Lemmas using (Lemmas₄; AppLemmas) open import Data.Nat.Base using (ℕ) module Data.Fin.Substitution.List {ℓ} {T : ℕ → Set ℓ} (lemmas₄ : Lemmas₄ T) where -open import Data.List.Base -open import Data.List.Properties -open import Data.Fin.Substitution +open import Data.List.Base using (List; map) +open import Data.List.Properties using (map-id; map-cong; map-∘) +open import Data.Fin.Substitution using (Sub) import Function.Base as Fun -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda index 526f71f6c4..fab340ea0e 100644 --- a/src/Data/Float/Properties.agda +++ b/src/Data/Float/Properties.agda @@ -24,7 +24,10 @@ open import Relation.Binary.Structures open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality) import Relation.Binary.Construct.On as On -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid) ------------------------------------------------------------------------ -- Primitive properties diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index 28d15d05fd..639188c180 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -8,15 +8,16 @@ module Data.Integer.DivMod where -open import Data.Integer.Base +open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣; + _%ℕ_; _/ℕ_; _+_; _*_; -_; _-_; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _<_; +≤+; suc; + +<+) open import Data.Integer.Properties open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z) -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary using (yes; no; ¬_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; sym; _≢_; subst; resp₂; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning; setoid; decSetoid; isEquivalence) +open import Relation.Nullary.Decidable.Core using (yes; no) import Relation.Nullary.Reflects as Reflects -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) import Relation.Nullary.Decidable as Dec open import Algebra.Definitions {A = ℤ} _≡_ diff --git a/src/Data/Integer/Tactic/RingSolver.agda b/src/Data/Integer/Tactic/RingSolver.agda index d4e1a43536..e673c0f3d7 100644 --- a/src/Data/Integer/Tactic/RingSolver.agda +++ b/src/Data/Integer/Tactic/RingSolver.agda @@ -13,11 +13,11 @@ module Data.Integer.Tactic.RingSolver where open import Agda.Builtin.Reflection open import Data.Maybe.Base using (just; nothing) -open import Data.Integer.Base -open import Data.Integer.Properties +open import Data.Integer.Base using (+0) +open import Data.Integer.Properties using (+-*-commutativeRing) open import Level using (0ℓ) open import Data.Unit.Base using (⊤) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (refl) import Tactic.RingSolver as Solver import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda index e3855b26c5..0bbcad4973 100644 --- a/src/Data/List/Effectful.agda +++ b/src/Data/List/Effectful.agda @@ -23,8 +23,10 @@ open import Effect.Monad using (RawMonad; module Join; RawMonadZero; RawMonadPlus) open import Function.Base using (flip; _∘_; const; _$_; id; _∘′_; _$′_) open import Level using (Level) -open import Relation.Binary.PropositionalEquality as ≡ +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≢_; _≗_; refl) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + open ≡.≡-Reasoning private diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda index 3c81c0ff1e..57bbb2cca0 100644 --- a/src/Data/List/Membership/DecPropositional.agda +++ b/src/Data/List/Membership/DecPropositional.agda @@ -13,6 +13,8 @@ module Data.List.Membership.DecPropositional open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) +open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) + ------------------------------------------------------------------------ -- Re-export contents of propositional membership diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 12785eb59b..47ee739817 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -8,36 +8,40 @@ module Data.List.Membership.Propositional.Properties where -open import Algebra using (Op₂; Selective) +open import Algebra.Core using (Op₂) +open import Algebra.Definitions using (Selective) open import Effect.Monad using (RawMonad) open import Data.Bool.Base using (Bool; false; true; T) open import Data.Fin.Base using (Fin) open import Data.List.Base as List open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.List.Relation.Unary.Any.Properties + using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[]) open import Data.List.Membership.Propositional + using (_∈_; _∉_; mapWith∈; _≢∈_) import Data.List.Membership.Setoid.Properties as Membership open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≡⇒≋; ≋⇒≡) open import Data.List.Effectful using (monad) open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_) -open import Data.Nat.Properties -open import Data.Product.Base hiding (map) +open import Data.Nat.Properties using (_≤?_; m≤n⇒m≤1+n; ≤ᵇ-reflects-≤; <⇒≢; ≰⇒>) +open import Data.Product.Base using (∃; ∃₂; _×_; _,_) open import Data.Product.Properties using (×-≡,≡↔≡) open import Data.Product.Function.NonDependent.Propositional using (_×-cong_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) -open import Function.Base -open import Function.Definitions +open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_) +open import Function.Definitions using (Injective) import Function.Related.Propositional as Related -open import Function.Bundles -open import Function.Related.TypeIsomorphisms +open import Function.Bundles using (_↔_; _↣_; Injection) +open import Function.Related.TypeIsomorphisms using (×-comm; ∃∃↔∃∃) open import Function.Construct.Identity using (↔-id) open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions as Binary hiding (Decidable) -open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_; _≢_; refl; sym; trans; cong; subst; _≗_) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_) +open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid) import Relation.Binary.Properties.DecTotalOrder as DTOProperties open import Relation.Unary using (_⟨×⟩_; Decidable) import Relation.Nullary.Reflects as Reflects @@ -74,7 +78,7 @@ mapWith∈-cong : ∀ (xs : List A) → (f g : ∀ {x} → x ∈ xs → B) → (∀ {x} → (x∈xs : x ∈ xs) → f x∈xs ≡ g x∈xs) → mapWith∈ xs f ≡ mapWith∈ xs g mapWith∈-cong [] f g cong = refl -mapWith∈-cong (x ∷ xs) f g cong = ≡.cong₂ _∷_ (cong (here refl)) +mapWith∈-cong (x ∷ xs) f g cong = cong₂ _∷_ (cong (here refl)) (mapWith∈-cong xs (f ∘ there) (g ∘ there) (cong ∘ there)) mapWith∈≗map : ∀ (f : A → B) xs → mapWith∈ xs (λ {x} _ → f x) ≡ map f xs @@ -94,7 +98,7 @@ map-mapWith∈ = Membership.map-mapWith∈ (≡.setoid _) module _ (f : A → B) where ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs - ∈-map⁺ = Membership.∈-map⁺ (≡.setoid A) (≡.setoid B) (≡.cong f) + ∈-map⁺ = Membership.∈-map⁺ (≡.setoid A) (≡.setoid B) (cong f) ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x ∈-map⁻ = Membership.∈-map⁻ (≡.setoid A) (≡.setoid B) @@ -163,7 +167,7 @@ module _ (f : A → B → C) where ∈-cartesianProductWith⁺ : ∀ {xs ys a b} → a ∈ xs → b ∈ ys → f a b ∈ cartesianProductWith f xs ys ∈-cartesianProductWith⁺ = Membership.∈-cartesianProductWith⁺ - (≡.setoid A) (≡.setoid B) (≡.setoid C) (≡.cong₂ f) + (≡.setoid A) (≡.setoid B) (≡.setoid C) (cong₂ f) ∈-cartesianProductWith⁻ : ∀ xs ys {v} → v ∈ cartesianProductWith f xs ys → ∃₂ λ a b → a ∈ xs × b ∈ ys × v ≡ f a b @@ -243,10 +247,10 @@ module _ {n} {f : Fin n → A} where module _ {p} {P : A → Set p} (P? : Decidable P) where ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs - ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.subst P) + ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (subst P) ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v - ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.subst P) + ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (subst P) ------------------------------------------------------------------------ -- derun and deduplicate diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 68e9bfcf0e..c20f024c4a 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -8,24 +8,29 @@ module Data.List.NonEmpty.Properties where -open import Effect.Monad -open import Data.Nat -open import Data.Nat.Properties +open import Effect.Monad using (RawMonad) +open import Data.Nat.Base using (suc; _+_) +open import Data.Nat.Properties using (suc-injective) open import Data.Maybe.Properties using (just-injective) open import Data.Bool.Base using (Bool; true; false) open import Data.List.Base as List using (List; []; _∷_; _++_) open import Data.List.Effectful using () renaming (monad to listMonad) open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad) open import Data.List.NonEmpty -open import Data.List.NonEmpty.Relation.Unary.All + using (List⁺; _∷_; tail; head; toList; _⁺++_; _⁺++⁺_; _++⁺_; length; fromList; + drop+; map; groupSeqs; ungroupSeqs) +open import Data.List.NonEmpty.Relation.Unary.All using (All; toList⁺; _∷_) open import Data.List.Relation.Unary.All using ([]; _∷_) renaming (All to ListAll) import Data.List.Properties as List open import Data.Sum.Base using (inj₁; inj₂) open import Data.Sum.Relation.Unary.All using (inj₁; inj₂) import Data.Sum.Relation.Unary.All as Sum using (All; inj₁; inj₂) open import Level using (Level) -open import Function.Base -open import Relation.Binary.PropositionalEquality +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; _≗_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Unary using (Pred; Decidable; ∁) open import Relation.Nullary using (¬_; does; yes; no) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 1dcf0d1a20..20ac353903 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -36,7 +36,8 @@ open import Function.Definitions using (Injective) open import Level using (Level) open import Relation.Binary.Definitions as B using (DecidableEquality) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Relation.Binary.PropositionalEquality as ≡ hiding ([_]) +open import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Relation.Binary.Core using (Rel) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction) diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index f014df8b41..9c400fdcff 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -8,33 +8,39 @@ module Data.List.Relation.Binary.BagAndSetEquality where -open import Algebra using (Idempotent; CommutativeMonoid) +open import Algebra.Bundles using (CommutativeMonoid) +open import Algebra.Definitions using (Idempotent) open import Algebra.Structures.Biased using (isCommutativeMonoidˡ) open import Effect.Monad using (RawMonad) -open import Data.Empty -open import Data.Fin.Base +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base + using (List; []; _∷_; map; _++_; concat; [_]; lookup; length) open import Data.List.Effectful using (monad; module Applicative; module MonadProperties) import Data.List.Properties as List open import Data.List.Relation.Unary.Any using (Any; here; there) -open import Data.List.Relation.Unary.Any.Properties hiding (++-comm) +open import Data.List.Relation.Unary.Any.Properties + using (∷↔; map↔; Any-cong; ++↔; concat↔; >>=↔; ++↔++; ⊎↔; ⊥↔Any[]) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Membership.Propositional.Properties + using (∈-∃++) open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-preorder) open import Data.List.Relation.Binary.Permutation.Propositional + using (_↭_; ↭-sym; refl; module PermutationReasoning) open import Data.List.Relation.Binary.Permutation.Propositional.Properties -open import Data.Product.Base as Prod hiding (map) + using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ↭-sym-involutive; shift; ++-comm) +open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; _×_) import Data.Product.Function.Dependent.Propositional as Σ -open import Data.Sum.Base as Sum hiding (map) -open import Data.Sum.Properties hiding (map-cong) +open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂) +open import Data.Sum.Properties using (inj₂-injective; inj₁-injective) open import Data.Sum.Function.Propositional using (_⊎-cong_) -open import Data.Unit.Polymorphic.Base -open import Function.Base +open import Data.Unit.Polymorphic.Base using (⊤) +open import Function.Base using (_∘_; _$_; id; _⟨_⟩_; case_of_) open import Function.Bundles using (_↔_; Inverse; Equivalence; mk↔ₛ′; mk⇔) open import Function.Related.Propositional as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym) -open import Function.Related.TypeIsomorphisms +open import Function.Related.TypeIsomorphisms using (×-identityʳ; ∃∃↔∃∃) open import Function.Properties.Inverse using (↔-sym; ↔-trans; to-from) open import Level using (Level) open import Relation.Binary.Core using (_⇒_) @@ -42,10 +48,12 @@ open import Relation.Binary.Definitions using (Trans) open import Relation.Binary.Bundles using (Preorder; Setoid) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reasoning.Preorder as ≲-Reasoning -open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_; _≢_; _≗_; refl) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + using (module ≡-Reasoning) open import Relation.Binary.Reasoning.Syntax -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) private variable diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index af78f43c2c..0253c55460 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -6,22 +6,22 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra.Core using (Op₂) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Definitions using (Transitive; Symmetric; Reflexive; _Respects_) -open import Relation.Binary.Structures using (IsEquivalence) module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where - +open import Algebra.Core using (Op₂) open import Data.Fin.Base using (Fin) -open import Data.List.Base +open import Data.List.Base using (List; length; map; foldr; _++_; concat; + tabulate; filter; _ʳ++_; reverse) open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise) open import Data.List.Relation.Unary.Unique.Setoid S using (Unique) open import Function.Base using (_∘_) -open import Level -open import Relation.Binary.Core renaming (Rel to Rel₂) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Level using (Level; _⊔_) +open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_) renaming (Rel to Rel₂) +open import Relation.Binary.Definitions using (Transitive; Symmetric; Reflexive; _Respects_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Unary as U using (Pred) open Setoid S renaming (Carrier to A) diff --git a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda index d509b12be0..a1df8dfd6e 100644 --- a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda +++ b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda @@ -20,7 +20,8 @@ import Data.List.Relation.Binary.Sublist.DecSetoid as DecSetoidSublist import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist open import Relation.Binary.Bundles using (DecPoset) open import Relation.Binary.Structures using (IsDecPartialOrder) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) ------------------------------------------------------------------------ -- Re-export core definitions and operations diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda index 86194916f8..57ae74303b 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda @@ -25,16 +25,16 @@ open import Data.Maybe.Base as Maybe open import Data.Nat.Base as ℕ using (ℕ) open import Data.Product.Base using (Σ-syntax; _,_) open import Data.Vec.Base as Vec using (Vec ; lookup) -open import Data.List.Base hiding (lookup) -open import Data.List.Properties +open import Data.List.Base using (List; []; _∷_; [_]; _++_) +open import Data.List.Properties using (++-assoc; ++-identityʳ) open import Data.List.Relation.Binary.Sublist.Heterogeneous - hiding (lookup) + using (Sublist; minimum; _∷_) open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties -open import Function +open import Function.Base using (_$_; case_of_) -open import Relation.Binary.PropositionalEquality as ≡ +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≗_; sym; cong; cong₂; subst₂) -open import Relation.Nullary +open import Relation.Binary.PropositionalEquality.Properties as ≡ open ≡.≡-Reasoning diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional.agda b/src/Data/List/Relation/Binary/Sublist/Propositional.agda index a0f816ad84..b423548af2 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional.agda @@ -18,7 +18,10 @@ open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Bundles using (Preorder; Poset) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) open import Relation.Binary.Definitions using (Antisymmetric) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (subst; _≡_; refl) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; isEquivalence) open import Relation.Unary using (Pred) ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda index 163818b6e8..4235daf001 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda @@ -10,8 +10,10 @@ module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; cong; subst; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; cong; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning open import Data.List.Base using (List; []; _∷_; [_]) diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda index c9d2ea6724..94ccb9038b 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda @@ -20,10 +20,13 @@ open import Data.List.Relation.Binary.Sublist.Propositional import Data.List.Relation.Binary.Sublist.Setoid.Properties as SetoidProperties open import Data.Product.Base using (∃; _,_; proj₂) -open import Function.Base +open import Function.Base using (id; _∘_; _∘′_) open import Level using (Level) open import Relation.Binary.Definitions using (_Respects_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; _≗_; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; subst-injective) open import Relation.Unary using (Pred) private diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda index 949fded0ae..cf16aa0f30 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda @@ -11,7 +11,10 @@ module Data.List.Relation.Binary.Sublist.Propositional.Slice open import Data.List.Base using (List) open import Data.List.Relation.Binary.Sublist.Propositional -open import Relation.Binary.PropositionalEquality + using (_⊆_; UpperBound; ⊆-trans; ∷ₙ-ub; _∷ʳ_; _∷ₗ-ub_; _∷_; _∷ᵣ-ub_; + _,_∷-ub_; ⊆-upper-bound; []) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong) ------------------------------------------------------------------------ -- A Union where the triangles commute is a diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index f4556c6760..75e1a5b00a 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -6,24 +6,25 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary.Definitions hiding (Decidable) -open import Relation.Binary.Structures using (IsPreorder) - module Data.List.Relation.Binary.Subset.Propositional.Properties where open import Data.Bool.Base using (Bool; true; false; T) -open import Data.List.Base +open import Data.List.Base using (List; map; _∷_; _++_; concat; applyUpTo; + any; filter) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.All using (All) import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺) -open import Data.List.Effectful +open import Data.List.Effectful using (monad) open import Data.List.Relation.Unary.Any using (Any) -open import Data.List.Membership.Propositional +open import Data.List.Membership.Propositional using (_∈_; mapWith∈) open import Data.List.Membership.Propositional.Properties + using (map-∈↔; concat-∈↔; >>=-∈↔; ⊛-∈↔; ⊗-∈↔) import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset open import Data.List.Relation.Binary.Subset.Propositional + using (_⊆_; _⊇_) open import Data.List.Relation.Binary.Permutation.Propositional + using (_↭_; ↭-sym; ↭-isEquivalence) import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation open import Data.Nat.Base using (ℕ; _≤_) import Data.Product.Base as Product @@ -36,8 +37,12 @@ open import Relation.Nullary using (¬_; yes; no) open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Bundles using (Preorder) -open import Relation.Binary.PropositionalEquality - using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning) +open import Relation.Binary.Definitions hiding (Decidable) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≗_; subst; resp; refl) +open import Relation.Binary.PropositionalEquality.Properties + using (isEquivalence; setoid; module ≡-Reasoning) +open import Relation.Binary.Structures using (IsPreorder) import Relation.Binary.Reasoning.Preorder as ≲-Reasoning private diff --git a/src/Data/List/Relation/Ternary/Appending/Propositional.agda b/src/Data/List/Relation/Ternary/Appending/Propositional.agda index f807a0d649..1d1ad63509 100644 --- a/src/Data/List/Relation/Ternary/Appending/Propositional.agda +++ b/src/Data/List/Relation/Ternary/Appending/Propositional.agda @@ -15,8 +15,10 @@ open import Data.Product.Base using (_,_) import Data.List.Properties as List import Data.List.Relation.Binary.Pointwise as Pw using (≡⇒Pointwise-≡; Pointwise-≡⇒≡) -open import Relation.Binary.PropositionalEquality - using (_≡_; setoid; refl; trans; cong₂; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; trans; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning; setoid) import Data.List.Relation.Ternary.Appending.Setoid (setoid A) as General import Data.List.Relation.Ternary.Appending.Setoid.Properties (setoid A) diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index 9b145c3834..173dd87b62 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -8,12 +8,13 @@ module Data.List.Relation.Unary.AllPairs.Properties where -open import Data.List.Base hiding (any) +open import Data.List.Base using (List; []; _∷_; map; _++_; concat; take; drop; + applyUpTo; applyDownFrom; tabulate; filter; catMaybes) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.All.Properties as All using (Any-catMaybes⁺) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) -open import Data.Maybe using (Maybe; nothing; just) +open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Maybe.Relation.Binary.Pointwise using (pointwise⊆any; Pointwise) open import Data.Fin.Base as F using (Fin) open import Data.Fin.Properties using (suc-injective; <⇒≢) @@ -25,7 +26,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (DecSetoid) open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Unary using (Pred; Decidable; _⊆_) -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) private variable diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda index 38fcdd1507..dc1b7fb87d 100644 --- a/src/Data/List/Relation/Unary/Linked.agda +++ b/src/Data/List/Relation/Unary/Linked.agda @@ -19,7 +19,7 @@ open import Level using (Level; _⊔_) open import Relation.Binary.Definitions as B open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (refl; cong₂) open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_) open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda index e12b5cf47b..bcd7df1176 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda @@ -8,11 +8,14 @@ module Data.List.Relation.Unary.Unique.Propositional.Properties where -open import Data.List.Base +open import Data.List.Base using (map; _++_; concat; cartesianProductWith; + cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom; + tabulate; allFin; filter) open import Data.List.Relation.Binary.Disjoint.Propositional + using (Disjoint) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) -open import Data.List.Relation.Unary.Unique.Propositional +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (_<_) @@ -23,8 +26,9 @@ open import Function.Base using (id; _∘_) open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality - using (refl; _≡_; _≢_; sym; setoid) +open import Relation.Binary.PropositionalEquality.Core + using (refl; _≡_; _≢_; sym) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Negation using (¬_) diff --git a/src/Data/List/Reverse.agda b/src/Data/List/Reverse.agda index 0464181932..a197142c3f 100644 --- a/src/Data/List/Reverse.agda +++ b/src/Data/List/Reverse.agda @@ -8,10 +8,12 @@ module Data.List.Reverse where -open import Data.List.Base as L hiding (reverse) +open import Data.List.Base as L using (List; []; _∷_; _∷ʳ_) open import Data.List.Properties + using (unfold-reverse; reverse-involutive) open import Function.Base using (_$_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (subst; sym) -- If you want to traverse a list from the end, then you can use the -- reverse view of it. diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 5c4ce7c7d8..1548b5bde4 100644 --- a/src/Data/List/Zipper/Properties.agda +++ b/src/Data/List/Zipper/Properties.agda @@ -11,9 +11,14 @@ module Data.List.Zipper.Properties where open import Data.List.Base as List using (List ; [] ; _∷_) open import Data.List.Properties open import Data.List.Zipper + using (Zipper; toList; left; right; mkZipper; reverse; _ˡ++_; _ʳ++_; + _++ˡ_; _++ʳ_; map; foldr) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Maybe.Relation.Unary.All using (All; just; nothing) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning open import Function.Base using (_on_; _$′_; _$_; flip) diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda index 212f1608ff..2b4f1567e8 100644 --- a/src/Data/Maybe/Properties.agda +++ b/src/Data/Maybe/Properties.agda @@ -8,17 +8,21 @@ module Data.Maybe.Properties where -open import Algebra.Bundles +open import Algebra.Bundles using (Semigroup; Monoid) import Algebra.Structures as Structures import Algebra.Definitions as Definitions -open import Data.Maybe.Base +open import Data.Maybe.Base using (Maybe; just; nothing; map; _<∣>_; + maybe; maybe′) open import Data.Maybe.Relation.Unary.All using (All; just; nothing) open import Data.Product.Base using (_,_) open import Function.Base using (_∋_; id; _∘_; _∘′_) open import Function.Definitions using (Injective) open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; _≗_) +open import Relation.Binary.PropositionalEquality.Properties + using (isEquivalence) open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Decidable using (map′) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 949969033c..4669e479d9 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -11,30 +11,40 @@ module Data.Nat.Binary.Properties where open import Algebra.Bundles open import Algebra.Morphism.Structures import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism -open import Algebra.Consequences.Propositional +open import Algebra.Consequences.Propositional using (comm∧distrˡ⇒distrʳ) open import Data.Bool.Base using (if_then_else_; Bool; true; false) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Binary.Base -open import Data.Nat as ℕ using (ℕ; z≤n; s≤s; s_; _≤_; _<_; _+_; zero; suc; 1ᵇ; + _*_) open import Data.Nat.Binary.Properties import Data.Nat.Properties as ℕ open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; ∃) @@ -23,7 +26,11 @@ open import Function.Base using (_∘_; _$_) open import Level using (0ℓ) open import Relation.Binary using (Tri; tri<; tri≈; tri>; _Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Algebra using (magma) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; sym; trans; subst; _≢_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Nullary using (Dec; yes; no; does) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index d07d22db47..9a1cae638f 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -8,12 +8,14 @@ module Data.Nat.Combinatorics where -open import Data.Nat.Base -open import Data.Nat.DivMod -open import Data.Nat.Divisibility +open import Data.Nat.Base using (ℕ; zero; suc; _!; _∸_; z≤n; s≤s; _≤_; + _+_; _*_; _<_; s; tri≈; tri<) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; subst) import Data.Nat.Combinatorics.Base as Base diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda index ac1c6ca1b4..cf7f826522 100644 --- a/src/Data/Nat/Combinatorics/Specification.agda +++ b/src/Data/Nat/Combinatorics/Specification.agda @@ -11,18 +11,19 @@ module Data.Nat.Combinatorics.Specification where open import Data.Bool.Base using (T; true; false) -open import Data.Nat.Base -open import Data.Nat.DivMod -open import Data.Nat.Divisibility +open import Data.Nat.Base using (zero; suc; _≤ᵇ_; _≤_; _!; _∸_; pred; + >-nonZero; _*_; NonZero; _+_; s≤s; z≤n; _>_) +open import Data.Nat.DivMod using (_/_; n/n≡1; /-congʳ; m*n/m!≡n/[m∸1]!; + *-/-assoc; n/1≡n; m/n/o≡m/[n*o]; /-congˡ) +open import Data.Nat.Divisibility using (m≤n⇒m!∣n!; _∣_; ∣-refl; + ∣-reflexive; module ∣-Reasoning; ∣m∣n⇒∣m+n; *-monoʳ-∣; m∣n/o⇒o*m∣n) open import Data.Nat.Properties open import Data.Nat.Combinatorics.Base open import Data.Sum.Base using (inj₁; inj₂) -open import Relation.Binary.PropositionalEquality - using (_≡_; trans; _≢_) open import Relation.Nullary.Decidable using (yes; no; does) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary.PropositionalEquality - using (subst; refl; sym; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; trans; _≢_; subst; refl; sym; cong; cong₂) import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 5ff23e4c72..cddb2768f7 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -19,7 +19,8 @@ open import Data.Nat.Induction open import Data.Nat.Properties open import Data.Sum.Base using (inj₁; inj₂) open import Function.Base using (_$_; _∘_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; cong; cong₂; refl; trans; _≢_; sym) open import Relation.Nullary.Negation using (contradiction) open ≤-Reasoning diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda index a49318fbcd..7e627f4bfa 100644 --- a/src/Data/Nat/DivMod/Core.agda +++ b/src/Data/Nat/DivMod/Core.agda @@ -11,11 +11,13 @@ module Data.Nat.DivMod.Core where open import Agda.Builtin.Nat using () renaming (div-helper to divₕ; mod-helper to modₕ) -open import Data.Nat.Base +open import Data.Nat.Base using (zero; suc; _+_; _*_; _∸_; _≤_; _<_; + _≥_; z≤n; s≤s) open import Data.Nat.Properties open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym; subst; trans) open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/Nat/DivMod/WithK.agda b/src/Data/Nat/DivMod/WithK.agda index 10ef4c4f21..c161d7ab3e 100644 --- a/src/Data/Nat/DivMod/WithK.agda +++ b/src/Data/Nat/DivMod/WithK.agda @@ -8,16 +8,17 @@ module Data.Nat.DivMod.WithK where -open import Data.Nat using (ℕ; NonZero; _+_; _*_) +open import Data.Nat.Base using (ℕ; NonZero; _+_; _*_) open import Data.Nat.DivMod hiding (_mod_; _divMod_) open import Data.Nat.Properties using (≤⇒≤″) -open import Data.Nat.WithK +open import Data.Nat.WithK using (≤″-erase) open import Data.Fin.Base using (Fin; toℕ; fromℕ<″) open import Data.Fin.Properties using (toℕ-fromℕ<″) open import Function.Base using (_$_) -open import Relation.Binary.PropositionalEquality - using (cong; module ≡-Reasoning) -open import Relation.Binary.PropositionalEquality.WithK +open import Relation.Binary.PropositionalEquality.Core using (cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.WithK using (≡-erase) open ≡-Reasoning diff --git a/src/Data/Nat/GCD/Lemmas.agda b/src/Data/Nat/GCD/Lemmas.agda index 21788f0d88..5f358e6cf3 100644 --- a/src/Data/Nat/GCD/Lemmas.agda +++ b/src/Data/Nat/GCD/Lemmas.agda @@ -11,7 +11,10 @@ module Data.Nat.GCD.Lemmas where open import Data.Nat.Base open import Data.Nat.Properties open import Function.Base using (_$_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; sym) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning diff --git a/src/Data/Nat/GeneralisedArithmetic.agda b/src/Data/Nat/GeneralisedArithmetic.agda index 38d9472092..a5b1d7700f 100644 --- a/src/Data/Nat/GeneralisedArithmetic.agda +++ b/src/Data/Nat/GeneralisedArithmetic.agda @@ -8,11 +8,15 @@ module Data.Nat.GeneralisedArithmetic where -open import Data.Nat.Base -open import Data.Nat.Properties +open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_) +open import Data.Nat.Properties using (+-comm; +-assoc; *-identityˡ; + *-assoc) open import Function.Base using (_∘′_; _∘_; id) open import Level using (Level) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning private diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda index 6d86336193..38a4c3eecd 100644 --- a/src/Data/Nat/InfinitelyOften.agda +++ b/src/Data/Nat/InfinitelyOften.agda @@ -11,12 +11,12 @@ module Data.Nat.InfinitelyOften where open import Effect.Monad using (RawMonad) open import Level using (Level; 0ℓ) open import Data.Empty using (⊥-elim) -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ; _≤_; _⊔_; _+_; suc; zero; s≤s) open import Data.Nat.Properties open import Data.Product.Base as Prod hiding (map) open import Data.Sum.Base using (inj₁; inj₂; _⊎_) open import Function.Base using (_∘_; id) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Negation using (¬¬-Monad; call/cc) open import Relation.Unary using (Pred; _∪_; _⊆_) diff --git a/src/Data/Nat/Logarithm/Core.agda b/src/Data/Nat/Logarithm/Core.agda index 397dd3b3b9..fea77bf42d 100644 --- a/src/Data/Nat/Logarithm/Core.agda +++ b/src/Data/Nat/Logarithm/Core.agda @@ -8,12 +8,15 @@ module Data.Nat.Logarithm.Core where -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ; _<_; zero; suc; _+_; ⌊_/2⌋; ⌈_/2⌉; + _≤_; z≤n; s≤s; _∸_; NonZero; _*_; _^_) open import Data.Nat.Properties open import Data.Nat.Induction using (<-wellFounded) open import Induction.WellFounded using (Acc; acc) -open import Relation.Binary.PropositionalEquality -open import Data.Unit +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) ------------------------------------------------------------------------ -- Logarithm base 2 diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 1a491fdf93..b07883ce9b 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -23,7 +23,7 @@ open import Relation.Nullary.Decidable as Dec open import Relation.Nullary.Negation using (¬_; contradiction; contradiction₂) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) private diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 66e75dd4df..4a91348a66 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -33,8 +33,10 @@ open import Induction using (build) open import Induction.Lexicographic using (_⊗_; [_⊗_]) open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; trans; cong; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; trans; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e58385f587..9bca65bacc 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -11,11 +11,14 @@ module Data.Nat.Properties where -open import Axiom.UniquenessOfIdentityProofs -open import Algebra.Bundles +open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP) +open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup; + CommutativeMonoid; Monoid; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne) open import Algebra.Morphism open import Algebra.Consequences.Propositional + using (comm+cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ) open import Algebra.Construct.NaturalChoice.Base + using (MinOperator; MaxOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties @@ -23,11 +26,13 @@ open import Data.Bool.Base using (Bool; false; true; T) open import Data.Bool.Properties using (T?) open import Data.Nat.Base open import Data.Product.Base using (∃; _×_; _,_) -open import Data.Sum.Base as Sum +open import Data.Sum.Base as Sum using (inj₁; inj₂; _⊎_; [_,_]′) open import Data.Unit.Base using (tt) -open import Function.Base +open import Function.Base using (_∘_; flip; _$_; id; _∘′_; _$′_) open import Function.Bundles using (_↣_) -open import Function.Metric.Nat +open import Function.Metric.Nat using (TriangleInequality; IsProtoMetric; IsPreMetric; + IsQuasiSemiMetric; IsSemiMetric; IsMetric; PreMetric; QuasiSemiMetric; + SemiMetric; Metric) open import Level using (0ℓ) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core diff --git a/src/Data/Nat/Tactic/RingSolver.agda b/src/Data/Nat/Tactic/RingSolver.agda index e55bf6c963..1d5c2036f5 100644 --- a/src/Data/Nat/Tactic/RingSolver.agda +++ b/src/Data/Nat/Tactic/RingSolver.agda @@ -10,14 +10,14 @@ module Data.Nat.Tactic.RingSolver where -open import Agda.Builtin.Reflection +open import Agda.Builtin.Reflection using (Term; TC) open import Data.Maybe.Base using (just; nothing) -open import Data.Nat.Base using (zero; suc) -open import Data.Nat.Properties +open import Data.Nat.Base using (zero) +open import Data.Nat.Properties using (+-*-commutativeSemiring) open import Level using (0ℓ) open import Data.Unit.Base using (⊤) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (refl) import Tactic.RingSolver as Solver import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index 079257482b..ebca1ef000 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -9,21 +9,23 @@ module Data.Parity.Properties where open import Algebra.Bundles -open import Data.Empty open import Data.Nat.Base as ℕ using (zero; suc; parity) open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; fromSign) open import Data.Product.Base using (_,_) -open import Data.Sign.Base as 𝕊 +import Data.Sign.Base as 𝕊 open import Function.Base using (_$_; id) open import Function.Definitions open import Function.Consequences.Propositional + using (inverseʳ⇒injective; inverseˡ⇒surjective) open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) -open import Relation.Binary.PropositionalEquality - using (_≡_; _≢_; refl; sym; cong; cong₂; module ≡-Reasoning - ; setoid; isEquivalence; decSetoid; isDecEquivalence) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≢_; refl; sym; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning; setoid; isEquivalence; decSetoid; isDecEquivalence) open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open import Algebra.Structures {A = Parity} _≡_ open import Algebra.Definitions {A = Parity} _≡_ @@ -129,8 +131,8 @@ p+p≡0ℙ 1ℙ = refl +-cancelʳ-≡ : RightCancellative ℙ._+_ +-cancelʳ-≡ _ 1ℙ 1ℙ _ = refl -+-cancelʳ-≡ _ 1ℙ 0ℙ eq = ⊥-elim (p≢p⁻¹ _ $ sym eq) -+-cancelʳ-≡ _ 0ℙ 1ℙ eq = ⊥-elim (p≢p⁻¹ _ eq) ++-cancelʳ-≡ _ 1ℙ 0ℙ eq = contradiction (sym eq) (p≢p⁻¹ _) ++-cancelʳ-≡ _ 0ℙ 1ℙ eq = contradiction eq (p≢p⁻¹ _) +-cancelʳ-≡ _ 0ℙ 0ℙ _ = refl +-cancelˡ-≡ : LeftCancellative ℙ._+_ @@ -407,8 +409,8 @@ toSign-inverseʳ {0ℙ} refl = refl toSign-inverseʳ {1ℙ} refl = refl toSign-inverseˡ : Inverseˡ _≡_ _≡_ toSign fromSign -toSign-inverseˡ { + } refl = refl -toSign-inverseˡ { - } refl = refl +toSign-inverseˡ { 𝕊.+ } refl = refl +toSign-inverseˡ { 𝕊.- } refl = refl toSign-injective : Injective _≡_ _≡_ toSign toSign-injective = inverseʳ⇒injective toSign toSign-inverseʳ diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 2063e1cfbb..cb8a8d99a1 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -9,22 +9,25 @@ module Data.Product.Function.Dependent.Propositional where -open import Data.Product.Base as Product -open import Data.Product.Function.NonDependent.Setoid using () -open import Data.Product.Relation.Binary.Pointwise.NonDependent using () +open import Data.Product.Base as Product using (Σ; map; proj₂; _,_) open import Data.Product.Properties using (Σ-≡,≡→≡; Σ-≡,≡↔≡; Σ-≡,≡←≡) open import Level using (Level; 0ℓ) -open import Function.Related.TypeIsomorphisms open import Function.Related.Propositional -open import Function.Base -open import Function.Properties.Inverse -open import Function.Properties.RightInverse + using (_∼[_]_; module EquationalReasoning; K-reflexive; + implication; reverseImplication; equivalence; injection; + reverseInjection; leftInverse; surjection; bijection) +open import Function.Base using (_$_; _∘_; _∘′_) +open import Function.Properties.Inverse using (↔⇒↠; ↔⇒⟶; ↔⇒⟵; ↔-sym; ↔⇒↩) +open import Function.Properties.RightInverse using (↩⇒↪; ↪⇒↩) open import Function.Properties.Inverse.HalfAdjointEquivalence + using (↔⇒≃; _≃_; ≃⇒↔) open import Function.Consequences.Propositional using (inverseʳ⇒injective; strictlySurjective⇒surjective) open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective; StrictlySurjective) open import Function.Bundles -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + using (module ≡-Reasoning) private variable diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda index 5e7f3d1496..1552564ed0 100644 --- a/src/Data/Product/Function/NonDependent/Propositional.agda +++ b/src/Data/Product/Function/NonDependent/Propositional.agda @@ -12,13 +12,20 @@ module Data.Product.Function.NonDependent.Propositional where open import Data.Product.Base using (_×_; map) open import Data.Product.Function.NonDependent.Setoid open import Data.Product.Relation.Binary.Pointwise.NonDependent -open import Function + using (_×ₛ_; Pointwise-≡↔≡) +open import Function.Base using (id) +open import Function.Bundles + using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _⤖_; _↩_; _↪_; _↔_) open import Function.Properties.Inverse as Inv + using (Inverse⇒Equivalence; Inverse⇒Injection; Inverse⇒Surjection; + Inverse⇒Bijection) open import Function.Related.Propositional -open import Function.Construct.Composition as Compose + using (_∼[_]_; implication; reverseImplication; equivalence; injection; + reverseInjection; leftInverse; surjection; bijection) +import Function.Construct.Composition as Compose open import Level using (Level; _⊔_) open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.PropositionalEquality using (setoid) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) private variable @@ -41,7 +48,7 @@ private ------------------------------------------------------------------------ -- Combinators for various function types -infixr 2 _×-⇔_ _×-↣_ _×-↠_ _×-⤖_ _×-↩_ _×-↪_ _×-↔_ +infixr 2 _×-⟶_ _×-⇔_ _×-↣_ _×-↠_ _×-⤖_ _×-↩_ _×-↪_ _×-↔_ _×-⟶_ : A ⟶ B → C ⟶ D → (A × C) ⟶ (B × D) _×-⟶_ = liftViaInverse Compose.function Inv.toFunction _×-function_ diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda index 95951951b4..861b960c36 100644 --- a/src/Data/Product/Function/NonDependent/Setoid.agda +++ b/src/Data/Product/Function/NonDependent/Setoid.agda @@ -10,10 +10,12 @@ module Data.Product.Function.NonDependent.Setoid where open import Data.Product.Base as Product -open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Level using (Level) -open import Relation.Binary -open import Function +open import Relation.Binary.Bundles using (Setoid) +open import Function.Bundles + using (Func; Equivalence; Injection; Surjection; Bijection; LeftInverse; + RightInverse; Inverse) private variable diff --git a/src/Data/Product/Properties/WithK.agda b/src/Data/Product/Properties/WithK.agda index 329cdaf675..593f18ab37 100644 --- a/src/Data/Product/Properties/WithK.agda +++ b/src/Data/Product/Properties/WithK.agda @@ -10,7 +10,8 @@ module Data.Product.Properties.WithK where open import Data.Product.Base using (Σ; _,_) open import Function.Base using (_∋_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl) ------------------------------------------------------------------------ -- Equality diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 43088288e2..a00ef23f82 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -30,7 +30,7 @@ open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) import Data.Nat.Properties as ℕ open import Data.Nat.Coprimality as C using (Coprime; coprime?) -open import Data.Nat.Divisibility +open import Data.Nat.Divisibility using (_∣_; divides; ∣-antisym; *-pres-∣) import Data.Nat.GCD as ℕ import Data.Nat.DivMod as ℕ open import Data.Product.Base using (proj₁; proj₂; _×_; _,_; uncurry) @@ -43,19 +43,22 @@ open import Data.Rational.Unnormalised.Base as ℚᵘ ; _+_ to _+ᵘ_ ) import Data.Rational.Unnormalised.Properties as ℚᵘ -open import Data.Sum.Base as Sum -import Data.Sign.Base as S +open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′; _⊎_) +import Data.Sign.Base as Sign open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip) open import Function.Definitions using (Injective) open import Level using (0ℓ) open import Relation.Binary -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; sym; trans; _≢_; subst; subst₂; resp₂) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid; module ≡-Reasoning; isEquivalence) open import Relation.Binary.Morphism.Structures import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms open import Relation.Nullary.Decidable.Core as Dec using (yes; no; recompute; map′; _×-dec_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Binary.Reasoning.Syntax +open import Relation.Binary.Reasoning.Syntax using (module ≃-syntax) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ @@ -254,8 +257,8 @@ normalize-coprime {n} {d-1} c = begin ↥-normalize i n = begin ↥ (normalize i n) ℤ.* + g ≡⟨ cong (ℤ._* + g) (↥-mkℚ+ _ (n ℕ./ g)) ⟩ + i/g ℤ.* + g ≡⟨⟩ - S.+ ◃ i/g ℕ.* g ≡⟨ cong (S.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣m i n)) ⟩ - S.+ ◃ i ≡⟨ ℤ.+◃n≡+n i ⟩ + Sign.+ ◃ i/g ℕ.* g ≡⟨ cong (Sign.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣m i n)) ⟩ + Sign.+ ◃ i ≡⟨ ℤ.+◃n≡+n i ⟩ + i ∎ where open ≡-Reasoning @@ -268,8 +271,8 @@ normalize-coprime {n} {d-1} c = begin ↧-normalize i n = begin ↧ (normalize i n) ℤ.* + g ≡⟨ cong (ℤ._* + g) (↧-mkℚ+ _ (n ℕ./ g)) ⟩ + (n ℕ./ g) ℤ.* + g ≡⟨⟩ - S.+ ◃ n ℕ./ g ℕ.* g ≡⟨ cong (S.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣n i n)) ⟩ - S.+ ◃ n ≡⟨ ℤ.+◃n≡+n n ⟩ + Sign.+ ◃ n ℕ./ g ℕ.* g ≡⟨ cong (Sign.+ ◃_) (ℕ.m/n*n≡m (ℕ.gcd[m,n]∣n i n)) ⟩ + Sign.+ ◃ n ≡⟨ ℤ.+◃n≡+n n ⟩ + n ∎ where open ≡-Reasoning @@ -352,7 +355,7 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡ ↥ (- norm) ℤ.* + g ≡⟨ cong (ℤ._* + g) (↥-neg norm) ⟩ ℤ.- (↥ norm) ℤ.* + g ≡⟨ sym (ℤ.neg-distribˡ-* (↥ norm) (+ g)) ⟩ ℤ.- (↥ norm ℤ.* + g) ≡⟨ cong (ℤ.-_) (↥-normalize (suc m) n) ⟩ - S.- ◃ suc m ≡⟨⟩ + Sign.- ◃ suc m ≡⟨⟩ -[1+ m ] ∎ where open ℤ.≤-Reasoning @@ -401,13 +404,13 @@ private /-injective-≃ : ∀ p q → ↥ᵘ p / ↧ₙᵘ p ≡ ↥ᵘ q / ↧ₙᵘ q → p ≃ᵘ q /-injective-≃ (mkℚᵘ (+ m) c-1) (mkℚᵘ (+ n) d-1) eq = - *≡* (cong (S.+ ◃_) (normalize-injective-≃ m n _ _ eq)) + *≡* (cong (Sign.+ ◃_) (normalize-injective-≃ m n _ _ eq)) /-injective-≃ (mkℚᵘ (+ m) c-1) (mkℚᵘ -[1+ n ] d-1) eq = ℚᵘ.≃-sym (/-injective-≃-helper (sym eq)) /-injective-≃ (mkℚᵘ -[1+ m ] c-1) (mkℚᵘ (+ n) d-1) eq = /-injective-≃-helper eq /-injective-≃ (mkℚᵘ -[1+ m ] c-1) (mkℚᵘ -[1+ n ] d-1) eq = - *≡* (cong (S.- ◃_) (normalize-injective-≃ (suc m) (suc n) _ _ (neg-injective eq))) + *≡* (cong (Sign.- ◃_) (normalize-injective-≃ (suc m) (suc n) _ _ (neg-injective eq))) ------------------------------------------------------------------------ -- Properties of toℚ/fromℚ diff --git a/src/Data/Record.agda b/src/Data/Record.agda index bd916a9005..709ce69a67 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -10,15 +10,14 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Bool.Base using (true; false; if_then_else_) -open import Data.Empty -open import Data.List.Base +open import Data.Empty using (⊥) +open import Data.List.Base using (List; []; _∷_; foldr) open import Data.Product.Base hiding (proj₁; proj₂) -open import Data.Unit.Polymorphic +open import Data.Unit.Polymorphic using (⊤) open import Function.Base using (id; _∘_) -open import Level +open import Level using (suc; _⊔_) open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Nullary -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable using (does) -- The module is parametrised by the type of labels, which should come -- with decidable equality. diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index 7ac07167e7..f72f5ce476 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -8,17 +8,21 @@ module Data.Sign.Properties where -open import Algebra.Bundles -open import Data.Empty -open import Data.Sign.Base +open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup; + Monoid; CommutativeMonoid; Group; AbelianGroup) +open import Data.Sign.Base using (Sign; opposite; _*_; +; -) open import Data.Product.Base using (_,_) open import Function.Base using (_$_; id) open import Function.Definitions using (Injective) open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; _≢_; sym; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid; isDecEquivalence; isEquivalence) open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open import Algebra.Structures {A = Sign} _≡_ open import Algebra.Definitions {A = Sign} _≡_ @@ -102,8 +106,8 @@ s*s≡+ - = refl *-cancelʳ-≡ : RightCancellative _*_ *-cancelʳ-≡ _ - - _ = refl -*-cancelʳ-≡ _ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq) -*-cancelʳ-≡ _ + - eq = ⊥-elim (s≢opposite[s] _ eq) +*-cancelʳ-≡ _ - + eq = contradiction (sym eq) (s≢opposite[s] _) +*-cancelʳ-≡ _ + - eq = contradiction eq (s≢opposite[s] _) *-cancelʳ-≡ _ + + _ = refl *-cancelˡ-≡ : LeftCancellative _*_ diff --git a/src/Data/Star/Environment.agda b/src/Data/Star/Environment.agda index 6d30db7c3c..67ac8e8abd 100644 --- a/src/Data/Star/Environment.agda +++ b/src/Data/Star/Environment.agda @@ -12,10 +12,11 @@ open import Level using (_⊔_) open import Data.Star.List using (List) open import Data.Star.Decoration using (All) open import Data.Star.Pointer as Pointer using (Any; this; that; result) -open import Data.Unit.Polymorphic using (⊤) +open import Data.Unit.Polymorphic.Base using (⊤) open import Function.Base using (const) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import Relation.Binary.Construct.Closure.ReflexiveTransitive + using (_▻_) -- Contexts, listing the types of all the elements in an environment. diff --git a/src/Data/Sum/Function/Propositional.agda b/src/Data/Sum/Function/Propositional.agda index 25bb1a0907..e2b1b10000 100644 --- a/src/Data/Sum/Function/Propositional.agda +++ b/src/Data/Sum/Function/Propositional.agda @@ -13,6 +13,8 @@ open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_) open import Function.Construct.Composition as Compose open import Function.Related.Propositional + using (_∼[_]_; implication; reverseImplication; equivalence; injection; + reverseInjection; leftInverse; surjection; bijection) open import Function.Base using (id) open import Function.Bundles using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _↩_; _↪_; _⤖_; _↔_) @@ -20,7 +22,7 @@ open import Function.Properties.Inverse as Inv open import Level using (Level; _⊔_) open import Relation.Binary.Core using (REL) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality using (setoid) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) private variable diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda index 72dc3aa641..a19a1daae6 100644 --- a/src/Data/Sum/Properties.agda +++ b/src/Data/Sum/Properties.agda @@ -8,15 +8,15 @@ module Data.Sum.Properties where -open import Level -open import Data.Sum.Base +open import Level using (Level) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; swap; [_,_]; map; + map₁; map₂; assocˡ; assocʳ) open import Function.Base using (_∋_; _∘_; id) open import Function.Bundles using (mk↔ₛ′; _↔_) open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable using (map′) - +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≗_; refl; cong) +open import Relation.Nullary.Decidable.Core using (yes; no; map′) private variable diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda index 9f6cb55ce1..79d35e53a6 100644 --- a/src/Data/These/Properties.agda +++ b/src/Data/These/Properties.agda @@ -9,10 +9,11 @@ module Data.These.Properties where open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry) -open import Data.These.Base +open import Data.These.Base using (These; this; that; these) open import Function.Base using (_∘_) open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂) open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) ------------------------------------------------------------------------ diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda index 0a3ecd2337..7f5151600f 100644 --- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda +++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda @@ -24,7 +24,7 @@ open import Level using (Level) open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Construct.Intersection using (_∩_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) open import Relation.Nullary using (Reflects; ¬_; yes; no) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda index 3c98800c66..fefb27764f 100644 --- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda +++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda @@ -24,7 +24,7 @@ open import Level using (Level) open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Construct.Intersection using (_∩_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) open import Relation.Nullary using (Reflects; ¬_; yes; no) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/Tree/Binary/Properties.agda b/src/Data/Tree/Binary/Properties.agda index b523b1e6f1..270e6c66a2 100644 --- a/src/Data/Tree/Binary/Properties.agda +++ b/src/Data/Tree/Binary/Properties.agda @@ -13,8 +13,9 @@ open import Function.Nary.NonDependent using (congₙ) open import Level using (Level) open import Data.Nat.Base using (suc; _+_) open import Data.Tree.Binary -open import Function.Base -open import Relation.Binary.PropositionalEquality +open import Function.Base using (id; flip) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; cong₂; _≗_) private variable diff --git a/src/Data/Tree/Binary/Zipper/Properties.agda b/src/Data/Tree/Binary/Zipper/Properties.agda index fa2f09c190..03a88b09d2 100644 --- a/src/Data/Tree/Binary/Zipper/Properties.agda +++ b/src/Data/Tree/Binary/Zipper/Properties.agda @@ -8,17 +8,22 @@ module Data.Tree.Binary.Zipper.Properties where -open import Data.Tree.Binary as BT using (Tree; node; leaf) -open import Data.Tree.Binary.Zipper -open import Data.Nat using (ℕ; suc; _+_) -open import Data.Nat.Properties open import Data.List.Base as List using (List ; [] ; _∷_; sum) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Maybe.Relation.Unary.All using (All; just; nothing) -open import Relation.Binary.PropositionalEquality -open ≡-Reasoning +open import Data.Nat.Base using (ℕ; suc; _+_) +open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc) +open import Data.Tree.Binary as BT using (Tree; node; leaf) +open import Data.Tree.Binary.Zipper using (Zipper; toTree; up; mkZipper; + leftBranch; rightBranch; left; right; #nodes; Crumb; getTree; #leaves; + map; foldr; _⟪_⟫ˡ_; _⟪_⟫ʳ_) open import Function.Base using (_on_; _∘_; _$_) open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) +open ≡-Reasoning private variable diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index 91600e68c8..da86ca31ad 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -11,12 +11,15 @@ module Data.Tree.Rose.Properties where open import Level using (Level) open import Size open import Data.List.Base as List using (List) -open import Data.List.Extrema.Nat +open import Data.List.Extrema.Nat using (max) import Data.List.Properties as List open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Tree.Rose -open import Function.Base -open import Relation.Binary.PropositionalEquality +open import Data.Tree.Rose using (Rose; node; map; depth; foldr) +open import Function.Base using (_∘′_; _$_; _∘_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≗_; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning private diff --git a/src/Data/Unit/Polymorphic/Properties.agda b/src/Data/Unit/Polymorphic/Properties.agda index 088758ab39..f5e9fb9be0 100644 --- a/src/Data/Unit/Polymorphic/Properties.agda +++ b/src/Data/Unit/Polymorphic/Properties.agda @@ -9,21 +9,23 @@ module Data.Unit.Polymorphic.Properties where -open import Level +open import Level using (Level) open import Function.Bundles using (_↔_; mk↔) open import Data.Product.Base using (_,_) open import Data.Sum.Base using (inj₁) open import Data.Unit.Base renaming (⊤ to ⊤*) open import Data.Unit.Polymorphic.Base using (⊤; tt) -open import Relation.Nullary +open import Relation.Nullary.Decidable using (yes) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) open import Relation.Binary.Definitions using (DecidableEquality; Antisymmetric; Total) -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; trans; decSetoid; setoid; isEquivalence) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (decSetoid; setoid; isEquivalence) private variable diff --git a/src/Data/Unit/Properties.agda b/src/Data/Unit/Properties.agda index 576e24c7dc..05cf0fbb94 100644 --- a/src/Data/Unit/Properties.agda +++ b/src/Data/Unit/Properties.agda @@ -8,16 +8,19 @@ module Data.Unit.Properties where -open import Data.Sum.Base -open import Data.Unit.Base +open import Data.Sum.Base using (inj₁) +open import Data.Unit.Base using (⊤) open import Level using (0ℓ) -open import Relation.Nullary +open import Relation.Nullary using (Irrelevant; yes) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Poset; DecTotalOrder) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) open import Relation.Binary.Definitions using (DecidableEquality; Total; Antisymmetric) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; trans) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid; isEquivalence) ------------------------------------------------------------------------ -- Irrelevancy diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index addfc32678..954f56c0d3 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -9,7 +9,8 @@ module Data.Vec.Functional.Properties where open import Data.Empty using (⊥-elim) -open import Data.Fin.Base +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ<; reduce≥; + _↑ˡ_; _↑ʳ_; punchIn; punchOut) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) import Data.Nat.Properties as ℕ open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) @@ -18,11 +19,15 @@ import Data.List.Properties as List open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Data.Vec.Base as Vec using (Vec) import Data.Vec.Properties as Vec -open import Data.Vec.Functional -open import Function.Base +open import Data.Vec.Functional using (Vector; head; tail; updateAt; + map; _++_; insertAt; removeAt; toVec; fromVec; toList; fromList) +open import Function.Base using (_∘_; id) open import Level using (Level) open import Relation.Binary.Definitions using (DecidableEquality; Decidable) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≗_; refl; _≢_; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Nullary.Decidable using (Dec; does; yes; no; map′; _×-dec_) diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda index 445f96be90..83d65ab5bb 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -12,11 +12,14 @@ open import Level using (Level) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Data.Nat.Base using (ℕ) open import Data.Fin.Permutation using (id; flip; _⟨$⟩ʳ_; inverseʳ; _∘ₚ_) -open import Data.Vec.Functional -open import Data.Vec.Functional.Relation.Binary.Permutation -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; trans; cong; module ≡-Reasoning) +open import Data.Vec.Functional using (Vector) +open import Data.Vec.Functional.Relation.Binary.Permutation using (_↭_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; trans; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Binary.Indexed.Heterogeneous + using (Reflexive; Symmetric; Transitive; IsIndexedEquivalence; IndexedSetoid) private variable diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 66752c65e7..bea3cfea95 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -14,7 +14,8 @@ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_) open import Data.List.Base as List using (List) import Data.List.Properties as List -open import Data.Nat.Base +open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s) open import Function.Base using (id; _∘_) open import Level using (Level; _⊔_) open import Relation.Binary.Core using (Rel; _⇒_) -open import Relation.Binary.Definitions as B +import Relation.Binary.Definitions as B open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_) open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_; map′) diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda index 8e1fe54b4f..dc78ff30d3 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda @@ -8,13 +8,13 @@ module Data.Vec.Relation.Unary.Unique.Propositional.Properties where -open import Data.Vec.Base +open import Data.Vec.Base using (Vec; map; take; drop; tabulate; lookup) open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs) -open import Data.Vec.Relation.Unary.Unique.Propositional +open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique) import Data.Vec.Relation.Unary.Unique.Setoid.Properties as Setoid -open import Data.Fin.Base using(Fin) -open import Data.Nat.Base +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (_+_) open import Data.Nat.Properties using (<⇒≢) open import Data.Product.Base using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡) @@ -22,10 +22,11 @@ open import Function.Base using (id; _∘_) open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality - using (refl; _≡_; _≢_; sym; setoid) +open import Relation.Binary.PropositionalEquality.Core + using (refl; _≡_; _≢_; sym) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) private variable diff --git a/src/Data/Word/Base.agda b/src/Data/Word/Base.agda index f0dddc1e2c..161502e4e9 100644 --- a/src/Data/Word/Base.agda +++ b/src/Data/Word/Base.agda @@ -12,7 +12,7 @@ open import Level using (zero) import Data.Nat.Base as ℕ open import Function.Base using (_on_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_) ------------------------------------------------------------------------ -- Re-export built-ins publicly diff --git a/src/Data/Word/Properties.agda b/src/Data/Word/Properties.agda index e0c2308909..2681d6ce15 100644 --- a/src/Data/Word/Properties.agda +++ b/src/Data/Word/Properties.agda @@ -10,16 +10,18 @@ module Data.Word.Properties where import Data.Nat.Base as ℕ open import Data.Bool.Base using (Bool) -open import Data.Word.Base +open import Data.Word.Base using (_≈_; toℕ; Word64; _<_) import Data.Nat.Properties as ℕ -open import Function.Base -open import Relation.Nullary.Decidable using (map′; ⌊_⌋) +open import Relation.Nullary.Decidable.Core using (map′; ⌊_⌋) open import Relation.Binary using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence ; Setoid; DecSetoid; StrictTotalOrder) import Relation.Binary.Construct.On as On -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid) ------------------------------------------------------------------------ -- Primitive properties diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda index 7a46fb38a8..6e4ed0ffb0 100644 --- a/src/Effect/Monad/Predicate.agda +++ b/src/Effect/Monad/Predicate.agda @@ -10,15 +10,12 @@ module Effect.Monad.Predicate where -open import Effect.Applicative.Indexed -open import Effect.Monad -open import Effect.Monad.Indexed -open import Data.Unit +open import Effect.Monad.Indexed using (RawIMonad) open import Data.Product.Base using (_,_) open import Function.Base using (const; id; _∘_) -open import Level -open import Relation.Binary.PropositionalEquality -open import Relation.Unary +open import Level using (Level; suc; _⊔_) +open import Relation.Binary.PropositionalEquality.Core using (refl) +open import Relation.Unary using (_⊆_; _⇒_; _∈_; _∩_; ｛_｝) open import Relation.Unary.PredicateTransformer using (Pt) private diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 5506f93dd4..e7e9f13db9 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -20,8 +20,8 @@ open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality - using (_≡_; cong; setoid) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) private variable diff --git a/src/Function/Metric/Nat/Bundles.agda b/src/Function/Metric/Nat/Bundles.agda index 57ff945ee0..6623fac24f 100644 --- a/src/Function/Metric/Nat/Bundles.agda +++ b/src/Function/Metric/Nat/Bundles.agda @@ -15,11 +15,11 @@ module Function.Metric.Nat.Bundles where open import Data.Nat.Base hiding (suc; _⊔_) open import Function.Base using (const) open import Level using (Level; suc; _⊔_) -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality - using (_≡_; isEquivalence) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence) -open import Function.Metric.Nat.Core +open import Function.Metric.Nat.Core using (DistanceFunction) open import Function.Metric.Nat.Structures open import Function.Metric.Bundles as Base using (GeneralMetric) diff --git a/src/Function/Metric/Rational/Bundles.agda b/src/Function/Metric/Rational/Bundles.agda index f578a8a8a2..018d26c6df 100644 --- a/src/Function/Metric/Rational/Bundles.agda +++ b/src/Function/Metric/Rational/Bundles.agda @@ -10,20 +10,19 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Rational.Base hiding (_⊔_) +module Function.Metric.Rational.Bundles where + open import Function.Base using (const) open import Level using (Level; suc; _⊔_) -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality - using (_≡_; isEquivalence) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence) -open import Function.Metric.Rational.Core +open import Function.Metric.Rational.Core using (DistanceFunction) open import Function.Metric.Rational.Structures open import Function.Metric.Bundles as Base using (GeneralMetric) -module Function.Metric.Rational.Bundles where - ------------------------------------------------------------------------ -- Proto-metric diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda index aa9c35a0f5..b1962a68c4 100644 --- a/src/Function/Nary/NonDependent.agda +++ b/src/Function/Nary/NonDependent.agda @@ -19,9 +19,11 @@ open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Product.Base using (_×_; _,_) open import Data.Product.Nary.NonDependent + using (Product; uncurryₙ; Equalₙ; curryₙ; fromEqualₙ; toEqualₙ) open import Function.Base using (_∘′_; _$′_; const; flip) open import Relation.Unary using (IUniversal) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; cong) private variable diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 50c84ce3c9..21e295e807 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -8,12 +8,13 @@ module Function.Properties.Bijection where -open import Function.Bundles +open import Function.Bundles using (Bijection; Inverse; Equivalence; + _⤖_; _↔_; _⇔_) open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Trans) -open import Relation.Binary.PropositionalEquality as ≡ using (setoid) +open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) open import Function.Properties.Surjection using (injective⇒to⁻-cong) @@ -37,7 +38,7 @@ refl = Identity.bijection _ -- Can't prove full symmetry as we have no proof that the witness -- produced by the surjection proof preserves equality -sym-≡ : Bijection S (≡.setoid B) → Bijection (≡.setoid B) S +sym-≡ : Bijection S (setoid B) → Bijection (setoid B) S sym-≡ = Symmetry.bijection-≡ trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 99e13c218d..d5e6b8e75d 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -8,15 +8,16 @@ module Function.Properties.Surjection where -open import Function.Base -open import Function.Definitions -open import Function.Bundles +open import Function.Base using (_∘_; _$_) +open import Function.Definitions using (Surjective; Injective; Congruent) +open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; + _⇔_; mk⇔) import Function.Construct.Identity as Identity import Function.Construct.Composition as Compose open import Level using (Level) open import Data.Product.Base using (proj₁; proj₂) -import Relation.Binary.PropositionalEquality as ≡ -open import Relation.Binary.Definitions +import Relation.Binary.PropositionalEquality.Core as ≡ +open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.Bundles using (Setoid) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning diff --git a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda index 4ed89565ae..496ac3d617 100644 --- a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda @@ -10,26 +10,25 @@ -- Relation.Nullary.Construct.Add.Extrema open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Structures - using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder) -open import Relation.Binary.Definitions - using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_) module Relation.Binary.Construct.Add.Extrema.Strict {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where open import Level -open import Function.Base -open import Relation.Nullary hiding (Irrelevant) +open import Function.Base using (_∘′_) import Relation.Nullary.Construct.Add.Infimum as I open import Relation.Nullary.Construct.Add.Extrema -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Construct.Add.Infimum.Strict as AddInfimum import Relation.Binary.Construct.Add.Supremum.Strict as AddSupremum import Relation.Binary.Construct.Add.Extrema.Equality as Equality import Relation.Binary.Construct.Add.Extrema.NonStrict as NonStrict +open import Relation.Binary.Definitions + using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_) +open import Relation.Binary.Structures + using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder) ------------------------------------------------------------------------ -- Definition diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda index ee4078a75c..899be634a1 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda @@ -13,8 +13,8 @@ module open import Function.Base using (_∋_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Construct.Closure.ReflexiveTransitive -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; _◅_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) ------------------------------------------------------------------------ -- Equality diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Core.agda b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda index 1015ef5449..a58276ad32 100644 --- a/src/Relation/Binary/Indexed/Heterogeneous/Core.agda +++ b/src/Relation/Binary/Indexed/Heterogeneous/Core.agda @@ -13,7 +13,6 @@ module Relation.Binary.Indexed.Heterogeneous.Core where open import Level import Relation.Binary.Core as B -import Relation.Binary.Definitions as B ------------------------------------------------------------------------ -- Indexed binary relations diff --git a/src/Relation/Binary/Rewriting.agda b/src/Relation/Binary/Rewriting.agda index 903ab9018e..de63347546 100644 --- a/src/Relation/Binary/Rewriting.agda +++ b/src/Relation/Binary/Rewriting.agda @@ -11,19 +11,19 @@ module Relation.Binary.Rewriting where open import Agda.Builtin.Equality using (_≡_ ; refl) open import Data.Product.Base using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂) -open import Data.Empty +open import Data.Empty using (⊥-elim) open import Function.Base using (flip) -open import Induction.WellFounded -open import Level -open import Relation.Binary.Core +open import Induction.WellFounded using (WellFounded; Acc; acc) +open import Relation.Binary.Core using (REL; Rel) open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure) open import Relation.Binary.Construct.Closure.Equivalence.Properties -open import Relation.Binary.Construct.Closure.Reflexive + using (a—↠b&a—↠c⇒b↔c) open import Relation.Binary.Construct.Closure.ReflexiveTransitive -open import Relation.Binary.Construct.Closure.Symmetric + using (Star; _◅_; ε; _◅◅_) +open import Relation.Binary.Construct.Closure.Symmetric using (fwd; bwd) open import Relation.Binary.Construct.Closure.Transitive -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary + using (Plus; [_]; _∼⁺⟨_⟩_) +open import Relation.Nullary.Negation.Core using (¬_) -- The following definitions are taken from Klop [5] module _ {a ℓ} {A : Set a} (_⟶_ : Rel A ℓ) where diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda index 1f42ef708c..1b27fae60a 100644 --- a/src/Tactic/RingSolver/Core/NatSet.agda +++ b/src/Tactic/RingSolver/Core/NatSet.agda @@ -41,7 +41,8 @@ open import Data.List.Base as List using (List; _∷_; []) open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) open import Data.Bool.Base as Bool using (Bool) open import Function.Base using (const; _∘_) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl) ------------------------------------------------------------------------ -- Helper methods diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda index 4a5a210fef..9a157ddda2 100644 --- a/src/Text/Pretty/Core.agda +++ b/src/Text/Pretty/Core.agda @@ -32,13 +32,16 @@ open import Data.Maybe.Relation.Unary.All as Allᴹ using (nothing; just) open import Data.String.Base as String using (String; length; replicate; _++_; unlines) -open import Data.String.Unsafe as String -open import Function.Base -open import Relation.Nullary.Decidable using (Dec) +import Data.String.Unsafe as String +open import Function.Base using (_∘_; flip; _on_; id; _∘′_; _$_) +open import Relation.Nullary.Decidable.Core using (Dec) open import Relation.Unary using (IUniversal; _⇒_; U) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; cong; cong₂; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) -open import Data.Refinement hiding (map) +open import Data.Refinement using (Refinement-syntax; _,_; value; proof) import Data.Refinement.Relation.Unary.All as Allᴿ ------------------------------------------------------------------------ @@ -148,7 +151,7 @@ private size-pad : maybe′ length 0 pad ≡ x.lastWidth size-pad with x.lastWidth ... | 0 = refl - ... | l@(suc _) = length-replicate l + ... | l@(suc _) = String.length-replicate l indent : Maybe String → String → String indent = maybe′ _++_ id @@ -156,7 +159,7 @@ private size-indent : ∀ ma str → length (indent ma str) ≡ maybe′ length 0 ma + length str size-indent nothing str = refl - size-indent (just pad) str = length-++ pad str + size-indent (just pad) str = String.length-++ pad str indents : Maybe String → Tree String ⊤ → Tree String ⊤ indents = maybe′ (mapₙ ∘ _++_) id @@ -217,7 +220,7 @@ private length vLast ≡ lastWidth isLastLine ∣x∣ ∣y∣ with blocky ... | nothing = begin - length (lastx ++ lasty) ≡⟨ length-++ lastx lasty ⟩ + length (lastx ++ lasty) ≡⟨ String.length-++ lastx lasty ⟩ length lastx + length lasty ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩ x.lastWidth + y.lastWidth ∎ where open ≡-Reasoning ... | just (hd , tl) = begin @@ -256,7 +259,7 @@ private middle : length (lastx ++ hd) ≤ vMaxWidth middle = begin - length (lastx ++ hd) ≡⟨ length-++ lastx hd ⟩ + length (lastx ++ hd) ≡⟨ String.length-++ lastx hd ⟩ length lastx + length hd ≡⟨ cong (_+ _) ∣x∣≡ ⟩ x.lastWidth + length hd ≤⟨ +-monoʳ-≤ x.lastWidth ∣hd∣ ⟩ x.lastWidth + widthy ≤⟨ m≤n⊔m _ _ ⟩ diff --git a/src/Text/Regex/Properties/Core.agda b/src/Text/Regex/Properties/Core.agda index 51097a7656..40e1cdf15b 100644 --- a/src/Text/Regex/Properties/Core.agda +++ b/src/Text/Regex/Properties/Core.agda @@ -23,13 +23,13 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_) open import Text.Regex.Base P -open import Data.List.Relation.Ternary.Appending.Propositional {A = A} open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A} + using (++[]⁻¹; []++⁻¹; conicalˡ; conicalʳ) ------------------------------------------------------------------------ -- Views