Define the semantics of pseudocode data types.

9 files changed, 922 insertions, 153 deletions

diff --git a/Everything.agda b/Everything.agda
index e1a82ae..f47f3b7 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -14,15 +14,26 @@ import Helium.Algebra.Bundles
 -- Relations between properties of functions when the underlying relation is a setoid
 import Helium.Algebra.Consequences.Setoid
 
--- Construct algebras of vectors in a pointwise manner
-import Helium.Algebra.Construct.Pointwise
-
 -- More core algebraic definitions
 import Helium.Algebra.Core
 
+-- Definitions of decidable algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+import Helium.Algebra.Decidable.Bundles
+
+-- Construct decidable algebras of vectors in a pointwise manner
+import Helium.Algebra.Decidable.Construct.Pointwise
+
+-- Some decidable algebraic structures (not packed up with sets,
+-- operations, etc.)
+import Helium.Algebra.Decidable.Structures
+
 -- More properties of functions
 import Helium.Algebra.Definitions
 
+-- Redefine Ring monomorphisms to resolve problems with overloading.
+import Helium.Algebra.Morphism.Structures
+
 -- Ordering properties of functions
 import Helium.Algebra.Ordered.Definitions
 
diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda
new file mode 100644
index 0000000..e446706
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Bundles.agda
@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of decidable algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Helium.Algebra.Decidable.Bundles where
+
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
+open import Helium.Algebra.Decidable.Structures
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Bundles using (DecSetoid)
+open import Relation.Binary.Core using (Rel)
+
+record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier   : Set c
+    _≈_       : Rel Carrier ℓ
+    _∨_       : Op₂ Carrier
+    _∧_       : Op₂ Carrier
+    isLattice : IsLattice _≈_ _∨_ _∧_
+
+  open IsLattice isLattice public
+
+  rawLattice : RawLattice c ℓ
+  rawLattice = record
+    { _≈_  = _≈_
+    ; _∧_  = _∧_
+    ; _∨_  = _∨_
+    }
+
+  open RawLattice rawLattice public
+    using (∨-rawMagma; ∧-rawMagma)
+
+  decSetoid : DecSetoid _ _
+  decSetoid = record { isDecEquivalence = isDecEquivalence }
+
+  open DecSetoid decSetoid public
+    using (_≉_; setoid)
+
+record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier               : Set c
+    _≈_                   : Rel Carrier ℓ
+    _∨_                   : Op₂ Carrier
+    _∧_                   : Op₂ Carrier
+    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
+
+  open IsDistributiveLattice isDistributiveLattice public
+
+  lattice : Lattice _ _
+  lattice = record { isLattice = isLattice }
+
+  open Lattice lattice public
+    using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice)
+
+record RawBooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∧_     : Op₂ Carrier
+    _∨_     : Op₂ Carrier
+    ¬_      : Op₁ Carrier
+    ⊤       : Carrier
+    ⊥       : Carrier
+
+  rawLattice : RawLattice c ℓ
+  rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ }
+
+  open RawLattice rawLattice public
+    using (_≉_; ∨-rawMagma; ∧-rawMagma)
+
+record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _∨_              : Op₂ Carrier
+    _∧_              : Op₂ Carrier
+    ¬_               : Op₁ Carrier
+    ⊤                : Carrier
+    ⊥                : Carrier
+    isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
+
+  open IsBooleanAlgebra isBooleanAlgebra public
+
+  distributiveLattice : DistributiveLattice _ _
+  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
+
+  open DistributiveLattice distributiveLattice public
+    using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice)
diff --git a/src/Helium/Algebra/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
index d3aa560..9f067ba 100644
--- a/src/Helium/Algebra/Construct/Pointwise.agda
+++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda
@@ -6,17 +6,20 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-module Helium.Algebra.Construct.Pointwise where
+module Helium.Algebra.Decidable.Construct.Pointwise where
 
-open import Algebra
-open import Relation.Binary.Core using (Rel)
+open import Algebra.Bundles using (RawLattice)
+open import Algebra.Core
 open import Data.Nat using (ℕ)
 open import Data.Product using (_,_)
 open import Data.Vec.Functional using (replicate; map; zipWith)
 open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
 import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
 open import Function using (_$_)
+open import Helium.Algebra.Decidable.Bundles
+open import Helium.Algebra.Decidable.Structures
 open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
 
 module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
   private
@@ -25,22 +28,23 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
   module _ {∨ ∧ : Op₂ A} where
     isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
     isLattice L n = record
-      { isEquivalence = Pwₚ.isEquivalence isEquivalence n
-      ; ∨-comm        = λ x y i → ∨-comm (x i) (y i)
-      ; ∨-assoc       = λ x y z i → ∨-assoc (x i) (y i) (z i)
-      ; ∨-cong        = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
-      ; ∧-comm        = λ x y i → ∧-comm (x i) (y i)
-      ; ∧-assoc       = λ x y z i → ∧-assoc (x i) (y i) (z i)
-      ; ∧-cong        = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
-      ; absorptive    = (λ x y i → ∨-absorbs-∧ (x i) (y i))
-                      , (λ x y i → ∧-absorbs-∨ (x i) (y i))
+      { isDecEquivalence = Pwₚ.isDecEquivalence isDecEquivalence n
+      ; ∨-comm           = λ x y i → ∨-comm (x i) (y i)
+      ; ∨-assoc          = λ x y z i → ∨-assoc (x i) (y i) (z i)
+      ; ∨-cong           = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
+      ; ∧-comm           = λ x y i → ∧-comm (x i) (y i)
+      ; ∧-assoc          = λ x y z i → ∧-assoc (x i) (y i) (z i)
+      ; ∧-cong           = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
+      ; absorptive       = (λ x y i → ∨-absorbs-∧ (x i) (y i))
+                         , (λ x y i → ∧-absorbs-∨ (x i) (y i))
       }
       where open IsLattice L
 
     isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
     isDistributiveLattice L n = record
       { isLattice = isLattice L.isLattice n
-      ; ∨-distribʳ-∧ = λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i)
+      ; ∨-distrib-∧ = (λ x y z i → L.∨-distribˡ-∧ (x i) (y i) (z i))
+                    , (λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i))
       }
       where module L = IsDistributiveLattice L
 
@@ -48,12 +52,22 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
     isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥)
     isBooleanAlgebra B n = record
       { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n
-      ; ∨-complementʳ = λ x i → B.∨-complementʳ (x i)
-      ; ∧-complementʳ = λ x i → B.∧-complementʳ (x i)
+      ; ∨-complement = (λ x i → B.∨-complementˡ (x i))
+                     , (λ x i → B.∨-complementʳ (x i))
+      ; ∧-complement = (λ x i → B.∧-complementˡ (x i))
+                     , (λ x i → B.∧-complementʳ (x i))
       ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i)
       }
       where module B = IsBooleanAlgebra B
 
+rawLattice : ∀ {a ℓ} → RawLattice a ℓ → ℕ → RawLattice a ℓ
+rawLattice L n = record
+  { _≈_ = Pointwise _≈_ {n}
+  ; _∧_ = zipWith _∧_
+  ; _∨_ = zipWith _∨_
+  }
+  where open RawLattice L
+
 lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ
 lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n }
 
@@ -63,6 +77,17 @@ distributiveLattice L n = record
     isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n
   }
 
+rawBooleanAlgebra : ∀ {a ℓ} → RawBooleanAlgebra a ℓ → ℕ → RawBooleanAlgebra a ℓ
+rawBooleanAlgebra B n = record
+  { _≈_ = Pointwise _≈_ {n}
+  ; _∧_ = zipWith _∧_
+  ; _∨_ = zipWith _∨_
+  ; ¬_  = map ¬_
+  ; ⊤   = replicate ⊤
+  ; ⊥   = replicate ⊥
+  }
+  where open RawBooleanAlgebra B
+
 booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ
 booleanAlgebra B n = record
   { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n }
diff --git a/src/Helium/Algebra/Decidable/Structures.agda b/src/Helium/Algebra/Decidable/Structures.agda
new file mode 100644
index 0000000..4380cc5
--- /dev/null
+++ b/src/Helium/Algebra/Decidable/Structures.agda
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some decidable algebraic structures (not packed up with sets,
+-- operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Decidable.Structures
+  {a ℓ} {A : Set a}  -- The underlying set
+  (_≈_ : Rel A ℓ)    -- The underlying equality relation
+  where
+
+open import Algebra.Core
+open import Algebra.Definitions (_≈_)
+open import Data.Product using (proj₁; proj₂)
+open import Level using (_⊔_)
+open import Relation.Binary.Structures using (IsDecEquivalence)
+
+record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isDecEquivalence : IsDecEquivalence _≈_
+    ∨-comm           : Commutative ∨
+    ∨-assoc          : Associative ∨
+    ∨-cong           : Congruent₂ ∨
+    ∧-comm           : Commutative ∧
+    ∧-assoc          : Associative ∧
+    ∧-cong           : Congruent₂ ∧
+    absorptive       : Absorptive ∨ ∧
+
+  open IsDecEquivalence isDecEquivalence public
+
+  ∨-absorbs-∧ : ∨ Absorbs ∧
+  ∨-absorbs-∧ = proj₁ absorptive
+
+  ∧-absorbs-∨ : ∧ Absorbs ∨
+  ∧-absorbs-∨ = proj₂ absorptive
+
+  ∧-congˡ : LeftCongruent ∧
+  ∧-congˡ y≈z = ∧-cong refl y≈z
+
+  ∧-congʳ : RightCongruent ∧
+  ∧-congʳ y≈z = ∧-cong y≈z refl
+
+  ∨-congˡ : LeftCongruent ∨
+  ∨-congˡ y≈z = ∨-cong refl y≈z
+
+  ∨-congʳ : RightCongruent ∨
+  ∨-congʳ y≈z = ∨-cong y≈z refl
+
+record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isLattice   : IsLattice ∨ ∧
+    ∨-distrib-∧ : ∨ DistributesOver ∧
+
+  open IsLattice isLattice public
+
+  ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧
+  ∨-distribˡ-∧ = proj₁ ∨-distrib-∧
+
+  ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
+  ∨-distribʳ-∧ = proj₂ ∨-distrib-∧
+
+record IsBooleanAlgebra
+         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
+  field
+    isDistributiveLattice : IsDistributiveLattice ∨ ∧
+    ∨-complement          : Inverse ⊤ ¬ ∨
+    ∧-complement          : Inverse ⊥ ¬ ∧
+    ¬-cong                : Congruent₁ ¬
+
+  open IsDistributiveLattice isDistributiveLattice public
+
+  ∨-complementˡ : LeftInverse ⊤ ¬ ∨
+  ∨-complementˡ = proj₁ ∨-complement
+
+  ∨-complementʳ : RightInverse ⊤ ¬ ∨
+  ∨-complementʳ = proj₂ ∨-complement
+
+  ∧-complementˡ : LeftInverse ⊥ ¬ ∧
+  ∧-complementˡ = proj₁ ∧-complement
+
+  ∧-complementʳ : RightInverse ⊥ ¬ ∧
+  ∧-complementʳ = proj₂ ∧-complement
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
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
index 6904bfb..a9430e9 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -10,13 +10,12 @@
 
 module Helium.Algebra.Ordered.StrictTotal.Bundles where
 
-import Algebra.Bundles as Unordered
+import Algebra.Bundles as NoOrder
 open import Algebra.Core
 open import Data.Sum using (_⊎_)
 open import Function using (flip)
 open import Helium.Algebra.Core
-open import Helium.Algebra.Bundles using
-  (RawAlmostGroup; AlmostGroup; AlmostAbelianGroup)
+import Helium.Algebra.Bundles as NoOrder′
 open import Helium.Algebra.Ordered.StrictTotal.Structures
 open import Level using (suc; _⊔_)
 open import Relation.Binary
@@ -44,6 +43,10 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   _≥_ : Rel Carrier _
   _≥_ = flip _≤_
 
+  module Unordered where
+    rawMagma : NoOrder.RawMagma c ℓ₁
+    rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ }
+
 record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infixl 7 _∙_
   infix  4 _≈_ _<_
@@ -55,6 +58,7 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isMagma : IsMagma _≈_ _<_ _∙_
 
   open IsMagma isMagma public
+    hiding (module Unordered)
 
   rawMagma : RawMagma _ _ _
   rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
@@ -62,6 +66,15 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open RawMagma rawMagma public
     using (_≉_; _≤_; _>_; _≥_)
 
+  module Unordered where
+    magma : NoOrder.Magma c ℓ₁
+    magma = record { isMagma = IsMagma.Unordered.isMagma isMagma }
+
+    open NoOrder.Magma magma public
+      using (rawMagma)
+
+    open IsMagma.Unordered isMagma public
+
 record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infixl 7 _∙_
   infix  4 _≈_ _<_
@@ -73,6 +86,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isSemigroup : IsSemigroup _≈_ _<_ _∙_
 
   open IsSemigroup isSemigroup public
+    hiding (module Unordered)
 
   magma : Magma c ℓ₁ ℓ₂
   magma = record { isMagma = isMagma }
@@ -80,6 +94,16 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Magma magma public
     using (_≉_; _≤_; _>_; _≥_; rawMagma)
 
+  module Unordered where
+    semigroup : NoOrder.Semigroup c ℓ₁
+    semigroup =
+      record { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup }
+
+    open NoOrder.Semigroup semigroup public
+      using (rawMagma; magma)
+
+    open IsSemigroup.Unordered isSemigroup public
+
 record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infixl 7 _∙_
   infix  4 _≈_ _<_
@@ -96,6 +120,13 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open RawMagma rawMagma public
     using (_≉_; _≤_; _>_; _≥_)
 
+  module Unordered where
+    rawMonoid : NoOrder.RawMonoid c ℓ₁
+    rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε }
+
+    open NoOrder.RawMonoid rawMonoid public
+      using (rawMagma)
+
 record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infixl 7 _∙_
   infix  4 _≈_ _<_
@@ -108,6 +139,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isMonoid : IsMonoid _≈_ _<_ _∙_ ε
 
   open IsMonoid isMonoid public
+    hiding (module Unordered)
 
   semigroup : Semigroup _ _ _
   semigroup = record { isSemigroup = isSemigroup }
@@ -118,6 +150,15 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   rawMonoid : RawMonoid _ _ _
   rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε}
 
+  module Unordered where
+    monoid : NoOrder.Monoid c ℓ₁
+    monoid = record { isMonoid = IsMonoid.Unordered.isMonoid isMonoid }
+
+    open NoOrder.Monoid monoid public
+      using (rawMagma; rawMonoid; magma; semigroup)
+
+    open IsMonoid.Unordered isMonoid public
+
 record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 _⁻¹
   infixl 7 _∙_
@@ -136,6 +177,12 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open RawMonoid rawMonoid public
     using (_≉_; _≤_; _>_; _≥_; rawMagma)
 
+  module Unordered where
+    rawGroup : NoOrder.RawGroup c ℓ₁
+    rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹ }
+
+    open NoOrder.RawGroup rawGroup public
+      using (rawMagma; rawMonoid)
 
 record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 _⁻¹
@@ -151,6 +198,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹
 
   open IsGroup isGroup public
+    hiding (module Unordered)
 
   rawGroup : RawGroup _ _ _
   rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
@@ -161,6 +209,15 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Monoid monoid public
     using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid)
 
+  module Unordered where
+    group : NoOrder.Group c ℓ₁
+    group = record { isGroup = IsGroup.Unordered.isGroup isGroup }
+
+    open NoOrder.Group group public
+      using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid)
+
+    open IsGroup.Unordered isGroup public
+
 record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 _⁻¹
   infixl 7 _∙_
@@ -175,6 +232,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹
 
   open IsAbelianGroup isAbelianGroup public
+    hiding (module Unordered)
 
   group : Group _ _ _
   group = record { isGroup = isGroup }
@@ -186,6 +244,16 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; rawMagma; rawMonoid; rawGroup
     )
 
+  module Unordered where
+    abelianGroup : NoOrder.AbelianGroup c ℓ₁
+    abelianGroup =
+      record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup }
+
+    open NoOrder.AbelianGroup abelianGroup public
+      using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group)
+
+    open IsAbelianGroup.Unordered isAbelianGroup public
+
 record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_
   infixl 7 _*_
@@ -211,13 +279,21 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; rawMonoid to +-rawMonoid
     )
 
-  *-rawMonoid : Unordered.RawMonoid c ℓ₁
+  *-rawMonoid : NoOrder.RawMonoid c ℓ₁
   *-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# }
 
-  open Unordered.RawMonoid *-rawMonoid public
+  open NoOrder.RawMonoid *-rawMonoid public
     using ()
     renaming ( rawMagma to *-rawMagma )
 
+  module Unordered where
+    rawRing : NoOrder.RawRing c ℓ₁
+    rawRing =
+      record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# }
+
+    open NoOrder.RawRing rawRing public
+      using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring)
+
 record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_
   infixl 7 _*_
@@ -235,6 +311,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isRing  : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1#
 
   open IsRing isRing public
+    hiding (module Unordered)
 
   rawRing : RawRing c ℓ₁ ℓ₂
   rawRing = record
@@ -262,10 +339,10 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; group to +-group
     )
 
-  *-monoid : Unordered.Monoid _ _
+  *-monoid : NoOrder.Monoid _ _
   *-monoid = record { isMonoid = *-isMonoid }
 
-  open Unordered.Monoid *-monoid public
+  open NoOrder.Monoid *-monoid public
     using ()
     renaming
     ( rawMagma to *-rawMagma
@@ -274,6 +351,19 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; semigroup to *-semigroup
     )
 
+  module Unordered where
+    ring : NoOrder.Ring c ℓ₁
+    ring = record { isRing = IsRing.Unordered.isRing isRing }
+
+    open NoOrder.Ring ring public
+      using
+      ( +-rawMagma; +-rawMonoid
+      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; rawRing; semiring
+      )
+
+    open IsRing.Unordered isRing public
+
 record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_
   infixl 7 _*_
@@ -291,6 +381,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
     isCommutativeRing  : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1#
 
   open IsCommutativeRing isCommutativeRing public
+    hiding (module Unordered)
 
   ring : Ring _ _ _
   ring = record { isRing = isRing }
@@ -298,12 +389,30 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
   open Ring ring public
     using
     ( _≉_; _≤_; _>_; _≥_
+    ; rawRing
     ; +-rawMagma; +-rawMonoid; +-rawGroup
     ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
     ; *-rawMagma; *-rawMonoid
     ; *-magma; *-semigroup; *-monoid
     )
 
+  module Unordered where
+    commutativeRing : NoOrder.CommutativeRing c ℓ₁
+    commutativeRing =
+      record { isCommutativeRing = IsCommutativeRing.Unordered.isCommutativeRing isCommutativeRing }
+
+    open NoOrder.CommutativeRing commutativeRing public
+      using
+      ( +-rawMagma; +-rawMonoid
+      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; rawRing; semiring; ring
+      )
+
+    open NoOrder.Semiring semiring public
+      using (rawSemiring)
+
+    open IsCommutativeRing.Unordered isCommutativeRing public
+
 record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  9 _⁻¹
   infix  8 -_
@@ -343,7 +452,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; *-rawMagma; *-rawMonoid
     )
 
-  *-rawAlmostGroup : RawAlmostGroup c ℓ₁
+  *-rawAlmostGroup : NoOrder′.RawAlmostGroup c ℓ₁
   *-rawAlmostGroup = record
     { _≈_ = _≈_
     ; _∙_ = _*_
@@ -352,6 +461,21 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; _⁻¹ = _⁻¹
     }
 
+  module Unordered where
+    rawField : NoOrder′.RawField c ℓ₁
+    rawField = record
+      { _≈_ = _≈_
+      ; _+_ = _+_
+      ; _*_ = _*_
+      ; -_  = -_
+      ; 0#  = 0#
+      ; 1#  = 1#
+      ; _⁻¹ = _⁻¹
+      }
+
+    open NoOrder′.RawField rawField public
+      using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring; rawRing)
+
 record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  9 _⁻¹
   infix  8 -_
@@ -371,6 +495,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isDivisionRing  : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
 
   open IsDivisionRing isDivisionRing public
+    hiding (module Unordered)
 
   rawField : RawField c ℓ₁ ℓ₂
   rawField = record
@@ -397,13 +522,28 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; *-magma; *-semigroup; *-monoid
     )
 
-  *-almostGroup : AlmostGroup _ _
+  *-almostGroup : NoOrder′.AlmostGroup _ _
   *-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
 
-  open AlmostGroup *-almostGroup public
+  open NoOrder′.AlmostGroup *-almostGroup public
     using ()
     renaming (rawAlmostGroup to *-rawAlmostGroup)
 
+  module Unordered where
+    divisionRing : NoOrder′.DivisionRing c ℓ₁
+    divisionRing =
+      record { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing }
+
+    open NoOrder′.DivisionRing divisionRing public
+      using
+      ( +-rawMagma; +-rawMonoid
+      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; rawSemiring; rawRing
+      ; semiring; ring
+      )
+
+    open IsDivisionRing.Unordered isDivisionRing public
+
 record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  9 _⁻¹
   infix  8 -_
@@ -423,15 +563,35 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     isField  : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹
 
   open IsField isField public
+    hiding (module Unordered)
 
   divisionRing : DivisionRing c ℓ₁ ℓ₂
   divisionRing = record { isDivisionRing = isDivisionRing }
 
-  open DivisionRing divisionRing
+  open DivisionRing divisionRing public
     using
     ( _≉_; _≤_; _>_; _≥_
+    ; rawRing; rawField; ring
     ; +-rawMagma; +-rawMonoid; +-rawGroup
     ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
     ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup
     ; *-magma; *-semigroup; *-monoid; *-almostGroup
     )
+
+  commutativeRing : CommutativeRing c ℓ₁ ℓ₂
+  commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+  module Unordered where
+    field′ : NoOrder′.Field c ℓ₁
+    field′ =
+      record { isField = IsField.Unordered.isField isField }
+
+    open NoOrder′.Field field′ public
+      using
+      ( +-rawMagma; +-rawMonoid
+      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; rawSemiring; rawRing
+      ; semiring; ring; divisionRing
+      )
+
+    open IsField.Unordered isField public
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
index 9dc0043..6f6b38d 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
@@ -18,11 +18,11 @@ module Helium.Algebra.Ordered.StrictTotal.Structures
 import Algebra.Consequences.Setoid as Consequences
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-import Algebra.Structures _≈_ as Unordered
+import Algebra.Structures _≈_ as NoOrder
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Helium.Algebra.Core
 open import Helium.Algebra.Definitions _≈_
-open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup)
+import Helium.Algebra.Structures _≈_ as NoOrder′
 open import Helium.Algebra.Ordered.Definitions _<_
 open import Level using (_⊔_)
 
@@ -52,26 +52,55 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   ∙-invariantʳ : RightInvariant ∙
   ∙-invariantʳ = proj₂ ∙-invariant
 
+  module Unordered where
+    isMagma : NoOrder.IsMagma ∙
+    isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
 record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isMagma : IsMagma ∙
     assoc   : Associative ∙
 
   open IsMagma isMagma public
+    hiding (module Unordered)
+
+  module Unordered where
+    isSemigroup : NoOrder.IsSemigroup ∙
+    isSemigroup = record
+      { isMagma = IsMagma.Unordered.isMagma isMagma
+      ; assoc   = assoc
+      }
+
+    open NoOrder.IsSemigroup isSemigroup public
+      using (isMagma)
 
-record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsMonoid (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    isSemigroup : IsSemigroup ∙
-    identity    : Identity ε ∙
+    isSemigroup : IsSemigroup _∙_
+    identity    : Identity ε _∙_
 
   open IsSemigroup isSemigroup public
+    hiding (module Unordered)
 
-  identityˡ : LeftIdentity ε ∙
+  identityˡ : LeftIdentity ε _∙_
   identityˡ = proj₁ identity
 
-  identityʳ : RightIdentity ε ∙
+  identityʳ : RightIdentity ε _∙_
   identityʳ = proj₂ identity
 
+  identity² : (ε ∙ ε) ≈ ε
+  identity² = identityˡ ε
+
+  module Unordered where
+    isMonoid : NoOrder.IsMonoid _∙_ ε
+    isMonoid = record
+      { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup
+      ; identity    = identity
+      }
+
+    open NoOrder.IsMonoid isMonoid public
+      using (isMagma; isSemigroup)
+
 record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isMonoid  : IsMonoid _∙_ ε
@@ -79,6 +108,7 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
     ⁻¹-cong   : Congruent₁ _⁻¹
 
   open IsMonoid isMonoid public
+    hiding (module Unordered)
 
   infixl 6 _-_
   _-_ : Op₂ A
@@ -98,6 +128,17 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
   uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
                 strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ
 
+  module Unordered where
+    isGroup : NoOrder.IsGroup _∙_ ε _⁻¹
+    isGroup = record
+      { isMonoid = IsMonoid.Unordered.isMonoid isMonoid
+      ; inverse  = inverse
+      ; ⁻¹-cong  = ⁻¹-cong
+      }
+
+    open NoOrder.IsGroup isGroup public
+      using (isMagma; isSemigroup; isMonoid)
+
 record IsAbelianGroup (∙ : Op₂ A)
                       (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -105,14 +146,25 @@ record IsAbelianGroup (∙ : Op₂ A)
     comm    : Commutative ∙
 
   open IsGroup isGroup public
+    hiding (module Unordered)
+
+  module Unordered where
+    isAbelianGroup : NoOrder.IsAbelianGroup ∙ ε ⁻¹
+    isAbelianGroup = record
+      { isGroup = IsGroup.Unordered.isGroup isGroup
+      ; comm    = comm
+      }
 
-record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    open NoOrder.IsAbelianGroup isAbelianGroup public
+      using (isMagma; isSemigroup; isMonoid; isGroup)
+
+record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    +-isAbelianGroup  : IsAbelianGroup + 0# -_
-    *-isMonoid        : Unordered.IsMonoid * 1#
-    distrib           : * DistributesOver +
-    zero              : Zero 0# *
-    preservesPositive : PreservesPositive 0# *
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isMonoid       : NoOrder.IsMonoid _*_ 1#
+    distrib          : _*_ DistributesOver +
+    zero             : Zero 0# _*_
+    0<a+0<b⇒0<ab     : PreservesPositive 0# _*_
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -120,9 +172,13 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; ∙-cong                 to +-cong
     ; ∙-congˡ                to +-congˡ
     ; ∙-congʳ                to +-congʳ
+    ; ∙-invariant            to +-invariant
+    ; ∙-invariantˡ           to +-invariantˡ
+    ; ∙-invariantʳ           to +-invariantʳ
     ; identity               to +-identity
     ; identityˡ              to +-identityˡ
     ; identityʳ              to +-identityʳ
+    ; identity²              to +-identity²
     ; inverse                to -‿inverse
     ; inverseˡ               to -‿inverseˡ
     ; inverseʳ               to -‿inverseʳ
@@ -133,8 +189,9 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; isMonoid               to +-isMonoid
     ; isGroup                to +-isGroup
     )
+    hiding (module Unordered)
 
-  open Unordered.IsMonoid *-isMonoid public
+  open NoOrder.IsMonoid *-isMonoid public
     using ()
     renaming
     ( assoc       to *-assoc
@@ -148,18 +205,33 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; isSemigroup to *-isSemigroup
     )
 
-  distribˡ : * DistributesOverˡ +
+  *-identity² : (1# * 1#) ≈ 1#
+  *-identity² = *-identityˡ 1#
+
+  distribˡ : _*_ DistributesOverˡ +
   distribˡ = proj₁ distrib
 
-  distribʳ : * DistributesOverʳ +
+  distribʳ : _*_ DistributesOverʳ +
   distribʳ = proj₂ distrib
 
-  zeroˡ : LeftZero 0# *
+  zeroˡ : LeftZero 0# _*_
   zeroˡ = proj₁ zero
 
-  zeroʳ : RightZero 0# *
+  zeroʳ : RightZero 0# _*_
   zeroʳ = proj₂ zero
 
+  module Unordered where
+    isRing : NoOrder.IsRing + _*_ -_ 0# 1#
+    isRing = record
+      { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+      ; *-isMonoid       = *-isMonoid
+      ; distrib          = distrib
+      ; zero             = zero
+      }
+
+    open NoOrder.IsRing isRing
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup)
+
 record IsCommutativeRing
          (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -167,16 +239,27 @@ record IsCommutativeRing
     *-comm : Commutative *
 
   open IsRing isRing public
+    hiding (module Unordered)
+
+  module Unordered where
+    isCommutativeRing : NoOrder.IsCommutativeRing + * (-) 0# 1#
+    isCommutativeRing = record
+      { isRing = IsRing.Unordered.isRing isRing
+      ; *-comm = *-comm
+      }
+
+    open NoOrder.IsCommutativeRing isCommutativeRing public
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
 
 record IsDivisionRing
          (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
          (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    +-isAbelianGroup  : IsAbelianGroup + 0# -_
-    *-isAlmostGroup   : IsAlmostGroup _*_ 0# 1# _⁻¹
-    distrib           : _*_ DistributesOver +
-    zero              : Zero 0# _*_
-    preservesPositive : PreservesPositive 0# _*_
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isAlmostGroup  : NoOrder′.IsAlmostGroup _*_ 0# 1# _⁻¹
+    distrib          : _*_ DistributesOver +
+    zero             : Zero 0# _*_
+    0<a+0<b⇒0<ab     : PreservesPositive 0# _*_
 
   infixl 7 _/_
   _/_ : AlmostOp₂ _≈_ 0#
@@ -203,8 +286,9 @@ record IsDivisionRing
     ; isMonoid               to +-isMonoid
     ; isGroup                to +-isGroup
     )
+    hiding (module Unordered)
 
-  open IsAlmostGroup *-isAlmostGroup public
+  open NoOrder′.IsAlmostGroup *-isAlmostGroup public
     using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
     renaming
     ( assoc       to *-assoc
@@ -228,12 +312,24 @@ record IsDivisionRing
     ; *-isMonoid = *-isMonoid
     ; distrib = distrib
     ; zero = zero
-    ; preservesPositive = preservesPositive
+    ; 0<a+0<b⇒0<ab = 0<a+0<b⇒0<ab
     }
 
   open IsRing isRing public
     using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ)
 
+  module Unordered where
+    isDivisionRing : NoOrder′.IsDivisionRing + _*_ -_ 0# 1# _⁻¹
+    isDivisionRing = record
+      { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+      ; *-isAlmostGroup  = *-isAlmostGroup
+      ; distrib          = distrib
+      ; zero             = zero
+      }
+
+    open NoOrder′.IsDivisionRing isDivisionRing
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
+
 record IsField
          (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
          (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -242,9 +338,23 @@ record IsField
     *-comm         : Commutative *
 
   open IsDivisionRing isDivisionRing public
+    hiding (module Unordered)
 
   isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
   isCommutativeRing = record
     { isRing = isRing
     ; *-comm = *-comm
     }
+
+  module Unordered where
+    isField : NoOrder′.IsField + * -_ 0# 1# ⁻¹
+    isField = record
+      { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing
+      ; *-comm         = *-comm
+      }
+
+    open NoOrder′.IsField isField
+      using
+      ( +-isMagma; +-isSemigroup; +-isMonoid; +-isGroup
+      ; isRing; isDivisionRing
+      )
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 146dbf9..d75ddba 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -8,112 +8,80 @@
 
 module Helium.Data.Pseudocode where
 
-open import Algebra.Bundles using (RawRing)
 open import Algebra.Core
 import Algebra.Definitions.RawSemiring as RS
 open import Data.Bool.Base using (Bool; if_then_else_)
+open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base as Fin hiding (cast)
 import Data.Fin.Properties as Fₚ
 import Data.Fin.Induction as Induction
 open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Functional
 open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
 import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
 open import Function using (_$_; _∘′_; id)
-open import Helium.Algebra.Bundles using (RawField; RawBooleanAlgebra)
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+open import Helium.Algebra.Decidable.Bundles
+  using (BooleanAlgebra; RawBooleanAlgebra)
+import Helium.Algebra.Decidable.Construct.Pointwise as Pw
+open import Helium.Algebra.Morphism.Structures
 open import Level using (_⊔_) renaming (suc to ℓsuc)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
-open import Relation.Nullary using (does)
-open import Relation.Nullary.Decidable.Core using (False; toWitnessFalse)
+import Relation.Binary.Reasoning.StrictPartialOrder as Reasoning
+open import Relation.Binary.Structures using (IsStrictTotalOrder)
+open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary.Decidable.Core
+  using (False; toWitnessFalse; fromWitnessFalse)
 
 record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
-  infix 6 _-ᶻ_
-  infix 4 _≟ᵇ_ _≟ᶻ_ _<ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ_ _<ʳ?_
-
   field
     bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂
-    integerRawRing : RawRing i₁ i₂
-    realRawField : RawField r₁ r₂
-
-  open RawBooleanAlgebra bitRawBooleanAlgebra public
-    using ()
-    renaming (Carrier to Bit; _≈_ to _≈ᵇ₁_; _≉_ to _≉ᵇ₁_; ⊤ to 1𝔹; ⊥ to 0𝔹)
-
-  module bitsRawBooleanAlgebra {n} = RawBooleanAlgebra record
-    { _≈_ = Pointwise (RawBooleanAlgebra._≈_ bitRawBooleanAlgebra) {n}
-    ; _∨_ = zipWith (RawBooleanAlgebra._∨_ bitRawBooleanAlgebra)
-    ; _∧_ = zipWith (RawBooleanAlgebra._∧_ bitRawBooleanAlgebra)
-    ; ¬_ = map (RawBooleanAlgebra.¬_ bitRawBooleanAlgebra)
-    ; ⊤ = replicate (RawBooleanAlgebra.⊤ bitRawBooleanAlgebra)
-    ; ⊥ = replicate (RawBooleanAlgebra.⊥ bitRawBooleanAlgebra)
-    }
-
-  open bitsRawBooleanAlgebra public
-    hiding (Carrier)
-    renaming (_≈_ to _≈ᵇ_; _≉_ to _≉ᵇ_; ⊤ to ones; ⊥ to zeros)
-
-  Bits = λ n → bitsRawBooleanAlgebra.Carrier {n}
-
-  open RawRing integerRawRing public
-    renaming
-    ( Carrier to ℤ; _≈_ to _≈ᶻ_; _≉_ to _≉ᶻ_
-    ; _+_ to _+ᶻ_; _*_ to _*ᶻ_; -_ to -ᶻ_; 0# to 0ℤ; 1# to 1ℤ
-    ; rawSemiring to integerRawSemiring
-    ; +-rawMagma to +ᶻ-rawMagma; +-rawMonoid to +ᶻ-rawMonoid
-    ; *-rawMagma to *ᶻ-rawMagma; *-rawMonoid to *ᶻ-rawMonoid
-    ; +-rawGroup to +ᶻ-rawGroup
-    )
-
-  _-ᶻ_ : Op₂ ℤ
-  x -ᶻ y = x +ᶻ -ᶻ y
-
-  open RS integerRawSemiring public using ()
-    renaming
-    ( _×_ to _×ᶻ_; _×′_ to _×′ᶻ_; sum to sumᶻ
-    ; _^_ to _^ᶻ_; _^′_ to _^′ᶻ_; product to productᶻ
-    )
-
-  open RawField realRawField public
-    renaming
-    ( Carrier to ℝ; _≈_ to _≈ʳ_; _≉_ to _≉ʳ_
-    ; _+_ to _+ʳ_; _*_ to _*ʳ_; -_ to -ʳ_; 0# to 0ℝ; 1# to 1ℝ; _-_ to _-ʳ_
-    ; rawSemiring to realRawSemiring; rawRing to realRawRing
-    ; +-rawMagma to +ʳ-rawMagma; +-rawMonoid to +ʳ-rawMonoid
-    ; *-rawMagma to *ʳ-rawMagma; *-rawMonoid to *ʳ-rawMonoid
-    ; +-rawGroup to +ʳ-rawGroup; *-rawAlmostGroup to *ʳ-rawAlmostGroup
-    )
-
-  open RS realRawSemiring public using ()
-    renaming
-    ( _×_ to _×ʳ_; _×′_ to _×′ʳ_; sum to sumʳ
-    ; _^_ to _^ʳ_; _^′_ to _^′ʳ_; product to productʳ
-    )
-
+    integerRawRing : RawRing i₁ i₂ i₃
+    realRawField : RawField r₁ r₂ r₃
+
+  bitsRawBooleanAlgebra : ℕ → RawBooleanAlgebra b₁ b₂
+  bitsRawBooleanAlgebra =  Pw.rawBooleanAlgebra  bitRawBooleanAlgebra
+
+  module 𝔹 = RawBooleanAlgebra bitRawBooleanAlgebra
+    renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹)
+  module Bits {n} = RawBooleanAlgebra (bitsRawBooleanAlgebra n)
+    renaming (⊤ to ones; ⊥ to zeros)
+  module ℤ = RawRing integerRawRing renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ)
+  module ℝ = RawField realRawField renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ)
+  module ℤ′ = RS ℤ.Unordered.rawSemiring
+  module ℝ′ = RS ℝ.Unordered.rawSemiring
+
+  Bits : ℕ → Set b₁
+  Bits n = Bits.Carrier {n}
+
+  open 𝔹 public using (Bit; 1𝔹; 0𝔹)
+  open Bits public using (ones; zeros)
+  open ℤ public using (ℤ; 1ℤ; 0ℤ)
+  open ℝ public using (ℝ; 1ℝ; 0ℝ)
+
+  infix 4 _≟ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ?_ _≟ᵇ₁_ _≟ᵇ_
   field
-    _≟ᶻ_  : Decidable _≈ᶻ_
-    _<ᶻ_  : Rel ℤ i₃
-    _<ᶻ?_ : Decidable _<ᶻ_
-
-    _≟ʳ_  : Decidable _≈ʳ_
-    _<ʳ_  : Rel ℝ r₃
-    _<ʳ?_ : Decidable _<ʳ_
+    _≟ᶻ_  : Decidable ℤ._≈_
+    _<ᶻ?_ : Decidable ℤ._<_
+    _≟ʳ_  : Decidable ℝ._≈_
+    _<ʳ?_ : Decidable ℝ._<_
+    _≟ᵇ₁_ : Decidable 𝔹._≈_
 
-    _≟ᵇ₁_ : Decidable _≈ᵇ₁_
-
-  _≟ᵇ_ : ∀ {n} → Decidable (_≈ᵇ_ {n})
+  _≟ᵇ_ : ∀ {n} → Decidable (Bits._≈_ {n})
   _≟ᵇ_ = Pwₚ.decidable _≟ᵇ₁_
 
   field
-    float : ℤ → ℝ
-    round : ℝ → ℤ
+    _/1 : ℤ → ℝ
+    ⌊_⌋ : ℝ → ℤ
 
   cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n
   cast eq x i = x $ Fin.cast (P.sym eq) i
 
   2ℤ : ℤ
-  2ℤ = 2 ×′ᶻ 1ℤ
+  2ℤ = 2 ℤ′.×′ 1ℤ
 
   getᵇ : ∀ {n} → Fin n → Bits n → Bit
   getᵇ i x = x (opposite i)
@@ -148,18 +116,18 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
 
   infixl 7 _div_ _mod_
 
-  _div_ : ∀ (x y : ℤ) → {y≉0 : False (float y ≟ʳ 0ℝ)} → ℤ
-  (x div y) {y≉0} = round (float x *ʳ toWitnessFalse y≉0 ⁻¹)
+  _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
+  (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋
 
-  _mod_ : ∀ (x y : ℤ) → {y≉0 : False (float y ≟ʳ 0ℝ)} → ℤ
-  (x mod y) {y≉0} = x -ᶻ y *ᶻ (x div y) {y≉0}
+  _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
+  (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0}
 
   infixl 5 _<<_
   _<<_ : ℤ → ℕ → ℤ
-  x << n = x *ᶻ 2ℤ ^′ᶻ n
+  x << n = 2ℤ ℤ′.^′ n ℤ.* x
 
   module ShiftNotZero
-    (1<<n≉0 : ∀ n → False (float (1ℤ << n) ≟ʳ 0ℝ))
+    (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
     where
 
     infixl 5 _>>_
@@ -179,8 +147,266 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     sliceᶻ (suc n) (suc i) x = sliceᶻ n i (x >> 1)
 
   uint : ∀ {n} → Bits n → ℤ
-  uint x = sumᶻ λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ
+  uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ
 
   sint : ∀ {n} → Bits n → ℤ
   sint {zero}  x = 0ℤ
-  sint {suc n} x = uint x -ᶻ (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ)
+  sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ)
+
+record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
+                  Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
+  field
+    bitBooleanAlgebra : BooleanAlgebra b₁ b₂
+    integerRing       : CommutativeRing i₁ i₂ i₃
+    realField         : Field r₁ r₂ r₃
+
+  bitsBooleanAlgebra : ℕ → BooleanAlgebra b₁ b₂
+  bitsBooleanAlgebra = Pw.booleanAlgebra bitBooleanAlgebra
+
+  module 𝔹 = BooleanAlgebra bitBooleanAlgebra
+    renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹)
+  module Bits {n} = BooleanAlgebra (bitsBooleanAlgebra n)
+    renaming (⊤ to ones; ⊥ to zeros)
+  module ℤ = CommutativeRing integerRing
+    renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ)
+  module ℝ = Field realField
+    renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ)
+
+  Bits : ℕ → Set b₁
+  Bits n = Bits.Carrier {n}
+
+  open 𝔹 public using (Bit; 1𝔹; 0𝔹)
+  open Bits public using (ones; zeros)
+  open ℤ public using (ℤ; 1ℤ; 0ℤ)
+  open ℝ public using (ℝ; 1ℝ; 0ℝ)
+
+  module ℤ-Reasoning = Reasoning ℤ.strictPartialOrder
+  module ℝ-Reasoning = Reasoning ℝ.strictPartialOrder
+
+  field
+    integerDiscrete : ∀ x y → y ℤ.≤ x ⊎ x ℤ.+ 1ℤ ℤ.≤ y
+    1≉0 : 1ℤ ℤ.≉ 0ℤ
+
+    _/1 : ℤ → ℝ
+    ⌊_⌋ : ℝ → ℤ
+    /1-isHomo : IsRingHomomorphism ℤ.Unordered.rawRing ℝ.Unordered.rawRing _/1
+    ⌊⌋-isHomo : IsRingHomomorphism ℝ.Unordered.rawRing ℤ.Unordered.rawRing ⌊_⌋
+    /1-mono : ∀ x y → x ℤ.< y → x /1 ℝ.< y /1
+    ⌊⌋-floor : ∀ x y → x ℤ.≤ ⌊ y ⌋ → ⌊ y ⌋ ℤ.< x ℤ.+ 1ℤ
+    ⌊⌋∘/1≗id : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x
+
+  module /1 = IsRingHomomorphism /1-isHomo renaming (⟦⟧-cong to cong)
+  module ⌊⌋ = IsRingHomomorphism ⌊⌋-isHomo renaming (⟦⟧-cong to cong)
+
+  bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂
+  bitRawBooleanAlgebra = record
+    { _≈_ = _≈_
+    ; _∨_ = _∨_
+    ; _∧_ = _∧_
+    ; ¬_  = ¬_
+    ; ⊤   = ⊤
+    ; ⊥   = ⊥
+    }
+    where open BooleanAlgebra bitBooleanAlgebra
+
+  rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃
+  rawPseudocode = record
+    { bitRawBooleanAlgebra = bitRawBooleanAlgebra
+    ; integerRawRing = ℤ.rawRing
+    ; realRawField = ℝ.rawField
+    ; _≟ᶻ_ = ℤ._≟_
+    ; _<ᶻ?_ = ℤ._<?_
+    ; _≟ʳ_ = ℝ._≟_
+    ; _<ʳ?_ = ℝ._<?_
+    ; _≟ᵇ₁_ = 𝔹._≟_
+    ; _/1 = _/1
+    ; ⌊_⌋ = ⌊_⌋
+    }
+
+  open RawPseudocode rawPseudocode public
+    using
+    ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit
+    ; _div_; _mod_; _<<_; uint; sint
+    )
+
+  private
+    -- FIXME: move almost all of these proofs into a separate module
+    a<b⇒ca<cb : ∀ {a b c} → 0ℤ ℤ.< c → a ℤ.< b → c ℤ.* a ℤ.< c ℤ.* b
+    a<b⇒ca<cb {a} {b} {c} 0<c a<b = begin-strict
+      c ℤ.* a                     ≈˘⟨ ℤ.+-identityʳ _ ⟩
+      c ℤ.* a ℤ.+ 0ℤ              <⟨  ℤ.+-invariantˡ _ $ ℤ.0<a+0<b⇒0<ab 0<c 0<b-a ⟩
+      c ℤ.* a ℤ.+ c ℤ.* (b ℤ.- a) ≈˘⟨ ℤ.distribˡ c a (b ℤ.- a) ⟩
+      c ℤ.* (a ℤ.+ (b ℤ.- a))     ≈⟨  ℤ.*-congˡ $ ℤ.+-congˡ $ ℤ.+-comm b (ℤ.- a) ⟩
+      c ℤ.* (a ℤ.+ (ℤ.- a ℤ.+ b)) ≈˘⟨ ℤ.*-congˡ $ ℤ.+-assoc a (ℤ.- a) b ⟩
+      c ℤ.* ((a ℤ.+ ℤ.- a) ℤ.+ b) ≈⟨  ℤ.*-congˡ $ ℤ.+-congʳ $ ℤ.-‿inverseʳ a ⟩
+      c ℤ.* (0ℤ ℤ.+ b)            ≈⟨  (ℤ.*-congˡ $ ℤ.+-identityˡ b) ⟩
+      c ℤ.* b                     ∎
+      where
+      open ℤ-Reasoning
+
+      0<b-a : 0ℤ ℤ.< b ℤ.- a
+      0<b-a = begin-strict
+        0ℤ      ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+        a ℤ.- a <⟨  ℤ.+-invariantʳ (ℤ.- a) a<b ⟩
+        b ℤ.- a ∎
+
+    -‿idem : ∀ x → ℤ.- (ℤ.- x) ℤ.≈ x
+    -‿idem x = begin-equality
+      ℤ.- (ℤ.- x)             ≈˘⟨ ℤ.+-identityˡ _ ⟩
+      0ℤ ℤ.- ℤ.- x            ≈˘⟨ ℤ.+-congʳ $ ℤ.-‿inverseʳ x ⟩
+      x ℤ.- x ℤ.- ℤ.- x       ≈⟨  ℤ.+-assoc x (ℤ.- x) _ ⟩
+      x ℤ.+ (ℤ.- x ℤ.- ℤ.- x) ≈⟨  ℤ.+-congˡ $ ℤ.-‿inverseʳ (ℤ.- x) ⟩
+      x ℤ.+ 0ℤ                ≈⟨  ℤ.+-identityʳ x ⟩
+      x                       ∎
+      where open ℤ-Reasoning
+
+    -a*b≈-ab : ∀ a b → ℤ.- a ℤ.* b ℤ.≈ ℤ.- (a ℤ.* b)
+    -a*b≈-ab a b = begin-equality
+      ℤ.- a ℤ.* b                           ≈˘⟨ ℤ.+-identityʳ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ 0ℤ                    ≈˘⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ (a ℤ.* b ℤ.- a ℤ.* b) ≈˘⟨ ℤ.+-assoc _ _ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ a ℤ.* b ℤ.- a ℤ.* b   ≈˘⟨ ℤ.+-congʳ $ ℤ.distribʳ b _ a ⟩
+      (ℤ.- a ℤ.+ a) ℤ.* b ℤ.- a ℤ.* b       ≈⟨  ℤ.+-congʳ $ ℤ.*-congʳ $ ℤ.-‿inverseˡ a ⟩
+      0ℤ ℤ.* b ℤ.- a ℤ.* b                  ≈⟨  ℤ.+-congʳ $ ℤ.zeroˡ b ⟩
+      0ℤ ℤ.- a ℤ.* b                        ≈⟨  ℤ.+-identityˡ _ ⟩
+      ℤ.- (a ℤ.* b)                         ∎
+      where open ℤ-Reasoning
+
+    a*-b≈-ab : ∀ a b → a ℤ.* ℤ.- b ℤ.≈ ℤ.- (a ℤ.* b)
+    a*-b≈-ab a b = begin-equality
+      a ℤ.* ℤ.- b   ≈⟨ ℤ.*-comm a (ℤ.- b) ⟩
+      ℤ.- b ℤ.* a   ≈⟨ -a*b≈-ab b a ⟩
+      ℤ.- (b ℤ.* a) ≈⟨ ℤ.-‿cong $ ℤ.*-comm b a ⟩
+      ℤ.- (a ℤ.* b) ∎
+      where open ℤ-Reasoning
+
+    0<a⇒0>-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a
+    0<a⇒0>-a {a} 0<a = begin-strict
+      ℤ.- a    ≈˘⟨ ℤ.+-identityˡ _ ⟩
+      0ℤ ℤ.- a <⟨  ℤ.+-invariantʳ _ 0<a ⟩
+      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
+      0ℤ       ∎
+      where open ℤ-Reasoning
+
+    0>a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a
+    0>a⇒0<-a {a} 0>a = begin-strict
+      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+      a ℤ.- a  <⟨  ℤ.+-invariantʳ _ 0>a ⟩
+      0ℤ ℤ.- a ≈⟨  ℤ.+-identityˡ _ ⟩
+      ℤ.- a    ∎
+      where open ℤ-Reasoning
+
+    0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a
+    0<-a⇒0>a {a} 0<-a = begin-strict
+      a        ≈˘⟨ ℤ.+-identityʳ a ⟩
+      a ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ a 0<-a ⟩
+      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
+      0ℤ       ∎
+      where open ℤ-Reasoning
+
+    0>-a⇒0<a : ∀ {a} → 0ℤ ℤ.> ℤ.- a → 0ℤ ℤ.< a
+    0>-a⇒0<a {a} 0>-a = begin-strict
+      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+      a ℤ.- a  <⟨  ℤ.+-invariantˡ a 0>-a ⟩
+      a ℤ.+ 0ℤ ≈⟨  ℤ.+-identityʳ a ⟩
+      a        ∎
+      where open ℤ-Reasoning
+
+    0>a+0<b⇒0>ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b
+    0>a+0<b⇒0>ab {a} {b} 0>a 0<b = 0<-a⇒0>a $ begin-strict
+      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) 0<b ⟩
+      ℤ.- a ℤ.* b     ≈⟨ -a*b≈-ab a b ⟩
+      ℤ.- (a ℤ.* b)   ∎
+      where open ℤ-Reasoning
+
+    0<a+0>b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b
+    0<a+0>b⇒0>ab {a} {b} 0<a 0>b = 0<-a⇒0>a $ begin-strict
+      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab 0<a (0>a⇒0<-a 0>b) ⟩
+      a ℤ.* ℤ.- b     ≈⟨ a*-b≈-ab a b ⟩
+      ℤ.- (a ℤ.* b)   ∎
+      where open ℤ-Reasoning
+
+    0>a+0>b⇒0<ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b
+    0>a+0>b⇒0<ab {a} {b} 0>a 0>b = begin-strict
+      0ℤ                  <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩
+      ℤ.- a ℤ.* ℤ.- b     ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩
+      ℤ.- (a ℤ.* ℤ.- b)   ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩
+      ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩
+      a ℤ.* b             ∎
+      where open ℤ-Reasoning
+
+    a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ
+    a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ
+    ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0<ab a<0 b<0
+    ... | tri< a<0 _ _ | tri≈ _ b≈0 _ = b≉0 b≈0
+    ... | tri< a<0 _ _ | tri> _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0<b⇒0>ab a<0 b>0
+    ... | tri≈ _ a≈0 _ | _            = a≉0 a≈0
+    ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0<a+0>b⇒0>ab a>0 b<0
+    ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0
+    ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.0<a+0<b⇒0<ab a>0 b>0
+
+    ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ
+    ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ
+    ... | yes a≈0 | _       = inj₁ a≈0
+    ... | no a≉0  | yes b≈0 = inj₂ b≈0
+    ... | no a≉0  | no b≉0  = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0)
+
+    2a<<n≈a<<1+n : ∀ a n → 2ℤ ℤ.* (a << n) ℤ.≈ a << suc n
+    2a<<n≈a<<1+n a zero    = ℤ.*-congˡ $ ℤ.*-identityˡ a
+    2a<<n≈a<<1+n a (suc n) = begin-equality
+      2ℤ ℤ.* (a << suc n) ≈˘⟨ ℤ.*-assoc 2ℤ _ a ⟩
+      (2ℤ ℤ.* _) ℤ.* a    ≈⟨  ℤ.*-congʳ $ ℤ.*-comm 2ℤ _ ⟩
+      a << suc (suc n)    ∎
+      where open ℤ-Reasoning
+
+    0<1 : 0ℤ ℤ.< 1ℤ
+    0<1 with ℤ.compare 0ℤ 1ℤ
+    ... | tri< 0<1 _ _ = 0<1
+    ... | tri≈ _ 0≈1 _ = ⊥-elim (1≉0 (ℤ.Eq.sym 0≈1))
+    ... | tri> _ _ 0>1 = begin-strict
+        0ℤ                  ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩
+        ℤ.- 1ℤ ℤ.* 0ℤ       <⟨  a<b⇒ca<cb (0>a⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩
+        ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ   ≈⟨  -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩
+        ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨  ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩
+        ℤ.- (ℤ.- 1ℤ)        ≈⟨  -‿idem 1ℤ ⟩
+        1ℤ                  ∎
+      where open ℤ-Reasoning
+
+    0<2 : 0ℤ ℤ.< 2ℤ
+    0<2 = begin-strict
+      0ℤ        ≈˘⟨ ℤ.+-identity² ⟩
+      0ℤ ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ 0ℤ 0<1 ⟩
+      0ℤ ℤ.+ 1ℤ <⟨  ℤ.+-invariantʳ 1ℤ 0<1 ⟩
+      2ℤ        ∎
+      where open ℤ-Reasoning
+
+    1<<n≉0 : ∀ n → 1ℤ << n ℤ.≉ 0ℤ
+    1<<n≉0 zero          eq = 1≉0 1≈0
+      where
+      open ℤ-Reasoning
+      1≈0 = begin-equality
+        1ℤ        ≈˘⟨ ℤ.*-identity² ⟩
+        1ℤ ℤ.* 1ℤ ≈⟨  eq ⟩
+        0ℤ        ∎
+    1<<n≉0 (suc zero)    eq = ℤ.irrefl 0≈2 0<2
+      where
+      open ℤ-Reasoning
+      0≈2 = begin-equality
+        0ℤ        ≈˘⟨ eq ⟩
+        2ℤ ℤ.* 1ℤ ≈⟨  ℤ.*-identityʳ 2ℤ ⟩
+        2ℤ        ∎
+    1<<n≉0 (suc (suc n)) eq =
+      [ (λ 2≈0 → ℤ.irrefl (ℤ.Eq.sym 2≈0) 0<2) , 1<<n≉0 (suc n) ]′
+      $ ab≈0⇒a≈0⊎b≈0 $ ℤ.Eq.trans (2a<<n≈a<<1+n 1ℤ (suc n)) eq
+
+    1<<n≉0ℝ : ∀ n → (1ℤ << n) /1 ℝ.≉ 0ℝ
+    1<<n≉0ℝ n eq = 1<<n≉0 n $ (begin-equality
+      1ℤ << n          ≈˘⟨ ⌊⌋∘/1≗id (1ℤ << n) ⟩
+      ⌊ (1ℤ << n) /1 ⌋ ≈⟨  ⌊⌋.cong $ eq ⟩
+      ⌊ 0ℝ ⌋           ≈⟨  ⌊⌋.0#-homo ⟩
+      0ℤ               ∎)
+      where open ℤ-Reasoning
+
+    open RawPseudocode rawPseudocode using (module ShiftNotZero)
+
+  open ShiftNotZero (λ n → fromWitnessFalse (1<<n≉0ℝ n)) public
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 3a616c0..046fff8 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -165,7 +165,7 @@ copyMasked dest =
   ∙end
 
 module fun-sliceᶻ
-  (1<<n≉0 : ∀ n → False (float (1ℤ << n) ≟ʳ 0ℝ))
+  (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
   where
 
   open ShiftNotZero 1<<n≉0
@@ -173,12 +173,12 @@ module fun-sliceᶻ
   signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool)
   signedSatQ n = declare ⦇ true ⦈ $
     -- 0:sat 1:x
-    if ⦇ (λ i → does ((1ℤ << n) +ᶻ -ᶻ 1ℤ <ᶻ? i)) (!# 1) ⦈
+    if ⦇ (λ i → does ((1ℤ << n) ℤ.+ ℤ.- 1ℤ <ᶻ? i)) (!# 1) ⦈
     then
-      var (# 1) ≔ ⦇ ((1ℤ << n) +ᶻ -ᶻ 1ℤ) ⦈
-    else if ⦇ (λ i → does (-ᶻ 1ℤ << n <ᶻ? i)) (!# 1) ⦈
+      var (# 1) ≔ ⦇ ((1ℤ << n) ℤ.+ ℤ.- 1ℤ) ⦈
+    else if ⦇ (λ i → does (ℤ.- 1ℤ << n <ᶻ? i)) (!# 1) ⦈
     then
-      var (# 1) ≔ ⦇ (-ᶻ 1ℤ << n) ⦈
+      var (# 1) ≔ ⦇ (ℤ.- 1ℤ << n) ⦈
     else
       var (# 0) ≔ ⦇ false ⦈
     ∙return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , (!# 0) ⦈
@@ -194,7 +194,7 @@ advanceVPT = declare (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) $
   else (
     if ⦇ (hasBit (# 3)) (!# 0) ⦈
     then
-      elem 4 &VPR-P0 (!# 1) ⟵ (¬_)
+      elem 4 &VPR-P0 (!# 1) ⟵ (Bits.¬_)
     else skip ∙
     (var (# 0) ⟵ λ x → sliceᵇ (# 3) zero x V.++ 0𝔹 ∷ [])) ∙
   if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (!# 1) ⦈
@@ -242,27 +242,27 @@ module _
 -- Instruction semantics
 
 module _
-  (1<<n≉0 : ∀ n → False (float (1ℤ << n) ≟ʳ 0ℝ))
+  (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
   where
 
   open ShiftNotZero 1<<n≉0
   open fun-sliceᶻ 1<<n≉0
 
   vadd : Instr.VAdd → Procedure 2 (Beat , ElmtMask , _)
-  vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y))
+  vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ uint y))
 
   vsub : Instr.VSub → Procedure 2 (Beat , ElmtMask , _)
-  vsub d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ -ᶻ uint y))
+  vsub d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ ℤ.- uint y))
 
   vhsub : Instr.VHSub → Procedure 2 (Beat , ElmtMask , _)
-  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x +ᶻ -ᶻ int y))
+  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x ℤ.+ ℤ.- int y))
     where open Instr.VHSub d ; int = Bool.if unsigned then uint else sint
 
   vmul : Instr.VMul → Procedure 2 (Beat , ElmtMask , _)
-  vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y))
+  vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x ℤ.* sint y))
 
   vmulh : Instr.VMulH → Procedure 2 (Beat , ElmtMask , _)
-  vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x *ᶻ int y +ᶻ rval)))
+  vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x ℤ.* int y ℤ.+ rval)))
     where
     open Instr.VMulH d
     int = Bool.if unsigned then uint else sint
@@ -279,7 +279,7 @@ module _
       -- 0:e 1:sat 2:op₁ 3:result 4:beat 5:elmntMask
       elem (toℕ esize) (&cast (sym e*e≡32) (var (# 3))) (!# 0) ,′ var (# 1) ≔
       call (signedSatQ (toℕ esize-1))
-           ⦇ (λ x y → (2ℤ *ᶻ sint x *ᶻ sint y +ᶻ rval) >> toℕ esize)
+           ⦇ (λ x y → (2ℤ ℤ.* sint x ℤ.* sint y ℤ.+ rval) >> toℕ esize)
              (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0))
              ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
               , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 4))) (!# 0))