From fe8405495e0adddff98c8ae727e1906a09efefb3 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 3 Apr 2026 16:37:35 -0500
Subject: Add free functor from rig-matrices to semimodules

---
 Category/Instance/Bisemimodules.agda | 51 ++++++++++++++++++++++++++++--------
 1 file changed, 40 insertions(+), 11 deletions(-)

(limited to 'Category/Instance/Bisemimodules.agda')

diff --git a/Category/Instance/Bisemimodules.agda b/Category/Instance/Bisemimodules.agda
index 7556a75..0b7b0b2 100644
--- a/Category/Instance/Bisemimodules.agda
+++ b/Category/Instance/Bisemimodules.agda
@@ -12,6 +12,7 @@ open import Algebra.Module using (Bisemimodule)
 open import Algebra.Module.Morphism.Structures using (IsBisemimoduleHomomorphism)
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary using (Rel; IsEquivalence)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 
 record BisemimoduleHomomorphism (M N : Bisemimodule R S m ℓm) : Set (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) where
@@ -24,6 +25,8 @@ record BisemimoduleHomomorphism (M N : Bisemimodule R S m ℓm) : Set (c₁ ⊔
     ⟦_⟧ : M.Carrierᴹ → N.Carrierᴹ
     isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism M.rawBisemimodule N.rawBisemimodule ⟦_⟧
 
+  open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public
+
 id : (M : Bisemimodule R S m ℓm) → BisemimoduleHomomorphism M M
 id M = record
     { isBisemimoduleHomomorphism = Identity.isBisemimoduleHomomorphism M.rawBisemimodule M.≈ᴹ-refl
@@ -50,20 +53,46 @@ compose M N P f g = record
 
 open BisemimoduleHomomorphism
 
-Bisemimodules : Category (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ suc (m ⊔ ℓm)) (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) m
+_≈_ : {M N : Bisemimodule R S m ℓm} → Rel (BisemimoduleHomomorphism M N) (m ⊔ ℓm)
+_≈_ {M} {N} f g = (x : M.Carrierᴹ) → ⟦ f ⟧ x N.≈ᴹ ⟦ g ⟧ x
+  where
+    module M = Bisemimodule M
+    module N = Bisemimodule N
+
+≈-isEquiv : {M N : Bisemimodule R S m ℓm} → IsEquivalence (_≈_ {M} {N})
+≈-isEquiv {M} {N} = record
+    { refl = λ _ → N.≈ᴹ-refl
+    ; sym = λ f≈g x → N.≈ᴹ-sym (f≈g x)
+    ; trans = λ f≈g g≈h x → N.≈ᴹ-trans (f≈g x) (g≈h x)
+    }
+  where
+    module M = Bisemimodule M
+    module N = Bisemimodule N
+
+∘-resp-≈
+    : {M N P : Bisemimodule R S m ℓm}
+      {f h : BisemimoduleHomomorphism N P}
+      {g i : BisemimoduleHomomorphism M N}
+    → f ≈ h
+    → g ≈ i
+    → compose M N P f g ≈ compose M N P h i
+∘-resp-≈ {M} {N} {P} {f} {g} {h} {i} f≈h g≈i x = P.≈ᴹ-trans (f.⟦⟧-cong (g≈i x)) (f≈h (⟦ i ⟧ x))
+  where
+    module P = Bisemimodule P
+    module f = BisemimoduleHomomorphism f
+
+open Bisemimodule
+
+Bisemimodules : Category (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ suc (m ⊔ ℓm)) (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) (m ⊔ ℓm)
 Bisemimodules = categoryHelper record
     { Obj = Bisemimodule R S m ℓm
     ; _⇒_ = BisemimoduleHomomorphism
-    ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+    ; _≈_ = _≈_
     ; id = λ {M} → id M
     ; _∘_ = λ {M N P} f g → compose M N P 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 = ≈-isEquiv
+    ; ∘-resp-≈ = λ {f = f} {g h i } → ∘-resp-≈ {f = f} {g} {h} {i}
     }
-- 
cgit v1.2.3