From 6a0549f4c5a93a1817cd311440de156c3283ba27 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 9 Jul 2026 10:20:43 -0700 Subject: Fix equivalence of rig homomorphisms --- Data/Matrix/BaseChange.agda | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) (limited to 'Data/Matrix/BaseChange.agda') 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 -- cgit v1.2.3