From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 18 Jan 2022 22:01:46 +0000
Subject: Define the semantics of pseudocode data types.

---
 src/Helium/Algebra/Morphism/Structures.agda | 42 +++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 src/Helium/Algebra/Morphism/Structures.agda

(limited to 'src/Helium/Algebra/Morphism/Structures.agda')

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
-- 
cgit v1.2.3