Fix equivalence of rig homomorphisms

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