aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Category/Instance/Rigs.agda80
-rw-r--r--Data/Matrix/BaseChange.agda13
-rw-r--r--Data/Matrix/Matrices.agda19
3 files changed, 67 insertions, 45 deletions
diff --git a/Category/Instance/Rigs.agda b/Category/Instance/Rigs.agda
index 8642491..37f2481 100644
--- a/Category/Instance/Rigs.agda
+++ b/Category/Instance/Rigs.agda
@@ -4,29 +4,63 @@ open import Level using (Level; suc; _⊔_)
module Category.Instance.Rigs {c ℓ : Level} where
-import Algebra.Morphism.Construct.Identity as Identity
import Algebra.Morphism.Construct.Composition as Compose
+import Algebra.Morphism.Construct.Identity as Identity
open import Algebra using (Semiring)
open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Function using (_⟶ₛ_; Func)
+open import Relation.Binary using (IsEquivalence)
+
+open Func
+open Semiring hiding (_≈_)
+
+record RigHomomorphism (R S : Semiring c ℓ) : Set (c ⊔ ℓ) where
+
+ constructor mk-⇒
+
+ field
+ semiringHomomorphism : SemiringHomomorphism (rawSemiring R) (rawSemiring S)
+
+ open SemiringHomomorphism semiringHomomorphism public
+
+ func : setoid R ⟶ₛ setoid S
+ func .to = ⟦_⟧
+ func .cong = ⟦⟧-cong
-open Semiring using (rawSemiring; refl; trans)
-open SemiringHomomorphism using (⟦_⟧)
+module _ {R S : Semiring c ℓ} where
-id : (R : Semiring c ℓ) → SemiringHomomorphism (rawSemiring R) (rawSemiring R)
-id R = record
+ -- Pointwise equality of rig homomorphisms
+
+ open RigHomomorphism
+
+ _≗_ : (f g : RigHomomorphism R S) → Set (c ⊔ ℓ)
+ _≗_ f g = (x : Carrier R) → let open Semiring S in ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+ infix 4 _≗_
+
+ ≗-isEquivalence : IsEquivalence _≗_
+ ≗-isEquivalence = record
+ { refl = λ x → refl S
+ ; sym = λ f≈g x → sym S (f≈g x)
+ ; trans = λ f≈g g≈h x → trans S (f≈g x) (g≈h x)
+ }
+
+ module ≗ = IsEquivalence ≗-isEquivalence
+
+id : (R : Semiring c ℓ) → RigHomomorphism R R
+id R = mk-⇒ record
{ isSemiringHomomorphism = Identity.isSemiringHomomorphism (rawSemiring R) (refl R)
}
compose
: (R S T : Semiring c ℓ)
- → SemiringHomomorphism (rawSemiring S) (rawSemiring T)
- → SemiringHomomorphism (rawSemiring R) (rawSemiring S)
- → SemiringHomomorphism (rawSemiring R) (rawSemiring T)
-compose R S T f g = record
+ → RigHomomorphism S T
+ → RigHomomorphism R S
+ → RigHomomorphism R T
+compose R S T f g = mk-⇒ record
{ isSemiringHomomorphism =
Compose.isSemiringHomomorphism
(trans T)
@@ -34,23 +68,21 @@ compose R S T f g = record
f.isSemiringHomomorphism
}
where
- module f = SemiringHomomorphism f
- module g = SemiringHomomorphism g
+ module f = RigHomomorphism f
+ module g = RigHomomorphism g
+
+open RigHomomorphism
-Rigs : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) c
+Rigs : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
Rigs = categoryHelper record
{ Obj = Semiring c ℓ
- ; _⇒_ = λ R S → SemiringHomomorphism (rawSemiring R) (rawSemiring S)
- ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+ ; _⇒_ = RigHomomorphism
+ ; _≈_ = _≗_
; id = λ {R} → id R
; _∘_ = λ {R S T} f g → compose R S T f g
- ; assoc = λ _ → ≡.refl
- ; identityˡ = λ _ → ≡.refl
- ; identityʳ = λ _ → ≡.refl
- ; equiv = record
- { refl = λ _ → ≡.refl
- ; sym = λ f≈g x → ≡.sym (f≈g x)
- ; trans = λ f≈g g≈h x → ≡.trans (f≈g x) (g≈h x)
- }
- ; ∘-resp-≈ = λ {f = f} {h g i} eq₁ eq₂ x → ≡.trans (≡.cong ⟦ f ⟧ (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+ ; assoc = λ {D = D} _ → refl D
+ ; identityˡ = λ {B = B} _ → refl B
+ ; identityʳ = λ {B = B} _ → refl B
+ ; equiv = ≗-isEquivalence
+ ; ∘-resp-≈ = λ {C = C} {f h g i} eq₁ eq₂ x → trans C (⟦⟧-cong f (eq₂ x)) (eq₁ (⟦ i ⟧ x))
}
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-21 22:13:17 +0000