Skip to content

Commit 3d8323c

Browse files
jamesmckinnajamesmckinna
authored
Merge branch 'master' into issue2502-v2.3
2 parents 796f156 + 4871f37 commit 3d8323c

File tree

538 files changed

+2442
-1801
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

538 files changed

+2442
-1801
lines changed

‎CHANGELOG.md

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,9 @@ Non-backwards compatible changes
2828
Minor improvements
2929
------------------
3030

31+
* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
32+
to its own dedicated module `Relation.Nullary.Irrelevant`.
33+
3134
Deprecated modules
3235
------------------
3336

@@ -58,18 +61,29 @@ Deprecated names
5861
∤∤-respˡ-≈ ↦ ∦-respˡ-≈
5962
∤∤-respʳ-≈ ↦ ∦-respʳ-≈
6063
∤∤-resp-≈ ↦ ∦-resp-≈
64+
∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈
65+
∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈
66+
∣-resp-≈ ↦ ∣ʳ-resp-≈
67+
x∣yx ↦ x∣ʳyx
68+
xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz
6169
```
6270

6371
* In `Algebra.Properties.Monoid.Divisibility`:
6472
```agda
6573
∣∣-refl ↦ ∥-refl
6674
∣∣-reflexive ↦ ∥-reflexive
6775
∣∣-isEquivalence ↦ ∥-isEquivalence
76+
ε∣_ ↦ ε∣ʳ_
77+
∣-refl ↦ ∣ʳ-refl
78+
∣-reflexive ↦ ∣ʳ-reflexive
79+
∣-isPreorder ↦ ∣ʳ-isPreorder
80+
∣-preorder ↦ ∣ʳ-preorder
6881
```
6982

7083
* In `Algebra.Properties.Semigroup.Divisibility`:
7184
```agda
7285
∣∣-trans ↦ ∥-trans
86+
∣-trans ↦ ∣ʳ-trans
7387
```
7488

7589
* In `Algebra.Structures`:
@@ -109,6 +123,12 @@ New modules
109123

110124
* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
111125

126+
* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid.
127+
128+
* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
129+
130+
* `Data.Sign.Show` to show a sign
131+
112132
Additions to existing modules
113133
-----------------------------
114134

@@ -141,6 +161,38 @@ Additions to existing modules
141161
commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
142162
```
143163

164+
* In `Algebra.Properties.Magma.Divisibility`:
165+
```agda
166+
∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_
167+
∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_
168+
∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_
169+
x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y
170+
xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
171+
```
172+
173+
* In `Algebra.Properties.Monoid.Divisibility`:
174+
```agda
175+
ε∣ˡ_ : ∀ x → ε ∣ˡ x
176+
∣ˡ-refl : Reflexive _∣ˡ_
177+
∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_
178+
∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
179+
∣ˡ-preorder : Preorder a ℓ _
180+
```
181+
182+
* In `Algebra.Properties.Semigroup.Divisibility`:
183+
```agda
184+
∣ˡ-trans : Transitive _∣ˡ_
185+
x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y
186+
x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
187+
x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
188+
x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z
189+
```
190+
191+
* In `Algebra.Properties.CommutativeSemigroup.Divisibility`:
192+
```agda
193+
∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
194+
```
195+
144196
* In `Data.List.Properties`:
145197
```agda
146198
map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
@@ -153,3 +205,9 @@ Additions to existing modules
153205
```agda
154206
filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
155207
```
208+
209+
* In `Relation.Nullary.Decidable.Core`:
210+
```agda
211+
⊤-dec : Dec {a} ⊤
212+
⊥-dec : Dec {a} ⊥
213+
```

‎src/Algebra/Apartness/Bundles.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open import Relation.Binary.Core using (Rel)
1313
open import Relation.Binary.Bundles using (ApartnessRelation)
1414
open import Algebra.Core using (Op₁; Op₂)
1515
open import Algebra.Bundles using (CommutativeRing)
16-
open import Algebra.Apartness.Structures
16+
open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField)
1717

1818
record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
1919
infix 8 -_

‎src/Algebra/Bundles/Raw.agda

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,10 @@
88

99
module Algebra.Bundles.Raw where
1010

11-
open import Algebra.Core
11+
open import Algebra.Core using (Op₁; Op₂)
1212
open import Relation.Binary.Core using (Rel)
1313
open import Relation.Binary.Bundles.Raw using (RawSetoid)
1414
open import Level using (suc; _⊔_)
15-
open import Relation.Nullary.Negation.Core using (¬_)
1615

1716
------------------------------------------------------------------------
1817
-- Raw bundles with 1 unary operation & 1 element

‎src/Algebra/Consequences/Base.agda

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,11 @@
1010
module Algebra.Consequences.Base
1111
{a} {A : Set a} where
1212

13-
open import Algebra.Core
13+
open import Algebra.Core using (Op₁; Op₂)
1414
open import Algebra.Definitions
15-
open import Data.Sum.Base
16-
open import Relation.Binary.Core
15+
using (Selective; Idempotent; SelfInverse; Involutive)
16+
open import Data.Sum.Base using (_⊎_; reduce)
17+
open import Relation.Binary.Core using (Rel)
1718
open import Relation.Binary.Definitions using (Reflexive)
1819

1920
module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where

‎src/Algebra/Consequences/Propositional.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ open import Relation.Binary.PropositionalEquality.Core
1919
open import Relation.Binary.PropositionalEquality.Properties
2020
using (setoid)
2121
open import Relation.Unary using (Pred)
22+
open import Algebra.Core using (Op₁; Op₂)
2223

23-
open import Algebra.Core
2424
open import Algebra.Definitions {A = A} _≡_
2525
import Algebra.Consequences.Setoid (setoid A) as Base
2626

‎src/Algebra/Consequences/Setoid.agda

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

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

10-
open import Relation.Binary.Core using (Rel)
1110
open import Relation.Binary.Bundles using (Setoid)
1211
open import Relation.Binary.Definitions
1312
using (Substitutive; Symmetric; Total)
@@ -22,6 +21,7 @@ open import Data.Product.Base using (_,_)
2221
open import Function.Base using (_$_; id; _∘_)
2322
open import Function.Definitions
2423
import Relation.Binary.Consequences as Bin
24+
open import Relation.Binary.Core using (Rel)
2525
open import Relation.Binary.Reasoning.Setoid S
2626
open import Relation.Unary using (Pred)
2727

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ open import Algebra.Core using (Op₂)
1414
open import Algebra.Definitions
1515
using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
1616
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
17-
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
1817
open import Data.Product.Base using (_,_)
1918
open import Level using (Level; _⊔_)
19+
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
2020
open import Relation.Binary.Core using (Rel)
2121
open import Relation.Binary.Definitions using (Reflexive)
2222
open import Relation.Binary.Structures using (IsEquivalence)

‎src/Algebra/Lattice/Bundles.agda

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,14 @@
1515

1616
module Algebra.Lattice.Bundles where
1717

18-
open import Algebra.Core
19-
open import Algebra.Bundles
20-
open import Algebra.Structures
18+
open import Algebra.Core using (Op₁; Op₂)
19+
open import Algebra.Bundles using (Band)
2120
import Algebra.Lattice.Bundles.Raw as Raw
2221
open import Algebra.Lattice.Structures
22+
using ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
23+
; IsBoundedSemilattice; IsBoundedMeetSemilattice
24+
; IsBoundedJoinSemilattice; IsLattice; IsDistributiveLattice
25+
; IsBooleanAlgebra)
2326
open import Level using (suc; _⊔_)
2427
open import Relation.Binary.Bundles using (Setoid)
2528
open import Relation.Binary.Core using (Rel)

‎src/Algebra/Lattice/Construct/DirectProduct.agda

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -13,15 +13,14 @@
1313

1414
{-# OPTIONS --cubical-compatible --safe #-}
1515

16-
open import Algebra
17-
open import Algebra.Lattice
16+
module Algebra.Lattice.Construct.DirectProduct where
17+
18+
open import Algebra using (Band)
19+
open import Algebra.Lattice using (Semilattice)
1820
import Algebra.Construct.DirectProduct as DirectProduct
1921
open import Data.Product.Base using (_,_; _<*>_)
20-
open import Data.Product.Relation.Binary.Pointwise.NonDependent
2122
open import Level using (Level; _⊔_)
2223

23-
module Algebra.Lattice.Construct.DirectProduct where
24-
2524
private
2625
variable
2726
a b ℓ₁ ℓ₂ : Level

‎src/Algebra/Lattice/Construct/LiftedChoice.agda

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,16 @@
66

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

9+
module Algebra.Lattice.Construct.LiftedChoice where
10+
911
open import Algebra
10-
open import Algebra.Lattice
11-
open import Algebra.Construct.LiftedChoice
12+
using (Op₂; IsSelectiveMagma; Associative; Commutative)
13+
open import Algebra.Lattice.Structures using (IsSemilattice)
14+
open import Algebra.Construct.LiftedChoice using (Lift; isBand; comm)
1215
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
1316
open import Relation.Binary.Structures using (IsEquivalence)
1417
open import Level using (Level)
1518

16-
module Algebra.Lattice.Construct.LiftedChoice where
17-
1819
private
1920
variable
2021
a b p ℓ : Level

‎src/Algebra/Lattice/Construct/Subst/Equality.agda

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

1010
{-# OPTIONS --cubical-compatible --safe #-}
1111

12-
open import Algebra.Core using (Op₂)
13-
open import Algebra.Definitions
14-
open import Algebra.Lattice.Structures
1512
open import Data.Product.Base using (_,_)
16-
open import Function.Base
17-
open import Relation.Binary.Core
13+
open import Relation.Binary.Core using (Rel ; _⇔_)
1814

1915
module Algebra.Lattice.Construct.Subst.Equality
2016
{a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
2117
(equiv@(to , from) : ≈₁ ⇔ ≈₂)
2218
where
2319

20+
open import Algebra.Core using (Op₂)
21+
open import Algebra.Lattice.Structures
22+
using (IsSemilattice ;IsLattice ;IsDistributiveLattice ;IsBooleanAlgebra )
23+
open import Function.Base using (id)
2424
open import Algebra.Construct.Subst.Equality equiv
2525
open import Relation.Binary.Construct.Subst.Equality equiv
2626

‎src/Algebra/Lattice/Construct/Zero.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ open import Level using (Level)
1717

1818
module Algebra.Lattice.Construct.Zero {c ℓ : Level} where
1919

20-
open import Algebra.Lattice.Bundles
21-
open import Data.Unit.Polymorphic
20+
open import Algebra.Lattice.Bundles using (Semilattice)
21+
open import Data.Unit.Polymorphic using (⊤)
2222

2323
------------------------------------------------------------------------
2424
-- Bundles

‎src/Algebra/Lattice/Structures.agda

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

1414
{-# OPTIONS --cubical-compatible --safe #-}
1515

16-
open import Algebra.Core
16+
open import Algebra.Core using (Op₁; Op₂)
1717
open import Data.Product.Base using (proj₁; proj₂)
1818
open import Level using (_⊔_)
1919
open import Relation.Binary.Core using (Rel)

‎src/Algebra/Module/Bundles.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,15 +26,15 @@
2626
module Algebra.Module.Bundles where
2727

2828
open import Algebra.Bundles
29-
using (Semiring; Ring; CommutativeSemiring; CommutativeRing;
30-
CommutativeMonoid; AbelianGroup)
29+
using (Semiring; Ring; CommutativeSemiring; CommutativeRing
30+
; CommutativeMonoid; AbelianGroup)
3131
open import Algebra.Core using (Op₁; Op₂)
3232
open import Algebra.Definitions using (Involutive)
3333
import Algebra.Module.Bundles.Raw as Raw
3434
open import Algebra.Module.Core using (Opₗ; Opᵣ)
3535
open import Algebra.Module.Structures
36-
using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule;
37-
IsSemimodule; IsLeftModule; IsRightModule; IsModule; IsBimodule)
36+
using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule
37+
; IsSemimodule; IsLeftModule; IsRightModule; IsModule; IsBimodule)
3838
open import Algebra.Module.Definitions
3939
open import Function.Base using (flip)
4040
open import Level using (Level; _⊔_; suc)

‎src/Algebra/Module/Bundles/Raw.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
module Algebra.Module.Bundles.Raw where
1010

11-
open import Algebra.Bundles.Raw
12-
open import Algebra.Core
13-
open import Algebra.Module.Core
14-
open import Level
11+
open import Algebra.Bundles.Raw using (RawMonoid; RawGroup)
12+
open import Algebra.Core using (Op₁; Op₂)
13+
open import Algebra.Module.Core using (Opₗ; Opᵣ)
14+
open import Level using (Level; _⊔_; suc)
1515
open import Relation.Nullary.Negation.Core using (¬_)
1616
open import Relation.Binary.Core using (Rel)
1717

‎src/Algebra/Module/Construct/DirectProduct.agda

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,12 @@
1212
module Algebra.Module.Construct.DirectProduct where
1313

1414
open import Algebra.Bundles
15-
open import Algebra.Construct.DirectProduct
15+
open import Algebra.Construct.DirectProduct using (commutativeMonoid)
1616
open import Algebra.Module.Bundles
1717
open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
1818
open import Data.Product.Relation.Binary.Pointwise.NonDependent
19-
open import Level
19+
using (Pointwise)
20+
open import Level using (Level; _⊔_)
2021

2122
private
2223
variable

‎src/Algebra/Module/Construct/Idealization.agda

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,11 +37,13 @@ open import Algebra.Module.Bundles using (Bimodule)
3737
module Algebra.Module.Construct.Idealization
3838
{r ℓr m ℓm} (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where
3939

40-
open import Algebra.Core
41-
import Algebra.Consequences.Setoid as Consequences
40+
open import Algebra.Core using (Op₂)
41+
import Algebra.Consequences.Setoid as Consequences using (comm∧assoc⇒middleFour)
4242
import Algebra.Definitions as Definitions
43-
import Algebra.Module.Construct.DirectProduct as DirectProduct
44-
import Algebra.Module.Construct.TensorUnit as TensorUnit
43+
using (Congruent₂; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_
44+
; LeftIdentity; RightIdentity; Identity; Associative)
45+
import Algebra.Module.Construct.DirectProduct as DirectProduct using (bimodule)
46+
import Algebra.Module.Construct.TensorUnit as TensorUnit using (bimodule)
4547
open import Algebra.Structures using (IsAbelianGroup; IsRing)
4648
open import Data.Product.Base using (_,_; ∃-syntax)
4749
open import Level using (Level; _⊔_)

‎src/Algebra/Module/Construct/TensorUnit.agda

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,14 @@
1212
module Algebra.Module.Construct.TensorUnit where
1313

1414
open import Algebra.Bundles
15+
using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring
16+
; CommutativeRing)
1517
open import Algebra.Module.Bundles
16-
open import Level
18+
using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule
19+
; RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule
20+
; RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule
21+
; Module)
22+
open import Level using (Level; _⊔_)
1723

1824
private
1925
variable

‎src/Algebra/Module/Construct/Zero.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,13 @@
1010

1111
{-# OPTIONS --cubical-compatible --safe #-}
1212

13-
open import Level
13+
open import Level using (Level)
1414

1515
module Algebra.Module.Construct.Zero {c ℓ : Level} where
1616

17-
open import Algebra.Bundles
17+
open import Algebra.Bundles using (RawSemiring; Semiring; Ring; CommutativeSemiring; CommutativeRing)
1818
open import Algebra.Module.Bundles
19-
open import Data.Unit.Polymorphic
19+
open import Data.Unit.Polymorphic using (⊤)
2020
open import Relation.Binary.Core using (Rel)
2121

2222
private

‎src/Algebra/Module/Definitions/Bi/Simultaneous.agda

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

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

9-
open import Relation.Binary using (Rel)
9+
open import Relation.Binary.Core using (Rel)
1010

1111
module Algebra.Module.Definitions.Bi.Simultaneous
1212
{a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)

0 commit comments

Comments
 (0)