From c2614ed08b0d4d9a7533079095a8b9150d3cc897 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 5 May 2024 10:30:13 +0100
Subject: [PATCH 1/6] Pointwise `Algebra`

---
 CHANGELOG.md                         |   5 +
 src/Algebra/Construct/Pointwise.agda | 224 +++++++++++++++++++++++++++
 2 files changed, 229 insertions(+)
 create mode 100644 src/Algebra/Construct/Pointwise.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5c9cc9037b..70346765e1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -78,6 +78,11 @@ Deprecated names
 New modules
 -----------
 
+* Pointwise algebraic structures and bundles:
+  ```
+  Algebra.Construct.Pointwise
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw
diff --git a/src/Algebra/Construct/Pointwise.agda b/src/Algebra/Construct/Pointwise.agda
new file mode 100644
index 0000000000..364ede5607
--- /dev/null
+++ b/src/Algebra/Construct/Pointwise.agda
@@ -0,0 +1,224 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- For each `IsX` algebraic structure `S`, lift the structure to the
+-- 'pointwise' function space `A → S`: categorically, this is the
+-- *power* object in the relevant category of `X` objects and morphisms
+--
+-- NB the module is parametrised only wrt `A`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Construct.Pointwise {a} (A : Set a) where
+
+open import Algebra.Bundles
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Structures
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _∘′_; const)
+open import Level
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+
+private
+
+  variable
+    c ℓ : Level
+    C : Set c
+    _≈_ : Rel C ℓ
+    ε 0# 1# : C
+    _⁻¹ -_ : Op₁ C
+    _∙_ _+_ _*_ : Op₂ C
+
+  lift₀ : C → A → C
+  lift₀ = const
+
+  lift₁ : Op₁ C → Op₁ (A → C)
+  lift₁ = _∘′_
+
+  lift₂ : Op₂ C → Op₂ (A → C)
+  lift₂ _∙_ g h x = (g x) ∙ (h x)
+
+  liftRel : Rel C ℓ → Rel (A → C) (a ⊔ ℓ)
+  liftRel _≈_ g h = ∀ x → (g x) ≈ (h x)
+
+
+------------------------------------------------------------------------
+-- Setoid structure: here rather than elsewhere? (could be imported?)
+
+module _ (isEquivalenceC : IsEquivalence _≈_) where
+
+  open IsEquivalence isEquivalenceC
+
+  isEquivalence : IsEquivalence (liftRel _≈_)
+  isEquivalence = record
+    { refl = λ {f} x → refl {f x}
+    ; sym = λ f≈g x → sym (f≈g x)
+    ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+    }
+
+------------------------------------------------------------------------
+-- Structures
+
+module _ (isMagmaC : IsMagma _≈_ _∙_) where
+
+  private
+    module M = IsMagma isMagmaC
+
+  isMagma : IsMagma (liftRel _≈_) (lift₂ _∙_)
+  isMagma = record
+    { isEquivalence = isEquivalence M.isEquivalence
+    ; ∙-cong = λ g h x → M.∙-cong (g x) (h x)
+    }
+
+module _ (isSemigroupC : IsSemigroup _≈_ _∙_) where
+
+  private
+    module M = IsSemigroup isSemigroupC
+
+  isSemigroup : IsSemigroup (liftRel _≈_) (lift₂ _∙_)
+  isSemigroup = record
+    { isMagma = isMagma M.isMagma
+    ; assoc = λ f g h x → M.assoc (f x) (g x) (h x)
+    }
+
+module _ (isBandC : IsBand _≈_ _∙_) where
+
+  private
+    module M = IsBand isBandC
+
+  isBand : IsBand (liftRel _≈_) (lift₂ _∙_)
+  isBand = record
+    { isSemigroup = isSemigroup M.isSemigroup
+    ; idem = λ f x → M.idem (f x)
+    }
+
+module _ (isCommutativeSemigroupC : IsCommutativeSemigroup _≈_ _∙_) where
+
+  private
+    module M = IsCommutativeSemigroup isCommutativeSemigroupC
+
+  isCommutativeSemigroup : IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
+  isCommutativeSemigroup = record
+    { isSemigroup = isSemigroup M.isSemigroup
+    ; comm = λ f g x → M.comm (f x) (g x)
+    }
+
+module _ (isMonoidC : IsMonoid _≈_ _∙_ ε) where
+
+  private
+    module M = IsMonoid isMonoidC
+
+  isMonoid : IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+  isMonoid = record
+    { isSemigroup = isSemigroup M.isSemigroup
+    ; identity = (λ f x → M.identityˡ (f x)) , λ f x → M.identityʳ (f x)
+    }
+
+module _ (isCommutativeMonoidC : IsCommutativeMonoid _≈_ _∙_ ε) where
+
+  private
+    module M = IsCommutativeMonoid isCommutativeMonoidC
+
+  isCommutativeMonoid : IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+  isCommutativeMonoid = record
+    { isMonoid = isMonoid M.isMonoid
+    ; comm = λ f g x → M.comm (f x) (g x)
+    }
+
+module _ (isGroupC : IsGroup _≈_ _∙_ ε _⁻¹) where
+
+  private
+    module M = IsGroup isGroupC
+
+  isGroup : IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+  isGroup = record
+    { isMonoid = isMonoid M.isMonoid
+    ; inverse = (λ f x → M.inverseˡ (f x)) , λ f x → M.inverseʳ (f x)
+    ; ⁻¹-cong = λ f x → M.⁻¹-cong (f x)
+    }
+
+module _ (isAbelianGroupC : IsAbelianGroup _≈_ _∙_ ε _⁻¹) where
+
+  private
+    module M = IsAbelianGroup isAbelianGroupC
+
+  isAbelianGroup : IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+  isAbelianGroup = record
+    { isGroup = isGroup M.isGroup
+    ; comm = λ f g x → M.comm (f x) (g x)
+    }
+
+module _ (isSemiringWithoutAnnihilatingZeroC : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#) where
+
+  private
+    module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZeroC
+
+  isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+  isSemiringWithoutAnnihilatingZero = record
+    { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
+    ; *-cong =  λ g h x → M.*-cong (g x) (h x)
+    ; *-assoc =  λ f g h x → M.*-assoc (f x) (g x) (h x)
+    ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
+    ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+    }
+
+module _ (isSemiringC : IsSemiring _≈_ _+_ _*_ 0# 1#) where
+
+  private
+    module M = IsSemiring isSemiringC
+
+  isSemiring : IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+  isSemiring = record
+    { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
+    ; zero = (λ f x → M.zeroˡ (f x)) , λ f x → M.zeroʳ (f x)
+    }
+
+module _ (isRingC : IsRing _≈_ _+_ _*_ -_ 0# 1#) where
+
+  private
+    module M = IsRing isRingC
+
+  isRing : IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
+  isRing = record
+    { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
+    ; *-cong = λ g h x → M.*-cong (g x) (h x)
+    ; *-assoc = λ f g h x → M.*-assoc (f x) (g x) (h x)
+    ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
+    ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+    }
+
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ → Magma (a ⊔ c) (a ⊔ ℓ)
+magma m = record { isMagma = isMagma (Magma.isMagma m) }
+
+semigroup : Semigroup c ℓ → Semigroup (a ⊔ c) (a ⊔ ℓ)
+semigroup m = record { isSemigroup = isSemigroup (Semigroup.isSemigroup m) }
+
+band : Band c ℓ → Band (a ⊔ c) (a ⊔ ℓ)
+band m = record { isBand = isBand (Band.isBand m) }
+
+commutativeSemigroup : CommutativeSemigroup c ℓ → CommutativeSemigroup (a ⊔ c) (a ⊔ ℓ)
+commutativeSemigroup m = record { isCommutativeSemigroup = isCommutativeSemigroup (CommutativeSemigroup.isCommutativeSemigroup m) }
+
+monoid : Monoid c ℓ → Monoid (a ⊔ c) (a ⊔ ℓ)
+monoid m = record { isMonoid = isMonoid (Monoid.isMonoid m) }
+
+group : Group c ℓ → Group (a ⊔ c) (a ⊔ ℓ)
+group m = record { isGroup = isGroup (Group.isGroup m) }
+
+abelianGroup : AbelianGroup c ℓ → AbelianGroup (a ⊔ c) (a ⊔ ℓ)
+abelianGroup m = record { isAbelianGroup = isAbelianGroup (AbelianGroup.isAbelianGroup m) }
+
+semiring : Semiring c ℓ → Semiring (a ⊔ c) (a ⊔ ℓ)
+semiring m = record { isSemiring = isSemiring (Semiring.isSemiring m) }
+
+ring : Ring c ℓ → Ring (a ⊔ c) (a ⊔ ℓ)
+ring m = record { isRing = isRing (Ring.isRing m) }
+

From 507362dcd2c282d85918215163eb82474ae2992f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 6 May 2024 08:02:34 +0100
Subject: [PATCH 2/6] temporary commit

---
 src/Algebra/Construct/Pointwise.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Algebra/Construct/Pointwise.agda b/src/Algebra/Construct/Pointwise.agda
index 364ede5607..b08d8568c3 100644
--- a/src/Algebra/Construct/Pointwise.agda
+++ b/src/Algebra/Construct/Pointwise.agda
@@ -17,6 +17,7 @@ open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Structures
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘′_; const)
+import Function.Relation.Binary.Setoid.Equality as FunctionEquality
 open import Level
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)

From cf7a2c7d326c9fb8d16a79e0494f9eeedb961655 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 6 May 2024 12:02:02 +0100
Subject: [PATCH 3/6] better `CHANGELOG` entry?

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 70346765e1..233096a7aa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -78,7 +78,8 @@ Deprecated names
 New modules
 -----------
 
-* Pointwise algebraic structures and bundles:
+* Pointwise lifting of algebraic structures `IsX` and bundles `X` from
+  carrier set `C` to function space `A → C`:
   ```
   Algebra.Construct.Pointwise
   ```

From dd5ef4ea61c50019a26a228801729fa38ca5a763 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 6 May 2024 12:02:36 +0100
Subject: [PATCH 4/6] begin removing redundant `module` implementation

---
 src/Algebra/Construct/Pointwise.agda | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/Algebra/Construct/Pointwise.agda b/src/Algebra/Construct/Pointwise.agda
index b08d8568c3..3d0a79006e 100644
--- a/src/Algebra/Construct/Pointwise.agda
+++ b/src/Algebra/Construct/Pointwise.agda
@@ -50,16 +50,13 @@ private
 ------------------------------------------------------------------------
 -- Setoid structure: here rather than elsewhere? (could be imported?)
 
-module _ (isEquivalenceC : IsEquivalence _≈_) where
-
-  open IsEquivalence isEquivalenceC
-
-  isEquivalence : IsEquivalence (liftRel _≈_)
-  isEquivalence = record
-    { refl = λ {f} x → refl {f x}
-    ; sym = λ f≈g x → sym (f≈g x)
-    ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
-    }
+isEquivalence : IsEquivalence _≈_ → IsEquivalence (liftRel _≈_)
+isEquivalence isEquivalence = record
+  { refl = λ {f} x → refl {f x}
+  ; sym = λ f≈g x → sym (f≈g x)
+  ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+  }
+  where open IsEquivalence isEquivalence
 
 ------------------------------------------------------------------------
 -- Structures

From ce2c50346cf09ac3929255171784f9490bdeaa47 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 6 May 2024 12:28:26 +0100
Subject: [PATCH 5/6] finish removing redundant `module` implementation

---
 src/Algebra/Construct/Pointwise.agda | 203 +++++++++++----------------
 1 file changed, 83 insertions(+), 120 deletions(-)

diff --git a/src/Algebra/Construct/Pointwise.agda b/src/Algebra/Construct/Pointwise.agda
index 3d0a79006e..6d4ebed804 100644
--- a/src/Algebra/Construct/Pointwise.agda
+++ b/src/Algebra/Construct/Pointwise.agda
@@ -61,133 +61,96 @@ isEquivalence isEquivalence = record
 ------------------------------------------------------------------------
 -- Structures
 
-module _ (isMagmaC : IsMagma _≈_ _∙_) where
-
-  private
-    module M = IsMagma isMagmaC
-
-  isMagma : IsMagma (liftRel _≈_) (lift₂ _∙_)
-  isMagma = record
-    { isEquivalence = isEquivalence M.isEquivalence
-    ; ∙-cong = λ g h x → M.∙-cong (g x) (h x)
-    }
-
-module _ (isSemigroupC : IsSemigroup _≈_ _∙_) where
-
-  private
-    module M = IsSemigroup isSemigroupC
-
-  isSemigroup : IsSemigroup (liftRel _≈_) (lift₂ _∙_)
-  isSemigroup = record
-    { isMagma = isMagma M.isMagma
-    ; assoc = λ f g h x → M.assoc (f x) (g x) (h x)
-    }
-
-module _ (isBandC : IsBand _≈_ _∙_) where
-
-  private
-    module M = IsBand isBandC
-
-  isBand : IsBand (liftRel _≈_) (lift₂ _∙_)
-  isBand = record
-    { isSemigroup = isSemigroup M.isSemigroup
-    ; idem = λ f x → M.idem (f x)
-    }
-
-module _ (isCommutativeSemigroupC : IsCommutativeSemigroup _≈_ _∙_) where
-
-  private
-    module M = IsCommutativeSemigroup isCommutativeSemigroupC
-
-  isCommutativeSemigroup : IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
-  isCommutativeSemigroup = record
-    { isSemigroup = isSemigroup M.isSemigroup
-    ; comm = λ f g x → M.comm (f x) (g x)
-    }
-
-module _ (isMonoidC : IsMonoid _≈_ _∙_ ε) where
-
-  private
-    module M = IsMonoid isMonoidC
-
-  isMonoid : IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
-  isMonoid = record
-    { isSemigroup = isSemigroup M.isSemigroup
-    ; identity = (λ f x → M.identityˡ (f x)) , λ f x → M.identityʳ (f x)
-    }
-
-module _ (isCommutativeMonoidC : IsCommutativeMonoid _≈_ _∙_ ε) where
-
-  private
-    module M = IsCommutativeMonoid isCommutativeMonoidC
-
-  isCommutativeMonoid : IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
-  isCommutativeMonoid = record
-    { isMonoid = isMonoid M.isMonoid
-    ; comm = λ f g x → M.comm (f x) (g x)
-    }
-
-module _ (isGroupC : IsGroup _≈_ _∙_ ε _⁻¹) where
-
-  private
-    module M = IsGroup isGroupC
-
-  isGroup : IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
-  isGroup = record
-    { isMonoid = isMonoid M.isMonoid
-    ; inverse = (λ f x → M.inverseˡ (f x)) , λ f x → M.inverseʳ (f x)
-    ; ⁻¹-cong = λ f x → M.⁻¹-cong (f x)
-    }
-
-module _ (isAbelianGroupC : IsAbelianGroup _≈_ _∙_ ε _⁻¹) where
-
-  private
-    module M = IsAbelianGroup isAbelianGroupC
-
-  isAbelianGroup : IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
-  isAbelianGroup = record
-    { isGroup = isGroup M.isGroup
-    ; comm = λ f g x → M.comm (f x) (g x)
-    }
-
-module _ (isSemiringWithoutAnnihilatingZeroC : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#) where
-
-  private
-    module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZeroC
+isMagma : IsMagma _≈_ _∙_ → IsMagma (liftRel _≈_) (lift₂ _∙_)
+isMagma isMagma = record
+  { isEquivalence = isEquivalence M.isEquivalence
+  ; ∙-cong = λ g h x → M.∙-cong (g x) (h x)
+  }
+  where module M = IsMagma isMagma
 
-  isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
-  isSemiringWithoutAnnihilatingZero = record
-    { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
-    ; *-cong =  λ g h x → M.*-cong (g x) (h x)
-    ; *-assoc =  λ f g h x → M.*-assoc (f x) (g x) (h x)
-    ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
-    ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
-    }
+isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup (liftRel _≈_) (lift₂ _∙_)
+isSemigroup isSemigroup = record
+  { isMagma = isMagma M.isMagma
+  ; assoc = λ f g h x → M.assoc (f x) (g x) (h x)
+  }
+  where module M = IsSemigroup isSemigroup
 
-module _ (isSemiringC : IsSemiring _≈_ _+_ _*_ 0# 1#) where
+isBand : IsBand _≈_ _∙_ → IsBand (liftRel _≈_) (lift₂ _∙_)
+isBand isBand = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; idem = λ f x → M.idem (f x)
+  }
+  where module M = IsBand isBand
 
-  private
-    module M = IsSemiring isSemiringC
+isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ →
+                         IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
+isCommutativeSemigroup isCommutativeSemigroup = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; comm = λ f g x → M.comm (f x) (g x)
+  }
+  where module M = IsCommutativeSemigroup isCommutativeSemigroup
 
-  isSemiring : IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
-  isSemiring = record
-    { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
-    ; zero = (λ f x → M.zeroˡ (f x)) , λ f x → M.zeroʳ (f x)
-    }
+isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+isMonoid isMonoid = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; identity = (λ f x → M.identityˡ (f x)) , λ f x → M.identityʳ (f x)
+  }
+  where module M = IsMonoid isMonoid
 
-module _ (isRingC : IsRing _≈_ _+_ _*_ -_ 0# 1#) where
+isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε →
+                      IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+isCommutativeMonoid isCommutativeMonoid = record
+  { isMonoid = isMonoid M.isMonoid
+  ; comm = λ f g x → M.comm (f x) (g x)
+  }
+  where module M = IsCommutativeMonoid isCommutativeMonoid
+
+isGroup : IsGroup _≈_ _∙_ ε _⁻¹ →
+          IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+isGroup isGroup = record
+  { isMonoid = isMonoid M.isMonoid
+  ; inverse = (λ f x → M.inverseˡ (f x)) , λ f x → M.inverseʳ (f x)
+  ; ⁻¹-cong = λ f x → M.⁻¹-cong (f x)
+  }
+  where module M = IsGroup isGroup
 
-  private
-    module M = IsRing isRingC
+isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹ →
+                 IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+isAbelianGroup isAbelianGroup = record
+  { isGroup = isGroup M.isGroup
+  ; comm = λ f g x → M.comm (f x) (g x)
+  }
+  where module M = IsAbelianGroup isAbelianGroup
+
+isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# →
+  IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
+  { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
+  ; *-cong =  λ g h x → M.*-cong (g x) (h x)
+  ; *-assoc =  λ f g h x → M.*-assoc (f x) (g x) (h x)
+  ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
+  ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+  }
+  where module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero
 
-  isRing : IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
-  isRing = record
-    { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
-    ; *-cong = λ g h x → M.*-cong (g x) (h x)
-    ; *-assoc = λ f g h x → M.*-assoc (f x) (g x) (h x)
-    ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
-    ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
-    }
+isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1# →
+             IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+isSemiring isSemiring = record
+  { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
+  ; zero = (λ f x → M.zeroˡ (f x)) , λ f x → M.zeroʳ (f x)
+  }
+  where module M = IsSemiring isSemiring
+
+isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
+         IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
+isRing isRing = record
+  { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
+  ; *-cong = λ g h x → M.*-cong (g x) (h x)
+  ; *-assoc = λ f g h x → M.*-assoc (f x) (g x) (h x)
+  ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
+  ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+  }
+  where module M = IsRing isRing
 
 
 ------------------------------------------------------------------------

From c27d46e10ba30c7224f108e78bcf34b6b89feff4 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 6 May 2024 13:59:01 +0100
Subject: [PATCH 6/6] make `liftRel` implicitly quantified

---
 src/Algebra/Construct/Pointwise.agda | 45 ++++++++++++++--------------
 1 file changed, 22 insertions(+), 23 deletions(-)

diff --git a/src/Algebra/Construct/Pointwise.agda b/src/Algebra/Construct/Pointwise.agda
index 6d4ebed804..842e36b1ed 100644
--- a/src/Algebra/Construct/Pointwise.agda
+++ b/src/Algebra/Construct/Pointwise.agda
@@ -17,7 +17,6 @@ open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Structures
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘′_; const)
-import Function.Relation.Binary.Setoid.Equality as FunctionEquality
 open import Level
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
@@ -44,7 +43,7 @@ private
   lift₂ _∙_ g h x = (g x) ∙ (h x)
 
   liftRel : Rel C ℓ → Rel (A → C) (a ⊔ ℓ)
-  liftRel _≈_ g h = ∀ x → (g x) ≈ (h x)
+  liftRel _≈_ g h = ∀ {x} → (g x) ≈ (h x)
 
 
 ------------------------------------------------------------------------
@@ -52,9 +51,9 @@ private
 
 isEquivalence : IsEquivalence _≈_ → IsEquivalence (liftRel _≈_)
 isEquivalence isEquivalence = record
-  { refl = λ {f} x → refl {f x}
-  ; sym = λ f≈g x → sym (f≈g x)
-  ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+  { refl = λ {f x} → refl {f x}
+  ; sym = λ f≈g → sym f≈g
+  ; trans = λ f≈g g≈h → trans f≈g g≈h
   }
   where open IsEquivalence isEquivalence
 
@@ -64,21 +63,21 @@ isEquivalence isEquivalence = record
 isMagma : IsMagma _≈_ _∙_ → IsMagma (liftRel _≈_) (lift₂ _∙_)
 isMagma isMagma = record
   { isEquivalence = isEquivalence M.isEquivalence
-  ; ∙-cong = λ g h x → M.∙-cong (g x) (h x)
+  ; ∙-cong = λ g h → M.∙-cong g h
   }
   where module M = IsMagma isMagma
 
 isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup (liftRel _≈_) (lift₂ _∙_)
 isSemigroup isSemigroup = record
   { isMagma = isMagma M.isMagma
-  ; assoc = λ f g h x → M.assoc (f x) (g x) (h x)
+  ; assoc = λ f g h → M.assoc (f _) (g _) (h _)
   }
   where module M = IsSemigroup isSemigroup
 
 isBand : IsBand _≈_ _∙_ → IsBand (liftRel _≈_) (lift₂ _∙_)
 isBand isBand = record
   { isSemigroup = isSemigroup M.isSemigroup
-  ; idem = λ f x → M.idem (f x)
+  ; idem = λ f → M.idem (f _)
   }
   where module M = IsBand isBand
 
@@ -86,14 +85,14 @@ isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ →
                          IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
 isCommutativeSemigroup isCommutativeSemigroup = record
   { isSemigroup = isSemigroup M.isSemigroup
-  ; comm = λ f g x → M.comm (f x) (g x)
+  ; comm = λ f g → M.comm (f _) (g _)
   }
   where module M = IsCommutativeSemigroup isCommutativeSemigroup
 
 isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
 isMonoid isMonoid = record
   { isSemigroup = isSemigroup M.isSemigroup
-  ; identity = (λ f x → M.identityˡ (f x)) , λ f x → M.identityʳ (f x)
+  ; identity = (λ f → M.identityˡ (f _)) , λ f → M.identityʳ (f _)
   }
   where module M = IsMonoid isMonoid
 
@@ -101,7 +100,7 @@ isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε →
                       IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
 isCommutativeMonoid isCommutativeMonoid = record
   { isMonoid = isMonoid M.isMonoid
-  ; comm = λ f g x → M.comm (f x) (g x)
+  ; comm = λ f g → M.comm (f _) (g _)
   }
   where module M = IsCommutativeMonoid isCommutativeMonoid
 
@@ -109,8 +108,8 @@ isGroup : IsGroup _≈_ _∙_ ε _⁻¹ →
           IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
 isGroup isGroup = record
   { isMonoid = isMonoid M.isMonoid
-  ; inverse = (λ f x → M.inverseˡ (f x)) , λ f x → M.inverseʳ (f x)
-  ; ⁻¹-cong = λ f x → M.⁻¹-cong (f x)
+  ; inverse = (λ f → M.inverseˡ (f _)) , λ f → M.inverseʳ (f _)
+  ; ⁻¹-cong = λ f → M.⁻¹-cong f
   }
   where module M = IsGroup isGroup
 
@@ -118,7 +117,7 @@ isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹ →
                  IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
 isAbelianGroup isAbelianGroup = record
   { isGroup = isGroup M.isGroup
-  ; comm = λ f g x → M.comm (f x) (g x)
+  ; comm = λ f g → M.comm (f _) (g _)
   }
   where module M = IsAbelianGroup isAbelianGroup
 
@@ -126,10 +125,10 @@ isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_
   IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
 isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
   { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
-  ; *-cong =  λ g h x → M.*-cong (g x) (h x)
-  ; *-assoc =  λ f g h x → M.*-assoc (f x) (g x) (h x)
-  ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
-  ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+  ; *-cong =  λ g h → M.*-cong g h
+  ; *-assoc =  λ f g h → M.*-assoc (f _) (g _) (h _)
+  ; *-identity = (λ f → M.*-identityˡ (f _)) , λ f → M.*-identityʳ (f _)
+  ; distrib = (λ f g h → M.distribˡ (f _) (g _) (h _)) , λ f g h → M.distribʳ (f _) (g _) (h _)
   }
   where module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero
 
@@ -137,7 +136,7 @@ isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1# →
              IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
 isSemiring isSemiring = record
   { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
-  ; zero = (λ f x → M.zeroˡ (f x)) , λ f x → M.zeroʳ (f x)
+  ; zero = (λ f → M.zeroˡ (f _)) , λ f → M.zeroʳ (f _)
   }
   where module M = IsSemiring isSemiring
 
@@ -145,10 +144,10 @@ isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
          IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
 isRing isRing = record
   { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
-  ; *-cong = λ g h x → M.*-cong (g x) (h x)
-  ; *-assoc = λ f g h x → M.*-assoc (f x) (g x) (h x)
-  ; *-identity = (λ f x → M.*-identityˡ (f x)) , λ f x → M.*-identityʳ (f x)
-  ; distrib = (λ f g h x → M.distribˡ (f x) (g x) (h x)) , λ f g h x → M.distribʳ (f x) (g x) (h x)
+  ; *-cong = λ g h → M.*-cong g h
+  ; *-assoc = λ f g h → M.*-assoc (f _) (g _) (h _)
+  ; *-identity = (λ f → M.*-identityˡ (f _)) , λ f → M.*-identityʳ (f _)
+  ; distrib = (λ f g h → M.distribˡ (f _) (g _) (h _)) , λ f g h → M.distribʳ (f _) (g _) (h _)
   }
   where module M = IsRing isRing