From 6a0549f4c5a93a1817cd311440de156c3283ba27 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 9 Jul 2026 10:20:43 -0700
Subject: Fix equivalence of rig homomorphisms

---
 Category/Instance/Rigs.agda | 80 +++++++++++++++++++++++++++++++--------------
 1 file changed, 56 insertions(+), 24 deletions(-)

(limited to 'Category/Instance')

diff --git a/Category/Instance/Rigs.agda b/Category/Instance/Rigs.agda
index 8642491..37f2481 100644
--- a/Category/Instance/Rigs.agda
+++ b/Category/Instance/Rigs.agda
@@ -4,29 +4,63 @@ open import Level using (Level; suc; _⊔_)
 
 module Category.Instance.Rigs {c ℓ : Level} where
 
-import Algebra.Morphism.Construct.Identity as Identity
 import Algebra.Morphism.Construct.Composition as Compose
+import Algebra.Morphism.Construct.Identity as Identity
 
 open import Algebra using (Semiring)
 open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Function using (_⟶ₛ_; Func)
+open import Relation.Binary using (IsEquivalence)
+
+open Func
+open Semiring hiding (_≈_)
+
+record RigHomomorphism (R S : Semiring c ℓ) : Set (c ⊔ ℓ) where
+
+  constructor mk-⇒
+
+  field
+    semiringHomomorphism : SemiringHomomorphism (rawSemiring R) (rawSemiring S)
+
+  open SemiringHomomorphism semiringHomomorphism public
+
+  func : setoid R ⟶ₛ setoid S
+  func .to = ⟦_⟧
+  func .cong = ⟦⟧-cong
 
-open Semiring using (rawSemiring; refl; trans)
-open SemiringHomomorphism using (⟦_⟧)
+module _ {R S : Semiring c ℓ} where
 
-id : (R : Semiring c ℓ) → SemiringHomomorphism (rawSemiring R) (rawSemiring R)
-id R = record
+  -- Pointwise equality of rig homomorphisms
+
+  open RigHomomorphism
+
+  _≗_ : (f g : RigHomomorphism R S) → Set (c ⊔ ℓ)
+  _≗_ f g = (x : Carrier R) → let open Semiring S in ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+  infix 4 _≗_
+
+  ≗-isEquivalence : IsEquivalence _≗_
+  ≗-isEquivalence = record
+      { refl = λ x → refl S
+      ; sym = λ f≈g x → sym S (f≈g x)
+      ; trans = λ f≈g g≈h x → trans S (f≈g x) (g≈h x)
+      }
+
+  module ≗ = IsEquivalence ≗-isEquivalence
+
+id : (R : Semiring c ℓ) → RigHomomorphism R R
+id R = mk-⇒ record
     { isSemiringHomomorphism = Identity.isSemiringHomomorphism (rawSemiring R) (refl R)
     }
 
 compose
     : (R S T : Semiring c ℓ)
-    → SemiringHomomorphism (rawSemiring S) (rawSemiring T)
-    → SemiringHomomorphism (rawSemiring R) (rawSemiring S)
-    → SemiringHomomorphism (rawSemiring R) (rawSemiring T)
-compose R S T f g = record
+    → RigHomomorphism S T
+    → RigHomomorphism R S
+    → RigHomomorphism R T
+compose R S T f g = mk-⇒ record
     { isSemiringHomomorphism =
         Compose.isSemiringHomomorphism
             (trans T)
@@ -34,23 +68,21 @@ compose R S T f g = record
             f.isSemiringHomomorphism
     }
   where
-    module f = SemiringHomomorphism f
-    module g = SemiringHomomorphism g
+    module f = RigHomomorphism f
+    module g = RigHomomorphism g
+
+open RigHomomorphism
 
-Rigs : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) c
+Rigs : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
 Rigs = categoryHelper record
     { Obj = Semiring c ℓ
-    ; _⇒_ = λ R S → SemiringHomomorphism (rawSemiring R) (rawSemiring S)
-    ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+    ; _⇒_ = RigHomomorphism
+    ; _≈_ = _≗_
     ; id = λ {R} → id R
     ; _∘_ = λ {R S T} f g → compose R S T f g
-    ; assoc = λ _ → ≡.refl
-    ; identityˡ = λ _ → ≡.refl
-    ; identityʳ = λ _ → ≡.refl
-    ; equiv = record
-        { refl = λ _ → ≡.refl
-        ; sym = λ f≈g x → ≡.sym (f≈g x)
-        ; trans = λ f≈g g≈h x → ≡.trans (f≈g x) (g≈h x)
-        }
-    ; ∘-resp-≈ = λ {f = f} {h g i} eq₁ eq₂ x → ≡.trans (≡.cong ⟦ f ⟧ (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+    ; assoc = λ {D = D} _ → refl D
+    ; identityˡ = λ {B = B} _ → refl B
+    ; identityʳ = λ {B = B} _ → refl B
+    ; equiv = ≗-isEquivalence
+    ; ∘-resp-≈ = λ {C = C} {f h g i} eq₁ eq₂ x → trans C (⟦⟧-cong f (eq₂ x)) (eq₁ (⟦ i ⟧ x))
     }
-- 
cgit v1.2.3