Skip to content

Commit e3d290b

Browse files
jmougeotjmougeot
committed
...
1 parent 35142dc commit e3d290b

File tree

22 files changed

+91
-62
lines changed

22 files changed

+91
-62
lines changed

‎src/Data/Parity/Properties.agda‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,11 @@ open import Algebra.Bundles
1212
open import Data.Nat.Base as ℕ using (zero; suc; parity)
1313
open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; fromSign)
1414
open import Data.Product.Base using (_,_)
15-
import Data.Sign.Base as 𝕊
15+
open import Data.Sign.Base as 𝕊
16+
using (Sign; +; -; _*_; opposite; *-rawMagma; *-1-rawMonoid; *-1-rawGroup)
1617
open import Function.Base using (_$_; id)
1718
open import Function.Definitions
19+
using (Injective; Surjective; Inverseʳ; Inverseˡ)
1820
open import Function.Consequences.Propositional
1921
using (inverseʳ⇒injective; inverseˡ⇒surjective)
2022
open import Level using (0ℓ)
@@ -24,7 +26,7 @@ open import Relation.Binary.PropositionalEquality.Core
2426
using (_≡_; _≢_; refl; sym; cong; cong₂)
2527
open import Relation.Binary.PropositionalEquality.Properties
2628
using (module ≡-Reasoning; setoid; isEquivalence; decSetoid; isDecEquivalence)
27-
open import Relation.Nullary using (yes; no)
29+
open import Relation.Nullary.Decidable.Core using (yes; no)
2830
open import Relation.Nullary.Negation.Core using (contradiction)
2931

3032
open import Algebra.Structures {A = Parity} _≡_

‎src/Data/Product/Algebra.agda‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,24 @@
88

99
module Data.Product.Algebra where
1010

11-
open import Algebra
11+
open import Algebra.Bundles
12+
using (Magma; Semigroup; Monoid; CommutativeMonoid; CommutativeSemiring)
13+
open import Algebra.Definitions
14+
open import Algebra.Structures
15+
using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid
16+
; IsSemiringWithoutAnnihilatingZero; IsSemiring; IsCommutativeSemiring)
1217
open import Data.Bool.Base using (true; false)
1318
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
1419
open import Data.Product.Base
1520
open import Data.Product.Properties
1621
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
17-
open import Data.Sum.Algebra
22+
open import Data.Sum.Algebra using (⊎-isCommutativeMonoid)
1823
open import Data.Unit.Polymorphic using (⊤; tt)
1924
open import Function.Base using (_∘′_)
2025
open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)
2126
open import Function.Properties.Inverse using (↔-isEquivalence)
2227
open import Level using (Level; suc)
23-
open import Relation.Binary.PropositionalEquality.Core
28+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong′; cong₂)
2429

2530
import Function.Definitions as FuncDef
2631

‎src/Data/Product/Effectful/Examples.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ open import Effect.Monad using (RawMonad)
1717
open import Data.Product.Base using (_×_; _,_)
1818
open import Data.Product.Relation.Binary.Pointwise.NonDependent
1919
open import Function.Base using (id)
20-
import Function.Identity.Effectful as Id
2120
open import Relation.Binary.Core using (Rel)
2221
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
2322

‎src/Data/Product/Effectful/Left.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,11 @@ open import Level
1818
module Data.Product.Effectful.Left
1919
{a e} (A : RawMonoid a e) (b : Level) where
2020

21-
open import Data.Product.Base
22-
import Data.Product.Effectful.Left.Base as Base
21+
open import Data.Product.Base using (_,_; map₁; map₂; zip; uncurry)
22+
import Data.Product.Effectful.Left.Base as Base using (Productₗ; functor)
2323
open import Effect.Applicative using (RawApplicative)
2424
open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
2525
open import Function.Base using (id; flip; _∘_; _∘′_)
26-
import Function.Identity.Effectful as Id
2726

2827
open RawMonoid A
2928

‎src/Data/Product/Effectful/Right.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,11 @@ open import Level
1818
module Data.Product.Effectful.Right
1919
(a : Level) {b e} (B : RawMonoid b e) where
2020

21-
open import Data.Product.Base
22-
import Data.Product.Effectful.Right.Base as Base
21+
open import Data.Product.Base using (_,_; map₁; map₂; zip; uncurry)
22+
import Data.Product.Effectful.Right.Base as Base using (Productᵣ; functor)
2323
open import Effect.Applicative using (RawApplicative)
2424
open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
2525
open import Function.Base using (id; flip; _∘_; _∘′_)
26-
import Function.Identity.Effectful as Id
2726

2827
open RawMonoid B
2928

‎src/Data/Product/Function/Dependent/Propositional/WithK.agda‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,17 @@
99

1010
module Data.Product.Function.Dependent.Propositional.WithK where
1111

12-
open import Data.Product.Base
13-
open import Data.Product.Properties
12+
open import Data.Product.Base using (Σ; _,_)
1413
open import Data.Product.Function.Dependent.Setoid using (injection)
15-
open import Data.Product.Relation.Binary.Pointwise.Dependent
1614
open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
15+
using (Pointwise-≡↔≡)
16+
open import Function.Base using (_$_)
17+
open import Function.Bundles using (Injection; _↣_)
18+
open import Function.Properties.Injection using (↣-trans)
19+
open import Function.Properties.Inverse as Inverse using (Inverse⇒Injection)
1720
open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_)
18-
open import Relation.Binary.HeterogeneousEquality as H
21+
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; ≡↔≅)
1922
open import Level using (Level)
20-
open import Function
21-
open import Function.Properties.Injection
22-
open import Function.Properties.Inverse as Inverse
2323

2424
private
2525
variable

‎src/Data/Product/Instances.agda‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,13 @@
88

99
module Data.Product.Instances where
1010

11-
open import Data.Product.Base
12-
using (Σ)
13-
open import Data.Product.Properties
14-
open import Level
11+
open import Data.Product.Base using (Σ)
12+
open import Data.Product.Properties using (≡-dec)
13+
open import Level using (Level)
1514
open import Relation.Binary.PropositionalEquality.Properties
1615
using (isDecEquivalence)
17-
open import Relation.Binary.PropositionalEquality.Core
18-
using (_≡_)
19-
open import Relation.Binary.Structures
20-
using (IsDecEquivalence)
16+
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
17+
open import Relation.Binary.Structures using (IsDecEquivalence)
2118
open import Relation.Binary.TypeClasses
2219

2320
private

‎src/Data/Product/Nary/NonDependent.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module Data.Product.Nary.NonDependent where
1515
------------------------------------------------------------------------
1616

1717
open import Level using (Level)
18-
open import Agda.Builtin.Unit
18+
open import Agda.Builtin.Unit using (⊤)
1919
open import Data.Product.Base as Prod
2020
import Data.Product.Properties as Prodₚ
2121
open import Data.Sum.Base using (_⊎_)

‎src/Data/Product/Relation/Binary/Lex/NonStrict.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ open import Relation.Binary.Bundles
2020
open import Relation.Binary.Structures
2121
using (IsPartialOrder; IsEquivalence; IsTotalOrder; IsDecTotalOrder)
2222
open import Relation.Binary.Definitions
23-
using (Transitive; Symmetric; Decidable; Antisymmetric; Total; Trichotomous; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈)
23+
using (Transitive; Symmetric; Decidable; Antisymmetric; Total; Trichotomous
24+
; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈)
2425
open import Relation.Binary.Consequences
2526
import Relation.Binary.Construct.NonStrictToStrict as Conv
2627
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise

‎src/Data/Product/Relation/Binary/Lex/Strict.agda‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,19 +15,21 @@ open import Data.Product.Base
1515
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
1616
using (Pointwise)
1717
open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
18-
open import Data.Empty
19-
open import Function.Base
20-
open import Induction.WellFounded
21-
open import Level
22-
open import Relation.Nullary.Decidable
18+
open import Data.Empty using (⊥-elim)
19+
open import Function.Base using (flip; _on_; _$_; _∘_)
20+
open import Induction.WellFounded using (Acc; acc; WfRec; WellFounded; Acc-resp-flip-≈)
21+
open import Level using (Level)
22+
open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
2323
open import Relation.Binary.Core using (Rel; _⇒_)
2424
open import Relation.Binary.Bundles
2525
using (Preorder; StrictPartialOrder; StrictTotalOrder)
2626
open import Relation.Binary.Structures
2727
using (IsEquivalence; IsPreorder; IsStrictPartialOrder; IsStrictTotalOrder)
2828
open import Relation.Binary.Definitions
29-
using (Transitive; Symmetric; Irreflexive; Asymmetric; Total; Decidable; Antisymmetric; Trichotomous; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri>; tri≈)
30-
open import Relation.Binary.Consequences
29+
using (Transitive; Symmetric; Irreflexive; Asymmetric; Total; Decidable
30+
; Antisymmetric; Trichotomous; _Respects₂_; _Respectsʳ_; _Respectsˡ_
31+
; tri<; tri>; tri≈)
32+
open import Relation.Binary.Consequences using (asym⇒irr)
3133
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
3234

3335
private

0 commit comments

Comments
 (0)