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

---
 Data/Matrix/BaseChange.agda | 13 ++++---------
 Data/Matrix/Matrices.agda   | 19 +++++++------------
 2 files changed, 11 insertions(+), 21 deletions(-)

(limited to 'Data')

diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda
index 906d1dd..4791efa 100644
--- a/Data/Matrix/BaseChange.agda
+++ b/Data/Matrix/BaseChange.agda
@@ -1,14 +1,13 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Algebra.Bundles using (Semiring)
-open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
+open import Algebra using (Semiring)
+open import Category.Instance.Rigs using (RigHomomorphism)
 open import Level using (Level)
 
 module Data.Matrix.BaseChange
     {c ℓ : Level}
     (R S : Semiring c ℓ)
-    (open Semiring using (rawSemiring))
-    (f : SemiringHomomorphism (rawSemiring R) (rawSemiring S))
+    (f : RigHomomorphism R S)
   where
 
 module R = Semiring R
@@ -47,7 +46,7 @@ open import Level using (0ℓ)
 open Func
 open Functor
 open MC using (Matrix)
-open SemiringHomomorphism f
+open RigHomomorphism f
 open ℕ
 private module Mat {A B : ℕ} = Functor (Endo.Mat A B {c} {ℓ})
 
@@ -75,10 +74,6 @@ module VecS where
   open VM S.+-monoid public
   open VB S public
 
-func : R.setoid ⟶ₛ S.setoid
-func .to = ⟦_⟧
-func .cong = ⟦⟧-cong
-
 change
     : {A B : ℕ}
     → Matrix R.setoid A B
diff --git a/Data/Matrix/Matrices.agda b/Data/Matrix/Matrices.agda
index 008ec36..1aa23d2 100644
--- a/Data/Matrix/Matrices.agda
+++ b/Data/Matrix/Matrices.agda
@@ -7,13 +7,12 @@ module Data.Matrix.Matrices {c ℓ : Level} where
 
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-open import Algebra.Bundles using (Semiring)
-open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
+open import Algebra using (Semiring)
 open import Categories.Category.Instance.Cats using (Cats)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Morphism.Properties using (id-iso)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
-open import Category.Instance.Rigs using (Rigs; compose) renaming (id to idRigHomo)
+open import Category.Instance.Rigs using (Rigs; RigHomomorphism; _≗_; compose) renaming (id to idRigHomo)
 open import Data.Matrix.BaseChange using (ChangeBase)
 open import Data.Matrix.BaseChange using (change)
 open import Data.Matrix.Category as Cat using (Mat)
@@ -21,10 +20,6 @@ open import Data.Matrix.Core as Core using ()
 open import Data.Matrix.Endofunctor using (mapₛ; identity; homomorphism; F-resp-≈)
 open import Data.Matrix.Transform as Transform using ()
 open import Data.Nat using (ℕ)
-open import Relation.Binary.PropositionalEquality using (_≗_)
-
-open Semiring using (rawSemiring)
-open SemiringHomomorphism using (⟦_⟧)
 
 ≃-identity : {A : Semiring c ℓ} → ChangeBase A A (Category.Instance.Rigs.id A) ≃ idF
 ≃-identity {A} = niHelper record
@@ -49,8 +44,8 @@ open SemiringHomomorphism using (⟦_⟧)
 
 ≃-homo
     : {X Y Z : Semiring c ℓ}
-      {g : SemiringHomomorphism (rawSemiring Y) (rawSemiring Z)}
-      {f : SemiringHomomorphism (rawSemiring X) (rawSemiring Y)}
+      {g : RigHomomorphism Y Z}
+      {f : RigHomomorphism X Y}
     → ChangeBase X Z (compose X Y Z g f) ≃ ChangeBase Y Z g ∘F ChangeBase X Y f
 ≃-homo {X} {Y} {Z} {g} {f} = niHelper record
     { η = λ n → I {n}
@@ -75,8 +70,8 @@ open SemiringHomomorphism using (⟦_⟧)
         open ≈-Reasoning (Matrixₛ n m)
 
 resp-≈ : {A B : Semiring c ℓ}
-    → {f g : SemiringHomomorphism (rawSemiring A) (rawSemiring B)}
-    → ⟦ f ⟧ ≗ ⟦ g ⟧
+    → {f g : RigHomomorphism A B}
+    → f ≗ g
     → ChangeBase A B f ≃ ChangeBase A B g
 resp-≈ {A} {B} {f} {g} f≗g = niHelper record
     { η = λ n → I {n}
@@ -94,7 +89,7 @@ resp-≈ {A} {B} {f} {g} f≗g = niHelper record
     commute : {n m : ℕ} (M : Matrix n m) → I · change A B f M ≋ change A B g M · I
     commute {n} {m} M = begin
         I · change A B f M  ≈⟨ ·-Iˡ ⟩
-        change A B f M      ≈⟨ F-resp-≈ n m (λ {x} → B.reflexive (f≗g x)) ⟩
+        change A B f M      ≈⟨ F-resp-≈ n m (λ {x} → f≗g x) ⟩
         change A B g M      ≈⟨ ·-Iʳ ⟨
         change A B g M · I  ∎
       where
-- 
cgit v1.2.3