Skip to content

Commit b58fc90

Browse files
jamesmckinnaMatthewDaggitt
jamesmckinna
and
MatthewDaggitt
authored
[ refactor ] Restate, and use, the definitions of Monotonic etc. operations (#2580)
* refactor: use the definitions! * add: `LeftMonotonic` and `RightMonotonic` * refactor: systematise `Congruence` reasoning * fix: knock-on DRY * fix: `CHANGELOG` plus cosmetics * refactor: change implicit to explicit * fix: make `CHANGELOG` more detailed * refactor: rectify the names * refactor: use the new definitions * refactor: use the new definitions some more * refactor: use the new definitions some more * refactor: unsolved metas make this a pain! * refactor: use the new definitions * refactor: use the new definitions * refactor: use the new lemma statements; not yet their generic proofs * add: missing redefinitions * refactor: use new lemma * refactor: one more use of `Monotonic₁` * refactor: `Congruent` in terms of `Monotonic` * refactor: de-nest `module Congruence` * fix: tighten `import`s * fix: make relation arguments explicit * fix: explicit imports * fix: parameterisation of proofs * fix: parameterisation of `mono` proofs * Removed comments --------- Co-authored-by: MatthewDaggitt <[email protected]>
1 parent 77fed0b commit b58fc90

File tree

13 files changed

+267
-179
lines changed

13 files changed

+267
-179
lines changed

‎CHANGELOG.md

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,21 @@ New modules
186186
Additions to existing modules
187187
-----------------------------
188188

189+
* In `Algebra.Consequences.Base`:
190+
```agda
191+
module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
192+
where
193+
∙-congˡ : LeftCongruent _≈_ _∙_
194+
∙-congʳ : RightCongruent _≈_ _∙_
195+
```
196+
197+
* In `Algebra.Consequences.Setoid`:
198+
```agda
199+
module Congruence (cong : Congruent₂ _≈_ _∙_) where
200+
∙-congˡ : LeftCongruent _≈_ _∙_
201+
∙-congʳ : RightCongruent _≈_ _∙_
202+
```
203+
189204
* In `Algebra.Construct.Pointwise`:
190205
```agda
191206
isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
@@ -447,13 +462,28 @@ Additions to existing modules
447462
sreplicate : ∀ n → Set a → Sets n (lreplicate n a)
448463
```
449464

465+
* In `Relation.Binary.Consequences`:
466+
```agda
467+
mono₂⇒monoˡ : Reflexive ≤₁ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
468+
mono₂⇒monoˡ : Reflexive ≤₂ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
469+
monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ →
470+
LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
471+
Monotonic₂ ≤₁ ≤₂ ≤₃ f
472+
```
473+
450474
* In `Relation.Binary.Construct.Add.Infimum.Strict`:
451475
```agda
452476
<₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
453477
<₋-accessible[_] : Acc _<_ x → Acc _<₋_ [ x ]
454478
<₋-wellFounded : WellFounded _<_ → WellFounded _<₋_
455479
```
456480

481+
* In `Relation.Binary.Definitions`:
482+
```agda
483+
LeftMonotonic : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
484+
RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
485+
```
486+
457487
* In `Relation.Nullary.Decidable`:
458488
```agda
459489
dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)

‎src/Algebra/Consequences/Base.agda

Lines changed: 20 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,22 +11,35 @@ module Algebra.Consequences.Base
1111
{a} {A : Set a} where
1212

1313
open import Algebra.Core using (Op₁; Op₂)
14-
open import Algebra.Definitions
15-
using (Selective; Idempotent; SelfInverse; Involutive)
14+
import Algebra.Definitions as Definitions
15+
using (Congruent₂; LeftCongruent; RightCongruent
16+
; Selective; Idempotent; SelfInverse; Involutive)
1617
open import Data.Sum.Base using (_⊎_; reduce)
18+
open import Relation.Binary.Consequences
19+
using (mono₂⇒monoˡ; mono₂⇒monoʳ)
1720
open import Relation.Binary.Core using (Rel)
1821
open import Relation.Binary.Definitions using (Reflexive)
1922

20-
module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
23+
module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_)
24+
(cong : Congruent₂ _∙_) (refl : Reflexive _≈_)
25+
where
2126

22-
sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
27+
∙-congˡ : LeftCongruent _∙_
28+
∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x
29+
30+
∙-congʳ : RightCongruent _∙_
31+
∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x
32+
33+
module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
34+
35+
sel⇒idem : Selective _∙_ → Idempotent _∙_
2336
sel⇒idem sel x = reduce (sel x x)
2437

25-
module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
38+
module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
2639

2740
reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
28-
SelfInverse _≈_ f →
29-
Involutive _≈_ f
41+
SelfInverse f →
42+
Involutive f
3043
reflexive∧selfInverse⇒involutive refl inv _ = inv refl
3144

3245
------------------------------------------------------------------------

‎src/Algebra/Consequences/Propositional.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
module Algebra.Consequences.Propositional
1111
{a} {A : Set a} where
1212

13+
open import Algebra.Core using (Op₁; Op₂)
1314
open import Data.Sum.Base using (inj₁; inj₂)
1415
open import Relation.Binary.Core using (Rel)
1516
open import Relation.Binary.Bundles using (Setoid)
@@ -19,7 +20,6 @@ open import Relation.Binary.PropositionalEquality.Core
1920
open import Relation.Binary.PropositionalEquality.Properties
2021
using (setoid)
2122
open import Relation.Unary using (Pred)
22-
open import Algebra.Core using (Op₁; Op₂)
2323

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

‎src/Algebra/Consequences/Setoid.agda

Lines changed: 54 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -13,55 +13,66 @@ open import Relation.Binary.Definitions
1313

1414
module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
1515

16-
open Setoid S renaming (Carrier to A)
16+
import Algebra.Consequences.Base as Base
1717
open import Algebra.Core
18-
open import Algebra.Definitions _≈_
1918
open import Data.Sum.Base using (inj₁; inj₂)
2019
open import Data.Product.Base using (_,_)
2120
open import Function.Base using (_$_; id; _∘_)
2221
open import Function.Definitions
2322
import Relation.Binary.Consequences as Bin
2423
open import Relation.Binary.Core using (Rel)
25-
open import Relation.Binary.Reasoning.Setoid S
2624
open import Relation.Unary using (Pred)
2725

26+
open Setoid S renaming (Carrier to A)
27+
open import Algebra.Definitions _≈_
28+
open import Relation.Binary.Reasoning.Setoid S
29+
2830
------------------------------------------------------------------------
2931
-- Re-exports
3032

3133
-- Export base lemmas that don't require the setoid
3234

33-
open import Algebra.Consequences.Base public
35+
open Base public
36+
hiding (module Congruence)
37+
38+
-- Export congruence lemmas using reflexivity
39+
40+
module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
41+
42+
open Base.Congruence _≈_ cong refl public
3443

3544
------------------------------------------------------------------------
3645
-- MiddleFourExchange
3746

3847
module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
3948

49+
open Congruence cong
50+
4051
comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
4152
_∙_ MiddleFourExchange _∙_
4253
comm∧assoc⇒middleFour comm assoc w x y z = begin
4354
(w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
44-
w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
45-
w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
46-
w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
47-
w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
55+
w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (assoc x y z) ⟨
56+
w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
57+
w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
58+
w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
4859
(w ∙ y) ∙ (x ∙ z) ∎
4960

5061
identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
5162
_∙_ MiddleFourExchange _∙_ →
5263
Associative _∙_
5364
identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
54-
(x ∙ y) ∙ z ≈⟨ cong refl (sym (identityˡ z)) ⟩
65+
(x ∙ y) ∙ z ≈⟨ ∙-congˡ (identityˡ z) ⟨
5566
(x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
56-
(x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
67+
(x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩
5768
x ∙ (y ∙ z) ∎
5869

5970
identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
6071
_∙_ MiddleFourExchange _+_ →
6172
Commutative _∙_
6273
identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
6374
= begin
64-
x ∙ y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
75+
x ∙ y ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
6576
(e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
6677
(e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
6778
y ∙ x ∎
@@ -198,25 +209,27 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
198209

199210
module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
200211

212+
open Congruence cong
213+
201214
assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
202215
Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
203216
∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
204217
assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
205-
x ≈⟨ sym (idʳ x) ⟩
206-
x ∙ e ≈⟨ cong refl (sym (invʳ y)) ⟩
207-
x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
208-
(x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
218+
x ≈⟨ idʳ x ⟨
219+
x ∙ e ≈⟨ ∙-congˡ (invʳ y) ⟨
220+
x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
221+
(x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩
209222
e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩
210223
y ⁻¹ ∎
211224

212225
assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ →
213226
Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
214227
∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
215228
assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
216-
y ≈⟨ sym (idˡ y) ⟩
217-
e ∙ y ≈⟨ cong (sym (invˡ x)) refl ⟩
229+
y ≈⟨ idˡ y ⟨
230+
e ∙ y ≈⟨ ∙-congʳ (invˡ x) ⟨
218231
((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
219-
(x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
232+
(x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
220233
(x ⁻¹) ∙ e ≈⟨ idʳ (x ⁻¹) ⟩
221234
x ⁻¹ ∎
222235

@@ -228,6 +241,8 @@ module _ {_∙_ _◦_ : Op₂ A}
228241
(∙-comm : Commutative _∙_)
229242
where
230243

244+
open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ)
245+
231246
comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
232247
comm∧distrˡ⇒distrʳ distrˡ x y z = begin
233248
(y ◦ z) ∙ x ≈⟨ ∙-comm (y ◦ z) x ⟩
@@ -250,7 +265,7 @@ module _ {_∙_ _◦_ : Op₂ A}
250265

251266
comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z)))
252267
comm⇒sym[distribˡ] x {y} {z} prf = begin
253-
x ◦ (z ∙ y) ≈⟨ ◦-cong refl (∙-comm z y) ⟩
268+
x ◦ (z ∙ y) ≈⟨ ◦-congˡ (∙-comm z y) ⟩
254269
x ◦ (y ∙ z) ≈⟨ prf ⟩
255270
(x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
256271
(x ◦ z) ∙ (x ◦ y) ∎
@@ -262,16 +277,18 @@ module _ {_∙_ _◦_ : Op₂ A}
262277
(◦-comm : Commutative _◦_)
263278
where
264279

280+
open Congruence ∙-cong
281+
265282
distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
266283
_◦_ Absorbs _∙_ →
267284
_◦_ DistributesOver _∙_ →
268285
_∙_ DistributesOverˡ _◦_
269286
distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin
270-
x ∙ (y ◦ z) ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨
271-
(x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩
287+
x ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨
288+
(x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩
272289
(x ∙ (y ◦ x)) ∙ (y ◦ z) ≈⟨ ∙-assoc _ _ _ ⟩
273-
x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨
274-
x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨
290+
x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨
291+
x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨
275292
(x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z)) ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
276293
(x ∙ y) ◦ (x ∙ z) ∎
277294

@@ -284,27 +301,31 @@ module _ {_+_ _*_ : Op₂ A}
284301
(*-cong : Congruent₂ _*_)
285302
where
286303

304+
open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)
305+
306+
open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ)
307+
287308
assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
288309
RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
289310
LeftZero 0# _*_
290311
assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin
291-
0# * x ≈⟨ sym (idʳ _) ⟩
292-
(0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩
293-
(0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩
294-
((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
295-
((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
312+
0# * x ≈⟨ idʳ _ ⟨
313+
(0# * x) + 0# ≈⟨ +-congˡ (invʳ _) ⟨
314+
(0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
315+
((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-congʳ (distribʳ _ _ _) ⟨
316+
((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩
296317
(0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩
297318
0# ∎
298319

299320
assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
300321
RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
301322
RightZero 0# _*_
302323
assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin
303-
x * 0# ≈⟨ sym (idʳ _) ⟩
304-
(x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩
305-
(x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩
306-
((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
307-
(x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
324+
x * 0# ≈⟨ idʳ _ ⟨
325+
(x * 0#) + 0# ≈⟨ +-congˡ (invʳ _) ⟨
326+
(x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
327+
((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ (distribˡ _ _ _) ⟨
328+
(x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩
308329
((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩
309330
0# ∎
310331

‎src/Algebra/Definitions.agda

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,7 @@
1515

1616
{-# OPTIONS --cubical-compatible --safe #-}
1717

18-
open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
19-
open import Relation.Nullary.Negation.Core using (¬_)
18+
open import Relation.Binary.Core using (Rel)
2019

2120
module Algebra.Definitions
2221
{a ℓ} {A : Set a} -- The underlying set
@@ -26,21 +25,24 @@ module Algebra.Definitions
2625
open import Algebra.Core using (Op₁; Op₂)
2726
open import Data.Product.Base using (_×_; ∃-syntax)
2827
open import Data.Sum.Base using (_⊎_)
28+
open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂)
29+
open import Relation.Nullary.Negation.Core using (¬_)
30+
2931

3032
------------------------------------------------------------------------
3133
-- Properties of operations
3234

3335
Congruent₁ : Op₁ A → Set _
34-
Congruent₁ f = f Preserves _≈_ ⟶ _≈_
36+
Congruent₁ = Monotonic₁ _≈_ _≈_
3537

3638
Congruent₂ : Op₂ A → Set _
37-
Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
39+
Congruent₂ = Monotonic₂ _≈_ _≈_ _≈_
3840

3941
LeftCongruent : Op₂ A → Set _
40-
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
42+
LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)
4143

4244
RightCongruent : Op₂ A → Set _
43-
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
45+
RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x)
4446

4547
Associative : Op₂ A → Set _
4648
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

‎src/Algebra/Structures.agda

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -55,12 +55,7 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
5555
setoid : Setoid a ℓ
5656
setoid = record { isEquivalence = isEquivalence }
5757

58-
∙-congˡ : LeftCongruent ∙
59-
∙-congˡ y≈z = ∙-cong refl y≈z
60-
61-
∙-congʳ : RightCongruent ∙
62-
∙-congʳ y≈z = ∙-cong y≈z refl
63-
58+
open Consequences.Congruence setoid ∙-cong public
6459

6560
record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
6661
field

‎src/Data/Fin/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -930,7 +930,7 @@ pinch-surjective _ zero = zero , λ { refl → refl }
930930
pinch-surjective zero (suc j) = suc (suc j) , λ { refl → refl }
931931
pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j)
932932

933-
pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
933+
pinch-mono-≤ : ∀ (i : Fin n) → Monotonic₁ _≤_ _≤_ (pinch i)
934934
pinch-mono-≤ 0F {0F} {k} 0≤n = z≤n
935935
pinch-mono-≤ 0F {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k
936936
pinch-mono-≤ (suc i) {0F} {k} 0≤n = z≤n

0 commit comments

Comments
 (0)