diff options
Diffstat (limited to 'Data/Matrix/Matrices.agda')
| -rw-r--r-- | Data/Matrix/Matrices.agda | 19 |
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 |