Skip to content

Commit 68b2bbf

Browse files
jmougeotjmougeot
authored
Natural Choice Import (#2598)
* Natural Choice * remove long line * cleaning import
1 parent 982fcae commit 68b2bbf

File tree

7 files changed

+39
-40
lines changed

7 files changed

+39
-40
lines changed

‎src/Algebra/Construct/Add/Identity.agda

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

1010
module Algebra.Construct.Add.Identity where
1111

12-
open import Algebra.Bundles
12+
open import Algebra.Bundles using (Semigroup; Monoid)
1313
open import Algebra.Core using (Op₂)
1414
open import Algebra.Definitions
15-
open import Algebra.Structures
15+
using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
16+
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
1617
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
1718
open import Data.Product.Base using (_,_)
1819
open import Level using (Level; _⊔_)
19-
open import Relation.Binary.Core
20-
open import Relation.Binary.Definitions
21-
open import Relation.Binary.Structures
22-
open import Relation.Nullary.Construct.Add.Point
20+
open import Relation.Binary.Core using (Rel)
21+
open import Relation.Binary.Definitions using (Reflexive)
22+
open import Relation.Binary.Structures using (IsEquivalence)
23+
open import Relation.Nullary.Construct.Add.Point using (Pointed; [_]; ∙)
2324

2425
private
2526
variable
@@ -101,3 +102,4 @@ monoid : Semigroup a (a ⊔ ℓ) → Monoid a (a ⊔ ℓ)
101102
monoid S = record
102103
{ isMonoid = isMonoid S.isSemigroup
103104
} where module S = Semigroup S
105+

‎src/Algebra/Construct/NaturalChoice/Base.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
10+
open import Algebra.Core using (Op₂)
1111
open import Level as L hiding (_⊔_)
1212
open import Function.Base using (flip)
1313
open import Relation.Binary.Bundles using (TotalPreorder)

‎src/Algebra/Construct/NaturalChoice/Max.agda

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,8 @@ open import Relation.Binary.Bundles using (TotalOrder)
1111
module Algebra.Construct.NaturalChoice.Max
1212
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
1313

14-
open import Algebra.Core
15-
open import Algebra.Definitions
16-
open import Algebra.Construct.NaturalChoice.Base
14+
open import Algebra.Core using (Op₂)
15+
open import Algebra.Construct.NaturalChoice.Base using (MaxOperator)
1716
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
1817
renaming (totalOrder to flip)
1918

‎src/Algebra/Construct/NaturalChoice/MaxOp.agda

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,21 +7,21 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
11-
open import Algebra.Construct.NaturalChoice.Base
12-
import Algebra.Construct.NaturalChoice.MinOp as MinOp
13-
open import Function.Base using (flip)
14-
open import Relation.Binary.Core using (_Preserves_⟶_)
10+
open import Algebra.Construct.NaturalChoice.Base using (MaxOperator; MaxOp⇒MinOp)
1511
open import Relation.Binary.Bundles using (TotalPreorder)
16-
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
17-
renaming (totalPreorder to flipOrder)
1812

1913
module Algebra.Construct.NaturalChoice.MaxOp
2014
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
2115
where
2216

23-
open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
17+
import Algebra.Construct.NaturalChoice.MinOp as MinOp
18+
open import Algebra.Core using (Op₂)
19+
open import Function.Base using (flip)
2420
open MaxOperator maxOp
21+
open import Relation.Binary.Core using (_Preserves_⟶_)
22+
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
23+
renaming (totalPreorder to flipOrder)
24+
open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
2525

2626
-- Max is just min with a flipped order
2727

‎src/Algebra/Construct/NaturalChoice/Min.agda

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,18 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Core
10-
open import Algebra.Bundles
11-
open import Algebra.Construct.NaturalChoice.Base
12-
open import Data.Sum.Base using (inj₁; inj₂; [_,_])
13-
open import Data.Product.Base using (_,_)
14-
open import Function.Base using (id)
159
open import Relation.Binary.Bundles using (TotalOrder)
16-
import Algebra.Construct.NaturalChoice.MinOp as MinOp
1710

1811
module Algebra.Construct.NaturalChoice.Min
1912
{a ℓ₁ ℓ₂} (O : TotalOrder a ℓ₁ ℓ₂)
2013
where
2114

15+
open import Algebra.Core using (Op₂)
16+
open import Algebra.Construct.NaturalChoice.Base
17+
import Algebra.Construct.NaturalChoice.MinOp as MinOp
18+
open import Data.Sum.Base using (inj₁; inj₂; [_,_])
19+
open import Data.Product.Base using (_,_)
20+
open import Function.Base using (id)
2221
open TotalOrder O renaming (Carrier to A)
2322

2423
------------------------------------------------------------------------

‎src/Algebra/Construct/NaturalChoice/MinMaxOp.agda

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,22 +7,20 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
11-
open import Algebra.Bundles
12-
open import Algebra.Construct.NaturalChoice.Base
13-
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
14-
open import Data.Product.Base using (_,_)
15-
open import Function.Base using (id; _∘_; flip)
16-
open import Relation.Binary.Core using (_Preserves_⟶_)
10+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator)
1711
open import Relation.Binary.Bundles using (TotalPreorder)
18-
open import Relation.Binary.Consequences
1912

2013
module Algebra.Construct.NaturalChoice.MinMaxOp
2114
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂}
2215
(minOp : MinOperator O)
2316
(maxOp : MaxOperator O)
2417
where
2518

19+
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
20+
open import Data.Product.Base using (_,_)
21+
open import Function.Base using (id; _∘_; flip)
22+
open import Relation.Binary.Core using (_Preserves_⟶_)
23+
2624
open TotalPreorder O renaming
2725
( Carrier to A
2826
; _≲_ to _≤_

‎src/Algebra/Construct/NaturalChoice/MinOp.agda

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,19 +7,20 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
10+
open import Relation.Binary.Bundles using (TotalPreorder)
11+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MinOp⇒MaxOp)
12+
13+
module Algebra.Construct.NaturalChoice.MinOp
14+
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where
15+
16+
open import Algebra.Core using (Op₂)
1117
open import Algebra.Bundles
12-
open import Algebra.Construct.NaturalChoice.Base
18+
using (RawMagma; Magma; Semigroup; Band; CommutativeSemigroup; SelectiveMagma; Monoid)
1319
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
1420
open import Data.Product.Base using (_,_)
1521
open import Function.Base using (id; _∘_)
1622
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
17-
open import Relation.Binary.Bundles using (TotalPreorder)
1823
open import Relation.Binary.Definitions using (Maximum; Minimum)
19-
open import Relation.Binary.Consequences
20-
21-
module Algebra.Construct.NaturalChoice.MinOp
22-
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where
2324

2425
open TotalPreorder O renaming
2526
( Carrier to A

0 commit comments

Comments
 (0)