diff --git a/CHANGELOG.md b/CHANGELOG.md
index 468a6e6915..895cbe789c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,11 @@ Non-backwards compatible changes
Minor improvements
------------------
+* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The module
+ `Algebra.Consequences.Base` now takes the underlying equality relation as
+ an additional top-level parameter, with slightly improved ergonomics wrt
+ subsequent imports by clients, as well as streamlined internals.
+
Deprecated modules
------------------
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 574ad48a16..2cedb9a5aa 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -7,26 +7,34 @@
{-# OPTIONS --cubical-compatible --safe #-}
+open import Relation.Binary.Core using (Rel)
+
module Algebra.Consequences.Base
- {a} {A : Set a} where
+ {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
-open import Algebra.Core
-open import Algebra.Definitions
-open import Data.Sum.Base
-open import Relation.Binary.Core
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Definitions _≈_
+open import Data.Sum.Base using (reduce)
open import Relation.Binary.Definitions using (Reflexive)
-module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
+private
+ variable
+ f : Op₁ A
+ _∙_ : Op₂ A
+
+------------------------------------------------------------------------
+-- Selective
- sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
- sel⇒idem sel x = reduce (sel x x)
+sel⇒idem : Selective _∙_ → Idempotent _∙_
+sel⇒idem sel x = reduce (sel x x)
+
+------------------------------------------------------------------------
+-- SelfInverse
-module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
+reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse f →
+ Involutive f
+reflexive∧selfInverse⇒involutive refl inv _ = inv refl
- reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
- SelfInverse _≈_ f →
- Involutive _≈_ f
- reflexive∧selfInverse⇒involutive refl inv _ = inv refl
------------------------------------------------------------------------
-- DEPRECATED NAMES
diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 29490cbd0c..14451e6e3e 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -20,10 +20,17 @@ open import Relation.Binary.PropositionalEquality.Properties
using (setoid)
open import Relation.Unary using (Pred)
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Definitions {A = A} _≡_
import Algebra.Consequences.Setoid (setoid A) as Base
+private
+ variable
+ e ε 0# : A
+ f _⁻¹ -_ : Op₁ A
+ _∙_ _◦_ _+_ _*_ : Op₂ A
+
+
------------------------------------------------------------------------
-- Re-export all proofs that don't require congruence or substitutivity
@@ -41,7 +48,6 @@ open Base public
; comm⇒sym[distribˡ]
; subst∧comm⇒sym
; wlog
- ; sel⇒idem
-- plus all the deprecated versions of the above
; comm+assoc⇒middleFour
; identity+middleFour⇒assoc
@@ -58,39 +64,35 @@ open Base public
------------------------------------------------------------------------
-- Group-like structures
-module _ {_∙_ _⁻¹ ε} where
-
- assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
- RightInverse ε _⁻¹ _∙_ →
- ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
- assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
+assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
+ RightInverse ε _⁻¹ _∙_ →
+ ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
+assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
- assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
- LeftInverse ε _⁻¹ _∙_ →
- ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
- assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
+assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
+ LeftInverse ε _⁻¹ _∙_ →
+ ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
+assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
------------------------------------------------------------------------
-- Ring-like structures
-module _ {_+_ _*_ -_ 0#} where
+assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
+ RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
+ LeftZero 0# _*_
+assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {_+_ = _+_} {_*_ = _*_} =
+ Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
- assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
- RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
- LeftZero 0# _*_
- assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ =
- Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
-
- assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
- RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
- RightZero 0# _*_
- assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ =
- Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
+assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
+ RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
+ RightZero 0# _*_
+assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {_+_ = _+_} {_*_ = _*_} =
+ Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
------------------------------------------------------------------------
-- Bisemigroup-like structures
-module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
+module _ (∙-comm : Commutative _∙_) where
comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
@@ -99,49 +101,37 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm
comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
- comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
+ comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _) ∙-comm
------------------------------------------------------------------------
--- Selectivity
-
-module _ {_∙_ : Op₂ A} where
-
- sel⇒idem : Selective _∙_ → Idempotent _∙_
- sel⇒idem = Base.sel⇒idem _≡_
-
-------------------------------------------------------------------------
--- Middle-Four Exchange
-
-module _ {_∙_ : Op₂ A} where
+-- MiddleFourExchange
- comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
- _∙_ MiddleFourExchange _∙_
- comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)
+comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
+ _∙_ MiddleFourExchange _∙_
+comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _)
- identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
- _∙_ MiddleFourExchange _∙_ →
- Associative _∙_
- identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
+identity∧middleFour⇒assoc : Identity e _∙_ →
+ _∙_ MiddleFourExchange _∙_ →
+ Associative _∙_
+identity∧middleFour⇒assoc {_∙_ = _∙_} = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
- identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
- _∙_ MiddleFourExchange _+_ →
- Commutative _∙_
- identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_)
+identity∧middleFour⇒comm : Identity e _+_ →
+ _∙_ MiddleFourExchange _+_ →
+ Commutative _∙_
+identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _)
------------------------------------------------------------------------
-- Without Loss of Generality
-module _ {p} {P : Pred A p} where
+module _ {p} {P : Pred A p} (∙-comm : Commutative _∙_) where
- subst∧comm⇒sym : ∀ {f} (f-comm : Commutative f) →
- Symmetric (λ a b → P (f a b))
- subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst
+ subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
+ subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst ∙-comm
- wlog : ∀ {f} (f-comm : Commutative f) →
- ∀ {r} {_R_ : Rel _ r} → Total _R_ →
- (∀ a b → a R b → P (f a b)) →
- ∀ a b → P (f a b)
- wlog = Base.wlog {P = P} subst
+ wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
+ (∀ a b → a R b → P (a ∙ b)) →
+ ∀ a b → P (a ∙ b)
+ wlog = Base.wlog {P = P} subst ∙-comm
------------------------------------------------------------------------
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 66e441a9e0..304bd8e004 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -7,10 +7,7 @@
{-# OPTIONS --cubical-compatible --safe #-}
-open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions
- using (Substitutive; Symmetric; Total)
module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
@@ -21,47 +18,55 @@ open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Product.Base using (_,_)
open import Function.Base using (_$_; id; _∘_)
open import Function.Definitions
-import Relation.Binary.Consequences as Bin
+import Relation.Binary.Consequences as BinaryConsequences
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+ using (Substitutive; Symmetric; Total)
open import Relation.Binary.Reasoning.Setoid S
open import Relation.Unary using (Pred)
+private
+ variable
+ e 0# : A
+ f _⁻¹ : Op₁ A
+ _∙_ _◦_ _+_ _*_ : Op₂ A
+
------------------------------------------------------------------------
-- Re-exports
-- Export base lemmas that don't require the setoid
-open import Algebra.Consequences.Base public
+open import Algebra.Consequences.Base _≈_ public
------------------------------------------------------------------------
-- MiddleFourExchange
-module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
+module _ (cong : Congruent₂ _∙_) where
comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
_∙_ MiddleFourExchange _∙_
comm∧assoc⇒middleFour comm assoc w x y z = begin
(w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
- w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
+ w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (assoc x y z) ⟨
w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
- w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
+ w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
(w ∙ y) ∙ (x ∙ z) ∎
- identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
- _∙_ MiddleFourExchange _∙_ →
+ identity∧middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ →
Associative _∙_
- identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
- (x ∙ y) ∙ z ≈⟨ cong refl (sym (identityˡ z)) ⟩
+ identity∧middleFour⇒assoc {e = e} (identityˡ , identityʳ) middleFour x y z
+ = begin
+ (x ∙ y) ∙ z ≈⟨ cong refl (identityˡ z) ⟨
(x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
(x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
x ∙ (y ∙ z) ∎
- identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
- _∙_ MiddleFourExchange _+_ →
+ identity∧middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ →
Commutative _∙_
- identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
+ identity∧middleFour⇒comm {e = e} {_+_ = _+_} (identityˡ , identityʳ) middleFour x y
= begin
- x ∙ y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+ x ∙ y ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
(e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
(e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
y ∙ x ∎
@@ -69,12 +74,12 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
------------------------------------------------------------------------
-- SelfInverse
-module _ {f : Op₁ A} (self : SelfInverse f) where
+module _ (self : SelfInverse f) where
selfInverse⇒involutive : Involutive f
- selfInverse⇒involutive = reflexive∧selfInverse⇒involutive _≈_ refl self
+ selfInverse⇒involutive = reflexive∧selfInverse⇒involutive refl self
- selfInverse⇒congruent : Congruent _≈_ _≈_ f
+ selfInverse⇒congruent : Congruent₁ f
selfInverse⇒congruent {x} {y} x≈y = sym (self (begin
f (f x) ≈⟨ selfInverse⇒involutive x ⟩
x ≈⟨ x≈y ⟩
@@ -98,7 +103,7 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
------------------------------------------------------------------------
-- Magma-like structures
-module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
+module _ (comm : Commutative _∙_) where
comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
@@ -117,16 +122,16 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
------------------------------------------------------------------------
-- Monoid-like structures
-module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
+module _ (comm : Commutative _∙_) where
comm∧idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_
- comm∧idˡ⇒idʳ idˡ x = begin
+ comm∧idˡ⇒idʳ {e = e} idˡ x = begin
x ∙ e ≈⟨ comm x e ⟩
e ∙ x ≈⟨ idˡ x ⟩
x ∎
comm∧idʳ⇒idˡ : RightIdentity e _∙_ → LeftIdentity e _∙_
- comm∧idʳ⇒idˡ idʳ x = begin
+ comm∧idʳ⇒idˡ {e = e} idʳ x = begin
e ∙ x ≈⟨ comm e x ⟩
x ∙ e ≈⟨ idʳ x ⟩
x ∎
@@ -138,13 +143,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
comm∧idʳ⇒id idʳ = comm∧idʳ⇒idˡ idʳ , idʳ
comm∧zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_
- comm∧zeˡ⇒zeʳ zeˡ x = begin
+ comm∧zeˡ⇒zeʳ {e = e} zeˡ x = begin
x ∙ e ≈⟨ comm x e ⟩
e ∙ x ≈⟨ zeˡ x ⟩
e ∎
comm∧zeʳ⇒zeˡ : RightZero e _∙_ → LeftZero e _∙_
- comm∧zeʳ⇒zeˡ zeʳ x = begin
+ comm∧zeʳ⇒zeˡ {e = e} zeʳ x = begin
e ∙ x ≈⟨ comm e x ⟩
x ∙ e ≈⟨ zeʳ x ⟩
e ∎
@@ -157,7 +162,7 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
AlmostRightCancellative e _∙_
- comm∧almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
+ comm∧almostCancelˡ⇒almostCancelʳ {e = e} cancelˡ-nonZero x y z x≉e yx≈zx =
cancelˡ-nonZero x y z x≉e $ begin
x ∙ y ≈⟨ comm x y ⟩
y ∙ x ≈⟨ yx≈zx ⟩
@@ -166,7 +171,7 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
AlmostLeftCancellative e _∙_
- comm∧almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
+ comm∧almostCancelʳ⇒almostCancelˡ {e = e} cancelʳ-nonZero x y z x≉e xy≈xz =
cancelʳ-nonZero x y z x≉e $ begin
y ∙ x ≈⟨ comm y x ⟩
x ∙ y ≈⟨ xy≈xz ⟩
@@ -176,10 +181,10 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
------------------------------------------------------------------------
-- Group-like structures
-module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where
+module _ (comm : Commutative _∙_) where
comm∧invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_
- comm∧invˡ⇒invʳ invˡ x = begin
+ comm∧invˡ⇒invʳ {e = e} {_⁻¹ = _⁻¹} invˡ x = begin
x ∙ (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
(x ⁻¹) ∙ x ≈⟨ invˡ x ⟩
e ∎
@@ -188,7 +193,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
comm∧invˡ⇒inv invˡ = invˡ , comm∧invˡ⇒invʳ invˡ
comm∧invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_
- comm∧invʳ⇒invˡ invʳ x = begin
+ comm∧invʳ⇒invˡ {e = e} {_⁻¹ = _⁻¹} invʳ x = begin
(x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩
x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩
e ∎
@@ -196,15 +201,15 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
comm∧invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm∧invʳ⇒inv invʳ = comm∧invʳ⇒invˡ invʳ , invʳ
-module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
+module _ (cong : Congruent₂ _∙_) where
assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
- assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
- x ≈⟨ sym (idʳ x) ⟩
+ assoc∧id∧invʳ⇒invˡ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invʳ x y eq = begin
+ x ≈⟨ idʳ x ⟨
x ∙ e ≈⟨ cong refl (sym (invʳ y)) ⟩
- x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
+ x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
(x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩
y ⁻¹ ∎
@@ -212,9 +217,9 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh
assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ →
Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
- assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
- y ≈⟨ sym (idˡ y) ⟩
- e ∙ y ≈⟨ cong (sym (invˡ x)) refl ⟩
+ assoc∧id∧invˡ⇒invʳ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invˡ x y eq = begin
+ y ≈⟨ idˡ y ⟨
+ e ∙ y ≈⟨ cong (invˡ x) refl ⟨
((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
(x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
(x ⁻¹) ∙ e ≈⟨ idʳ (x ⁻¹) ⟩
@@ -223,10 +228,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh
------------------------------------------------------------------------
-- Bisemigroup-like structures
-module _ {_∙_ _◦_ : Op₂ A}
- (◦-cong : Congruent₂ _◦_)
- (∙-comm : Commutative _∙_)
- where
+module _ (◦-cong : Congruent₂ _◦_) (∙-comm : Commutative _∙_) where
comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
comm∧distrˡ⇒distrʳ distrˡ x y z = begin
@@ -256,8 +258,7 @@ module _ {_∙_ _◦_ : Op₂ A}
(x ◦ z) ∙ (x ◦ y) ∎
-module _ {_∙_ _◦_ : Op₂ A}
- (∙-cong : Congruent₂ _∙_)
+module _ (∙-cong : Congruent₂ _∙_)
(∙-assoc : Associative _∙_)
(◦-comm : Commutative _◦_)
where
@@ -278,20 +279,17 @@ module _ {_∙_ _◦_ : Op₂ A}
------------------------------------------------------------------------
-- Ring-like structures
-module _ {_+_ _*_ : Op₂ A}
- {_⁻¹ : Op₁ A} {0# : A}
- (+-cong : Congruent₂ _+_)
- (*-cong : Congruent₂ _*_)
- where
+module _ (+-cong : Congruent₂ _+_) (*-cong : Congruent₂ _*_) where
assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
LeftZero 0# _*_
- assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin
- 0# * x ≈⟨ sym (idʳ _) ⟩
+ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribʳ idʳ invʳ x
+ = begin
+ 0# * x ≈⟨ idʳ _ ⟨
(0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩
- (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩
- ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
+ (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
+ ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (distribʳ _ _ _) refl ⟨
((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
(0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩
0# ∎
@@ -299,11 +297,12 @@ module _ {_+_ _*_ : Op₂ A}
assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
RightZero 0# _*_
- assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin
- x * 0# ≈⟨ sym (idʳ _) ⟩
+ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribˡ idʳ invʳ x
+ = begin
+ x * 0# ≈⟨ idʳ _ ⟨
(x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩
- (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩
- ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
+ (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
+ ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (distribˡ _ _ _) refl ⟨
(x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩
0# ∎
@@ -311,18 +310,18 @@ module _ {_+_ _*_ : Op₂ A}
------------------------------------------------------------------------
-- Without Loss of Generality
-module _ {p} {f : Op₂ A} {P : Pred A p}
+module _ {p} {P : Pred A p}
(≈-subst : Substitutive _≈_ p)
- (comm : Commutative f)
+ (∙-comm : Commutative _∙_)
where
- subst∧comm⇒sym : Symmetric (λ a b → P (f a b))
- subst∧comm⇒sym = ≈-subst P (comm _ _)
+ subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b))
+ subst∧comm⇒sym = ≈-subst P (∙-comm _ _)
wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
- (∀ a b → a R b → P (f a b)) →
- ∀ a b → P (f a b)
- wlog r-total = Bin.wlog r-total subst∧comm⇒sym
+ (∀ a b → a R b → P (a ∙ b)) →
+ ∀ a b → P (a ∙ b)
+ wlog r-total = BinaryConsequences.wlog r-total subst∧comm⇒sym
------------------------------------------------------------------------