Define the semantics of pseudocode data types.

1 files changed, 42 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda
new file mode 100644
index 0000000..bf219ef
--- /dev/null
+++ b/src/Helium/Algebra/Morphism/Structures.agda
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Redefine Ring monomorphisms to resolve problems with overloading.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Morphism.Structures where
+
+open import Algebra.Bundles using (RawRing)
+open import Algebra.Morphism.Structures
+  hiding (IsRingHomomorphism; module RingMorphisms)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
+  module R₁ = RawRing R₁ renaming (Carrier to A)
+  module R₂ = RawRing R₂ renaming (Carrier to B)
+  open R₁ using (A)
+  open R₂ using (B)
+
+  private
+    module +′ = GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup
+    module *′ = MonoidMorphisms R₁.*-rawMonoid R₂.*-rawMonoid
+
+  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      +-isGroupHomomorphism  : +′.IsGroupHomomorphism  ⟦_⟧
+      *-isMonoidHomomorphism : *′.IsMonoidHomomorphism ⟦_⟧
+
+    open +′.IsGroupHomomorphism +-isGroupHomomorphism public
+      renaming (homo to +-homo; ε-homo to 0#-homo; ⁻¹-homo to -‿homo)
+
+    open *′.IsMonoidHomomorphism *-isMonoidHomomorphism public
+      hiding (⟦⟧-cong)
+      renaming (homo to *-homo; ε-homo to 1#-homo)
+
+open RingMorphisms public