Add more properties for ordered structures.

1 files changed, 0 insertions, 42 deletions

diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda
deleted file mode 100644
index bf219ef..0000000
--- a/src/Helium/Algebra/Morphism/Structures.agda
+++ /dev/null
@@ -1,42 +0,0 @@
-------------------------------------------------------------------------
--- 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