Fix equivalence of rig homomorphisms

1 files changed, 7 insertions, 12 deletions

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