Add categories of Rigs, Bisemimodules, and Semimodules

3 files changed, 194 insertions, 0 deletions

diff --git a/Category/Instance/Bisemimodules.agda b/Category/Instance/Bisemimodules.agda
new file mode 100644
index 0000000..7556a75
--- /dev/null
+++ b/Category/Instance/Bisemimodules.agda
@@ -0,0 +1,69 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+open import Level using (Level; suc; _⊔_)
+
+module Category.Instance.Bisemimodules {c₁ c₂ ℓ₁ ℓ₂ m ℓm : Level} (R : Semiring c₁ ℓ₁) (S : Semiring c₂ ℓ₂) where
+
+import Algebra.Module.Morphism.Construct.Composition as Compose
+import Algebra.Module.Morphism.Construct.Identity as Identity
+
+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.PropositionalEquality as ≡ using (_≗_)
+
+record BisemimoduleHomomorphism (M N : Bisemimodule R S m ℓm) : Set (c₁ ⊔ c₂ ⊔ m ⊔ ℓm) where
+
+  private
+    module M = Bisemimodule M
+    module N = Bisemimodule N
+
+  field
+    ⟦_⟧ : M.Carrierᴹ → N.Carrierᴹ
+    isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism M.rawBisemimodule N.rawBisemimodule ⟦_⟧
+
+id : (M : Bisemimodule R S m ℓm) → BisemimoduleHomomorphism M M
+id M = record
+    { isBisemimoduleHomomorphism = Identity.isBisemimoduleHomomorphism M.rawBisemimodule M.≈ᴹ-refl
+    }
+  where
+    module M = Bisemimodule M
+
+compose
+    : (M N P : Bisemimodule R S m ℓm)
+    → BisemimoduleHomomorphism N P
+    → BisemimoduleHomomorphism M N
+    → BisemimoduleHomomorphism M P
+compose M N P f g = record
+    { isBisemimoduleHomomorphism =
+        Compose.isBisemimoduleHomomorphism
+            P.≈ᴹ-trans
+            g.isBisemimoduleHomomorphism
+            f.isBisemimoduleHomomorphism
+    }
+  where
+    module f = BisemimoduleHomomorphism f
+    module g = BisemimoduleHomomorphism g
+    module P = Bisemimodule P
+
+open BisemimoduleHomomorphism
+
+Bisemimodules : Category (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ suc (m ⊔ ℓm)) (c₁ ⊔ c₂ ⊔ 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))
+    }
diff --git a/Category/Instance/Rigs.agda b/Category/Instance/Rigs.agda
new file mode 100644
index 0000000..8642491
--- /dev/null
+++ b/Category/Instance/Rigs.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --without-K --safe #-}
+
+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
+
+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 Semiring using (rawSemiring; refl; trans)
+open SemiringHomomorphism using (⟦_⟧)
+
+id : (R : Semiring c ℓ) → SemiringHomomorphism (rawSemiring R) (rawSemiring R)
+id R = 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
+    { isSemiringHomomorphism =
+        Compose.isSemiringHomomorphism
+            (trans T)
+            g.isSemiringHomomorphism
+            f.isSemiringHomomorphism
+    }
+  where
+    module f = SemiringHomomorphism f
+    module g = SemiringHomomorphism g
+
+Rigs : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) c
+Rigs = categoryHelper record
+    { Obj = Semiring c ℓ
+    ; _⇒_ = λ R S → SemiringHomomorphism (rawSemiring R) (rawSemiring S)
+    ; _≈_ = λ f g → ⟦ f ⟧ ≗ ⟦ g ⟧
+    ; 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))
+    }
diff --git a/Category/Instance/Semimodules.agda b/Category/Instance/Semimodules.agda
new file mode 100644
index 0000000..d8ab6f5
--- /dev/null
+++ b/Category/Instance/Semimodules.agda
@@ -0,0 +1,69 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CommutativeSemiring)
+open import Level using (Level; suc; _⊔_)
+
+module Category.Instance.Semimodules {c ℓ m ℓm : Level} (R : CommutativeSemiring c ℓ) where
+
+import Algebra.Module.Morphism.Construct.Composition as Compose
+import Algebra.Module.Morphism.Construct.Identity as Identity
+
+open import Algebra.Module using (Semimodule)
+open import Algebra.Module.Morphism.Structures using (IsSemimoduleHomomorphism)
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+
+record SemimoduleHomomorphism (M N : Semimodule R m ℓm) : Set (c ⊔ m ⊔ ℓm) where
+
+  private
+    module M = Semimodule M
+    module N = Semimodule N
+
+  field
+    ⟦_⟧ : M.Carrierᴹ → N.Carrierᴹ
+    isSemimoduleHomomorphism : IsSemimoduleHomomorphism M.rawSemimodule N.rawSemimodule ⟦_⟧
+
+id : (M : Semimodule R m ℓm) → SemimoduleHomomorphism M M
+id M = record
+    { isSemimoduleHomomorphism = Identity.isSemimoduleHomomorphism M.rawSemimodule M.≈ᴹ-refl
+    }
+  where
+    module M = Semimodule M
+
+compose
+    : (M N P : Semimodule R m ℓm)
+    → SemimoduleHomomorphism N P
+    → SemimoduleHomomorphism M N
+    → SemimoduleHomomorphism M P
+compose M N P f g = record
+    { isSemimoduleHomomorphism =
+        Compose.isSemimoduleHomomorphism
+            P.≈ᴹ-trans
+            g.isSemimoduleHomomorphism
+            f.isSemimoduleHomomorphism
+    }
+  where
+    module f = SemimoduleHomomorphism f
+    module g = SemimoduleHomomorphism g
+    module P = Semimodule P
+
+open SemimoduleHomomorphism
+
+Semimodules : Category (c ⊔ ℓ ⊔ suc (m ⊔ ℓm)) (c ⊔ m ⊔ ℓm) m
+Semimodules = categoryHelper record
+    { Obj = Semimodule R m ℓm
+    ; _⇒_ = SemimoduleHomomorphism
+    ; _≈_ = λ 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))
+    }