Fix equivalence of rig homomorphisms

1 files changed, 4 insertions, 9 deletions

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