diff --git a/Cubical/Algebra/CommRing/Instances/Fast/Int.agda b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda
index e01dde2d62..eddd1e13e9 100644
--- a/Cubical/Algebra/CommRing/Instances/Fast/Int.agda
+++ b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda
@@ -1,8 +1,12 @@
 module Cubical.Algebra.CommRing.Instances.Fast.Int where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 
+open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
+
+open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
 open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
 
 open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
@@ -21,3 +25,113 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
                                  -Cancel Int.+Comm Int.·Assoc
                                  Int.·IdR ·DistR+ Int.·Comm
+
+private
+  variable
+    ℓ : Level
+
+module CanonicalHomFromℤ (R : CommRing ℓ) where
+
+  private
+    module R where
+      open CommRingStr (snd R) public
+      open RingTheory (CommRing→Ring R) public
+
+  suc-fromℕ : ∀ x → R.fromℕ (suc x) ≡ R.1r R.+ R.fromℕ x
+  suc-fromℕ zero    = sym (R.+IdR R.1r)
+  suc-fromℕ (suc x) = refl
+
+  fromℕ-pres+ : (x y : ℕ) → R.fromℕ (x ℕ.+ y) ≡ R.fromℕ x R.+ R.fromℕ y
+  fromℕ-pres+ zero          y = sym (R.+IdL _)
+  fromℕ-pres+ (suc zero)    y = suc-fromℕ y
+  fromℕ-pres+ (suc (suc x)) y = cong (R.1r R.+_) (fromℕ-pres+ (suc x) y) ∙ R.+Assoc _ _ _
+
+  fromℤ-pres- : (x : ℤ) → R.fromℤ (-ℤ x) ≡ R.- R.fromℤ x
+  fromℤ-pres- (pos zero)    = sym R.0Selfinverse
+  fromℤ-pres- (pos (suc n)) = refl
+  fromℤ-pres- (negsuc n)    = sym (R.-Idempotent _)
+
+  suc-fromℤ : ∀ z → R.fromℤ (1 +ℤ z) ≡ R.1r R.+ R.fromℤ (z)
+  suc-fromℤ (pos n)          = suc-fromℕ n
+  suc-fromℤ (negsuc zero)    = sym (R.+InvR R.1r)
+  suc-fromℤ (negsuc (suc n)) =
+       sym (cong (R._+ (R.- R.fromℕ (suc n))) (R.+InvR _) ∙ R.+IdL _)
+    ∙∙ sym (R.+Assoc _ _ _)
+    ∙∙ cong (R.1r R.+_) (R.-Dist _ _)
+
+  fromℤ-pres+' : (n m : ℕ) →
+    R.fromℤ (pos n +ℤ negsuc m) ≡
+    R.fromℤ (pos n) R.+ R.fromℤ (negsuc m)
+  fromℤ-pres+' zero    m = sym (R.+IdL _)
+  fromℤ-pres+' (suc n) m =
+      (cong R.fromℤ (sym (+Assoc 1 (pos n) (negsuc m)))
+    ∙ suc-fromℤ (pos n +ℤ negsuc m))
+    ∙∙ cong (R.1r R.+_) (fromℤ-pres+' n m)
+    ∙∙ R.+Assoc _ _ _
+    ∙ cong (R._+ R.fromℤ (negsuc m))
+     (sym (suc-fromℕ n))
+
+  fromℤ-pres+ : (x y : ℤ) → R.fromℤ (x +ℤ y) ≡ R.fromℤ x R.+ R.fromℤ y
+  fromℤ-pres+ (pos n)    (pos m)    = fromℕ-pres+  n m
+  fromℤ-pres+ (pos n)    (negsuc m) = fromℤ-pres+' n m
+  fromℤ-pres+ (negsuc n) (pos m)    = fromℤ-pres+' m n ∙ R.+Comm _ _
+  fromℤ-pres+ (negsuc n) (negsuc m) =
+      cong (R.-_)
+      (cong (R.1r R.+_) (cong R.fromℕ (sym (ℕ.+-suc n m)))
+        ∙ sym (suc-fromℕ (n ℕ.+ suc m))
+        ∙ fromℕ-pres+ (suc n) (suc m))
+    ∙ sym (R.-Dist _ _)
+
+  fromℕ-pres· : (x y : ℕ) → R.fromℕ (x ℕ.· y) ≡ R.fromℕ x R.· R.fromℕ y
+  fromℕ-pres· zero y    = sym (R.0LeftAnnihilates _)
+  fromℕ-pres· (suc x) y =
+      fromℕ-pres+ y (x ℕ.· y)
+    ∙∙ cong₂ (R._+_) (sym (R.·IdL _)) (fromℕ-pres· x y)
+    ∙∙ sym (R.·DistL+ _ _ _)
+    ∙ cong (R._· R.fromℕ y) (sym (suc-fromℕ x))
+  fromℤ-pres· : (x y : ℤ) → R.fromℤ (x ·ℤ y) ≡ R.fromℤ x R.· R.fromℤ y
+  fromℤ-pres· (pos n) (pos m)    = fromℕ-pres· n m
+  fromℤ-pres· (pos n) (negsuc m) =
+      cong R.fromℤ (sym (-DistR· (pos n) (pos (suc m))))
+    ∙∙ (fromℤ-pres- (pos (n ℕ.· suc m))
+      ∙ cong R.-_ (fromℕ-pres· n (suc m)))
+    ∙∙ sym (R.-DistR· _ _)
+  fromℤ-pres· (negsuc n) (pos m) =
+      cong R.fromℤ (sym (-DistL· (pos (suc n)) (pos m)))
+    ∙∙ (fromℤ-pres- (pos ((suc n) ℕ.· m))
+      ∙ cong R.-_ (fromℕ-pres· (suc n) m))
+    ∙∙ sym (R.-DistL· _ _)
+  fromℤ-pres· (negsuc n) (negsuc m) =
+       fromℕ-pres· (suc n) (suc m)
+    ∙∙ cong₂ R._·_ (sym (R.-Idempotent _)) refl
+    ∙∙ R.-Swap· _ _
+
+  isHomFromℤ : IsCommRingHom (ℤCommRing .snd) R.fromℤ (R .snd)
+  isHomFromℤ .IsCommRingHom.pres0 = refl
+  isHomFromℤ .IsCommRingHom.pres1 = refl
+  isHomFromℤ .IsCommRingHom.pres+ = fromℤ-pres+
+  isHomFromℤ .IsCommRingHom.pres· = fromℤ-pres·
+  isHomFromℤ .IsCommRingHom.pres- = fromℤ-pres-
+
+  fromℤHom : CommRingHom ℤCommRing R
+  fst fromℤHom = R.fromℤ
+  snd fromℤHom = isHomFromℤ
+
+  module _ (φ : CommRingHom ℤCommRing R) where
+
+    open IsCommRingHom (snd φ)
+
+    isUniqueFromℕ : ∀ n → R.fromℕ n ≡ φ $cr pos n
+    isUniqueFromℕ zero            = sym pres0
+    isUniqueFromℕ (suc zero)      = sym pres1
+    isUniqueFromℕ (suc k@(suc n)) = cong₂ R._+_ (sym pres1) (isUniqueFromℕ k)
+                                  ∙ sym (pres+ 1 (pos k))
+
+    isUniqueFromℤ : ∀ n → R.fromℤ n ≡ φ $cr n
+    isUniqueFromℤ (pos n)    = isUniqueFromℕ n
+    isUniqueFromℤ (negsuc n) = cong R.-_ (isUniqueFromℕ (suc n))
+                             ∙ sym (pres- (pos (suc n)))
+
+  isContrHom[ℤCR,-] : isContr (CommRingHom ℤCommRing R)
+  fst isContrHom[ℤCR,-] = fromℤHom
+  snd isContrHom[ℤCR,-] = CommRingHom≡ ∘ funExt ∘ isUniqueFromℤ
diff --git a/Cubical/Algebra/OrderedCommRing.agda b/Cubical/Algebra/OrderedCommRing.agda
index 2aca413aff..ba0a384be4 100644
--- a/Cubical/Algebra/OrderedCommRing.agda
+++ b/Cubical/Algebra/OrderedCommRing.agda
@@ -1,3 +1,4 @@
 module Cubical.Algebra.OrderedCommRing where
 
 open import Cubical.Algebra.OrderedCommRing.Base public
+open import Cubical.Algebra.OrderedCommRing.Properties public
diff --git a/Cubical/Algebra/OrderedCommRing/Base.agda b/Cubical/Algebra/OrderedCommRing/Base.agda
index 29cd5dbb4b..0bf5ca7948 100644
--- a/Cubical/Algebra/OrderedCommRing/Base.agda
+++ b/Cubical/Algebra/OrderedCommRing/Base.agda
@@ -4,20 +4,25 @@ module Cubical.Algebra.OrderedCommRing.Base where
 -}
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.SIP
 
+open import Cubical.Algebra.CommRing.Base
+
 import Cubical.Functions.Logic as L
 
-open import Cubical.Relation.Nullary.Base
+open import Cubical.HITs.PropositionalTruncation as PT
 
-open import Cubical.Algebra.CommRing.Base
+open import Cubical.Reflection.RecordEquiv
 
 open import Cubical.Relation.Binary.Base
-open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice)
-open import Cubical.Relation.Binary.Order.StrictOrder
-
+open import Cubical.Relation.Binary.Order.Poset hiding (
+  isPseudolattice ; isPropIsPseudolattice)
 open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Nullary
 
 open BinaryRelation
 
@@ -53,6 +58,8 @@ record IsOrderedCommRing
                                                                 ; _∧l_ to _⊓_ ; _∨l_ to _⊔_) public
   open IsStrictOrder isStrictOrder hiding (is-set) renaming (is-prop-valued to is-prop-valued< ; is-trans to is-trans<) public
 
+unquoteDecl IsOrderedCommRingIsoΣ = declareRecordIsoΣ IsOrderedCommRingIsoΣ (quote IsOrderedCommRing)
+
 record OrderedCommRingStr (ℓ' : Level) (R : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   constructor orderedcommringstr
   field
@@ -134,3 +141,26 @@ OrderedCommRing→CommRing : OrderedCommRing ℓ ℓ' → CommRing ℓ
 OrderedCommRing→CommRing R .fst = R .fst
 OrderedCommRing→CommRing R .snd = commringstr _ _ _ _ _ isCommRing where
   open OrderedCommRingStr (str R)
+
+isPropIsOrderedCommRing : {R : Type ℓ}
+                          → (0r 1r : R)
+                          → (_+_ _·_ : R → R → R) (-_ : R → R)
+                          → (_<_ _≤_ : R → R → Type ℓ')
+                          → isProp (IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_)
+isPropIsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_ = isOfHLevelRetractFromIso 1
+  IsOrderedCommRingIsoΣ $
+    isPropΣ (isPropIsCommRing _ _ _ _ _) λ isCR →
+    isPropΣ (isPropIsPseudolattice _) λ isPL →
+    isPropΣ (isPropIsStrictOrder _) λ isSO →
+    isProp× (isPropΠ3 λ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ2 λ x y → isOfHLevel≃ 1
+      (IsPoset.is-prop-valued (IsPseudolattice.isPoset isPL) x y)
+      (isProp¬ (y < x))) $
+    isProp× (isPropΠ4 λ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ4 λ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ3 λ _ _ _ → PT.squash₁) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _)
+            (isSO .IsStrictOrder.is-prop-valued _ _)
diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda
index 45a38d41c6..93163da4ef 100644
--- a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda
+++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda
@@ -8,15 +8,20 @@ open import Cubical.Data.Empty as ⊥
 
 open import Cubical.HITs.PropositionalTruncation
 
+open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
+open import Cubical.Data.Nat.Order as ℕ using () renaming (_≤_ to _≤ℕ_ ; _<_ to _<ℕ_)
+import Cubical.Data.Nat.Order.Inductive as ℕ
 open import Cubical.Data.Fast.Int as ℤ
   renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
 open import Cubical.Data.Fast.Int.Order
   renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
 
+open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Instances.Fast.Int
 
 open import Cubical.Algebra.OrderedCommRing
+open import Cubical.Algebra.OrderedCommRing.Morphisms
 
 open import Cubical.Relation.Nullary
 
@@ -64,3 +69,100 @@ isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
     isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
     isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
     isOrderedCommRingℤ .0<1             = zero-<possuc
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where
+
+  open CanonicalHomFromℤ (OrderedCommRing→CommRing R)
+  open OrderedCommRingTheory R
+
+  private
+    module R where
+      open OrderedCommRingStr (snd R) public
+      open RingTheory (OrderedCommRing→Ring R) using (fromℕ ; fromℤ) public
+
+  1≤fromℕsuc : ∀ n → R.1r R.≤ R.fromℕ (suc n)
+  1≤fromℕsuc zero    = R.is-refl R.1r
+  1≤fromℕsuc (suc n) =
+    subst (R._≤ R.fromℕ (suc (suc n))) (R.+IdL R.1r) (+Mono≤ _ _ _ _ 0≤1 (1≤fromℕsuc n))
+
+  0<fromℕsuc : ∀ n → R.0r R.< R.fromℕ (suc n)
+  0<fromℕsuc n = R.<-≤-trans _ _ _ R.0<1 (1≤fromℕsuc n)
+
+  0≤fromℕ : ∀ n → R.0r R.≤ R.fromℕ n
+  0≤fromℕ zero    = R.is-refl R.0r
+  0≤fromℕ (suc n) = R.<-≤-weaken _ _ (0<fromℕsuc n)
+
+  fromℕ-pres≤ᵗ : ∀ m n → m ℕ.≤ᵗ n → R.fromℕ m R.≤ R.fromℕ n
+  fromℕ-pres≤ᵗ zero          n             t = 0≤fromℕ n
+  fromℕ-pres≤ᵗ (suc zero)    (suc n)       t = 1≤fromℕsuc n
+  fromℕ-pres≤ᵗ (suc (suc m)) (suc (suc n)) t =
+    +MonoL≤ _ _ _ (fromℕ-pres≤ᵗ (suc m) (suc n) t)
+
+  fromℕ-pres≤ : ∀ m n → m ≤ℕ n → R.fromℕ m R.≤ R.fromℕ n
+  fromℕ-pres≤ m n = fromℕ-pres≤ᵗ m n ∘ ℕ.≤→≤ᵇ
+
+  fromℕ-pres<ᵗ : ∀ m n → m ℕ.<ᵗ n → R.fromℕ m R.< R.fromℕ n
+  fromℕ-pres<ᵗ zero          (suc n)       t = 0<fromℕsuc n
+  fromℕ-pres<ᵗ (suc zero)    (suc (suc n)) t = <SumLeftPos R.1r _ (0<fromℕsuc n)
+  fromℕ-pres<ᵗ (suc (suc m)) (suc (suc n)) t =
+    +MonoL< _ _ _ (fromℕ-pres<ᵗ (suc m) (suc n) t)
+
+  fromℕ-pres< : ∀ m n → m <ℕ n → R.fromℕ m R.< R.fromℕ n
+  fromℕ-pres< m n = fromℕ-pres<ᵗ m n ∘ ℕ.<→<ᵇ
+
+  fromℤ-pres≤ : ∀ m n → m ≤ℤ n → R.fromℤ m R.≤ R.fromℤ n
+  fromℤ-pres≤ (pos m)    (pos n)    (pos≤pos p)       = fromℕ-pres≤ᵗ m n p
+  fromℤ-pres≤ (negsuc m) (pos n)    negsuc≤pos        =
+    R.is-trans≤ _ _ _ (0≤→-≤0 _ (0≤fromℕ (suc m))) (0≤fromℕ n)
+  fromℤ-pres≤ (negsuc m) (negsuc n) (negsuc≤negsuc p) =
+    -Flip≤ _ _ (fromℕ-pres≤ᵗ (suc n) (suc m) p)
+
+  fromℤ-pres< : ∀ m n → m <ℤ n → R.fromℤ m R.< R.fromℤ n
+  fromℤ-pres< (pos m)    (pos n)    (pos<pos p)       = fromℕ-pres<ᵗ m n p
+  fromℤ-pres< (negsuc m) (pos n)    negsuc<pos        =
+    R.<-≤-trans _ _ _ (0<→-<0 _ (0<fromℕsuc m)) (0≤fromℕ n)
+  fromℤ-pres< (negsuc m) (negsuc n) (negsuc<negsuc p) =
+    -Flip< _ _ (fromℕ-pres<ᵗ (suc n) (suc m) p)
+
+  fromℤ-reflect< : ∀ m n → R.fromℤ m R.< R.fromℤ n → m <ℤ n
+  fromℤ-reflect< m n fm<fn with m ≟ n
+  ... | lt m<n = m<n
+  ... | eq m≡n = ⊥.rec (R.is-irrefl _ (subst (R._< _) (cong R.fromℤ m≡n) fm<fn))
+  ... | gt m>n = ⊥.rec (R.is-asym _ _ fm<fn (fromℤ-pres< n m m>n))
+
+  isOCRHomFromℤ : IsOrderedCommRingHom (snd ℤOrderedCommRing) R.fromℤ (snd R)
+  isOCRHomFromℤ .IsOrderedCommRingHom.isCommRingHom = isHomFromℤ
+  isOCRHomFromℤ .IsOrderedCommRingHom.pres≤         = fromℤ-pres≤
+  isOCRHomFromℤ .IsOrderedCommRingHom.reflect<      = fromℤ-reflect<
+
+  isOCRMonoFromℤ : IsOrderedCommRingMono (snd ℤOrderedCommRing) R.fromℤ (snd R)
+  isOCRMonoFromℤ .IsOrderedCommRingMono.isOrderedCommRingHom = isOCRHomFromℤ
+  isOCRMonoFromℤ .IsOrderedCommRingMono.pres<                = fromℤ-pres<
+
+  fromℤOCR : OrderedCommRingHom ℤOrderedCommRing R
+  fst fromℤOCR = R.fromℤ
+  snd fromℤOCR = isOCRHomFromℤ
+
+  fromℤOCRMono : OrderedCommRingMono ℤOrderedCommRing R
+  fst fromℤOCRMono = R.fromℤ
+  snd fromℤOCRMono = isOCRMonoFromℤ
+
+  isUniqueFromℤOCR : (φ : OrderedCommRingHom ℤOrderedCommRing R)
+                   → ∀ n → R.fromℤ n ≡ fst φ n
+  isUniqueFromℤOCR = isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom
+
+  isUniqueFromℤOCRMono : (φ : OrderedCommRingMono ℤOrderedCommRing R)
+                       → ∀ n → R.fromℤ n ≡ fst φ n
+  isUniqueFromℤOCRMono = isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom
+
+  isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R)
+  fst isContrHom[ℤOCR,-] = fromℤOCR
+  snd isContrHom[ℤOCR,-] = OrderedCommRingHom≡ ∘ funExt ∘ isUniqueFromℤOCR
+
+  isContrMono[ℤOCR,-] : isContr (OrderedCommRingMono ℤOrderedCommRing R)
+  fst isContrMono[ℤOCR,-] = fromℤOCRMono
+  snd isContrMono[ℤOCR,-] = OrderedCommRingMono≡ ∘ funExt ∘ isUniqueFromℤOCRMono
diff --git a/Cubical/Algebra/OrderedCommRing/Morphisms.agda b/Cubical/Algebra/OrderedCommRing/Morphisms.agda
new file mode 100644
index 0000000000..09bb5c8684
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing/Morphisms.agda
@@ -0,0 +1,372 @@
+module Cubical.Algebra.OrderedCommRing.Morphisms where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.SIP
+
+open import Cubical.Algebra.CommRing.Base
+open import Cubical.Algebra.OrderedCommRing.Base
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Reflection.RecordEquiv
+
+private
+  variable
+    ℓ ℓ' ℓ<≤ ℓ<≤' : Level
+
+record IsOrderedCommRingHom {A : Type ℓ} {B : Type ℓ'}
+  (R : OrderedCommRingStr ℓ<≤ A)
+  (f : A → B)
+  (S : OrderedCommRingStr ℓ<≤' B)
+  : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ<≤ ℓ<≤')))
+  where
+  no-eta-equality
+  private
+    module R = OrderedCommRingStr R
+    module S = OrderedCommRingStr S
+    Rcring = str (OrderedCommRing→CommRing (_ , R))
+    Scring = str (OrderedCommRing→CommRing (_ , S))
+
+  field
+    isCommRingHom : IsCommRingHom Rcring f Scring
+    pres≤         : ∀ x y → x R.≤ y → f x S.≤ f y
+    reflect<      : ∀ x y → f x S.< f y → x R.< y
+
+  open IsCommRingHom isCommRingHom public
+
+unquoteDecl IsOrderedCommRingHomIsoΣ = declareRecordIsoΣ IsOrderedCommRingHomIsoΣ (quote IsOrderedCommRingHom)
+
+OrderedCommRingHom : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _
+OrderedCommRingHom R S =
+  Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsOrderedCommRingHom (R .snd) f (S .snd)
+
+isPropIsOrderedCommRingHom : {A : Type ℓ} {B : Type ℓ'}
+                           → (R : OrderedCommRingStr ℓ<≤ A)
+                           → (f : A → B)
+                           → (S : OrderedCommRingStr ℓ<≤' B)
+                           → isProp (IsOrderedCommRingHom R f S)
+isPropIsOrderedCommRingHom R f S = isOfHLevelRetractFromIso 1
+  IsOrderedCommRingHomIsoΣ $
+  isProp×2 (isPropIsCommRingHom _ f _)
+           (isPropΠ2 λ _ _ → isProp→ (S.is-prop-valued≤ _ _))
+           (isPropΠ2 λ _ _ → isProp→ (R.is-prop-valued< _ _))
+  where
+    open module R = OrderedCommRingStr R
+    open module S = OrderedCommRingStr S
+
+isSetOrderedCommRingHom : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤')
+                        → isSet (OrderedCommRingHom R S)
+isSetOrderedCommRingHom R S = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f →
+  isPropIsOrderedCommRingHom (snd R) f (snd S))
+    where open OrderedCommRingStr (str S) using (is-set)
+
+module _
+  {R : OrderedCommRing ℓ  ℓ<≤}
+  {S : OrderedCommRing ℓ' ℓ<≤'}
+  {f : ⟨ R ⟩ → ⟨ S ⟩} where
+
+  private
+    module R = OrderedCommRingStr (str R)
+    module S = OrderedCommRingStr (str S)
+    RCR = OrderedCommRing→CommRing R
+    SCR = OrderedCommRing→CommRing S
+
+  module _
+    (p1  : f R.1r ≡ S.1r)
+    (p+  : ∀ x y → f (x R.+ y) ≡ f x S.+ f y)
+    (p·  : ∀ x y → f (x R.· y) ≡ f x S.· f y)
+    (p<⁻ : ∀ x y → f x S.< f y → x R.< y)
+    where
+
+    open IsOrderedCommRingHom
+
+    private
+      p≤ : ∀ x y → x R.≤ y → f x S.≤ f y
+      p≤ x y = invEq (S.≤≃¬> (f x) (f y)) ∘ (_∘ p<⁻ y x) ∘ equivFun (R.≤≃¬> x y)
+
+    makeIsOrderedCommRingHom : IsOrderedCommRingHom (str R) f (str S)
+    makeIsOrderedCommRingHom .isCommRingHom = makeIsCommRingHom p1 p+ p·
+    makeIsOrderedCommRingHom .pres≤         = p≤
+    makeIsOrderedCommRingHom .reflect<      = p<⁻
+
+  module _ (isHomf : IsOrderedCommRingHom (str R) f (str S)) where
+
+    isOrderedCommRingHom→IsCommRingHom : IsCommRingHom (str RCR) f (str SCR)
+    isOrderedCommRingHom→IsCommRingHom = isCommRingHom
+      where open IsOrderedCommRingHom isHomf
+
+OrderedCommRingHom→CommRingHom : {A : OrderedCommRing ℓ  ℓ<≤}
+                               → {B : OrderedCommRing ℓ' ℓ<≤'}
+                               → OrderedCommRingHom A B
+                               → CommRingHom
+                                  (OrderedCommRing→CommRing A)
+                                  (OrderedCommRing→CommRing B)
+fst (OrderedCommRingHom→CommRingHom f) = fst f
+snd (OrderedCommRingHom→CommRingHom f) = isOrderedCommRingHom→IsCommRingHom (snd f)
+
+_$ocr_ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'}
+       → (φ : OrderedCommRingHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
+φ $ocr x = φ .fst x
+
+opaque
+  OrderedCommRingHom≡ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'}
+                      → {φ ψ : OrderedCommRingHom R S}
+                      → fst φ ≡ fst ψ
+                      → φ ≡ ψ
+  OrderedCommRingHom≡ = Σ≡Prop λ f → isPropIsOrderedCommRingHom _ f _
+
+  OrderedCommRingHomPathP : (R : OrderedCommRing ℓ ℓ<≤) (S T : OrderedCommRing ℓ' ℓ<≤')
+                          → (p : S ≡ T)
+                          → (φ : OrderedCommRingHom R S)
+                          → (ψ : OrderedCommRingHom R T)
+                          → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst)
+                          → PathP (λ i → OrderedCommRingHom R (p i)) φ ψ
+  OrderedCommRingHomPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ →
+    isPropIsOrderedCommRingHom _ _ _) _ _)
+
+record IsOrderedCommRingMono {A : Type ℓ} {B : Type ℓ'}
+  (R : OrderedCommRingStr ℓ<≤ A)
+  (f : A → B)
+  (S : OrderedCommRingStr ℓ<≤' B)
+  : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ<≤ ℓ<≤')))
+  where
+  no-eta-equality
+  private
+    module R = OrderedCommRingStr R
+    module S = OrderedCommRingStr S
+
+  field
+    isOrderedCommRingHom : IsOrderedCommRingHom R f S
+    pres<                : (x y : A) → x R.< y → f x S.< f y
+
+  open IsOrderedCommRingHom isOrderedCommRingHom public
+
+unquoteDecl IsOrderedCommRingMonoIsoΣ = declareRecordIsoΣ IsOrderedCommRingMonoIsoΣ (quote IsOrderedCommRingMono)
+
+OrderedCommRingMono : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _
+OrderedCommRingMono R S =
+  Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsOrderedCommRingMono (R .snd) f (S .snd)
+
+OrderedCommRingMono→OrderedCommRingHom : {A : OrderedCommRing ℓ  ℓ<≤}
+                                       → {B : OrderedCommRing ℓ' ℓ<≤'}
+                                       → OrderedCommRingMono A B
+                                       → OrderedCommRingHom A B
+fst (OrderedCommRingMono→OrderedCommRingHom f) = fst f
+snd (OrderedCommRingMono→OrderedCommRingHom f) = isOrderedCommRingHom
+  where open IsOrderedCommRingMono (snd f)
+
+OrderedCommRingMono→CommRingHom : {A : OrderedCommRing ℓ  ℓ<≤}
+                                → {B : OrderedCommRing ℓ' ℓ<≤'}
+                                → OrderedCommRingMono A B
+                                → CommRingHom
+                                   (OrderedCommRing→CommRing A)
+                                   (OrderedCommRing→CommRing B)
+OrderedCommRingMono→CommRingHom =
+  OrderedCommRingHom→CommRingHom ∘ OrderedCommRingMono→OrderedCommRingHom
+
+isPropIsOrderedCommRingMono : {A : Type ℓ} {B : Type ℓ'}
+                            → (R : OrderedCommRingStr ℓ<≤ A)
+                            → (f : A → B)
+                            → (S : OrderedCommRingStr ℓ<≤' B)
+                            → isProp (IsOrderedCommRingMono R f S)
+isPropIsOrderedCommRingMono R f S = isOfHLevelRetractFromIso 1
+  IsOrderedCommRingMonoIsoΣ $
+  isProp× (isPropIsOrderedCommRingHom R f S)
+          (isPropΠ2 λ _ _ → isProp→ (S.is-prop-valued< _ _))
+  where
+    open module S = OrderedCommRingStr S
+
+isSetOrderedCommRingMono : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤')
+                         → isSet (OrderedCommRingMono R S)
+isSetOrderedCommRingMono R S = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f →
+  isPropIsOrderedCommRingMono (snd R) f (snd S))
+    where open OrderedCommRingStr (str S) using (is-set)
+
+module _
+  {R : OrderedCommRing ℓ  ℓ<≤}
+  {S : OrderedCommRing ℓ' ℓ<≤'}
+  {f : ⟨ R ⟩ → ⟨ S ⟩} where
+
+  private
+    module R = OrderedCommRingStr (str R)
+    module S = OrderedCommRingStr (str S)
+
+  module _
+    (p1  : f R.1r ≡ S.1r)
+    (p+  : ∀ x y → f (x R.+ y) ≡ f x S.+ f y)
+    (p·  : ∀ x y → f (x R.· y) ≡ f x S.· f y)
+    (p<  : ∀ x y → x R.< y → f x S.< f y)
+    (p<⁻ : ∀ x y → f x S.< f y → x R.< y)
+    where
+
+    open IsOrderedCommRingMono
+
+    makeIsOrderedCommRingMono : IsOrderedCommRingMono (str R) f (str S)
+    makeIsOrderedCommRingMono .isOrderedCommRingHom = makeIsOrderedCommRingHom p1 p+ p· p<⁻
+    makeIsOrderedCommRingMono .pres< = p<
+
+  module _ (isMonof : IsOrderedCommRingMono (str R) f (str S)) where
+
+    isOrderedCommRingMono→reflect≤ : ∀ x y → f x S.≤ f y → x R.≤ y
+    isOrderedCommRingMono→reflect≤ x y =
+      invEq (R.≤≃¬> x y) ∘ (_∘ pres< y x) ∘ equivFun (S.≤≃¬> (f x) (f y))
+      where open IsOrderedCommRingMono isMonof
+
+    isOrderedCommRingMono→isOrderedCommRingHom : IsOrderedCommRingHom (str R) f (str S)
+    isOrderedCommRingMono→isOrderedCommRingHom = isOrderedCommRingHom
+      where open IsOrderedCommRingMono isMonof
+
+    isOrderedCommRingMono→isInjective : ∀ x y → f x ≡ f y → x ≡ y
+    isOrderedCommRingMono→isInjective x y fx≡fy = R.is-antisym x y
+      (isOrderedCommRingMono→reflect≤ x y (subst (S._≤_ (f x)) fx≡fy (S.is-refl _)))
+      (isOrderedCommRingMono→reflect≤ y x (subst (S._≤_ (f y)) (sym fx≡fy) (S.is-refl _)))
+
+opaque
+  OrderedCommRingMono≡ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'}
+                       → {φ ψ : OrderedCommRingMono R S}
+                       → fst φ ≡ fst ψ
+                       → φ ≡ ψ
+  OrderedCommRingMono≡ = Σ≡Prop λ f → isPropIsOrderedCommRingMono _ f _
+
+  OrderedCommRingMonoPathP : (R : OrderedCommRing ℓ ℓ<≤) (S T : OrderedCommRing ℓ' ℓ<≤')
+                           → (p : S ≡ T)
+                           → (φ : OrderedCommRingMono R S)
+                           → (ψ : OrderedCommRingMono R T)
+                           → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst)
+                           → PathP (λ i → OrderedCommRingMono R (p i)) φ ψ
+  OrderedCommRingMonoPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ →
+    isPropIsOrderedCommRingMono _ _ _) _ _)
+
+record IsOrderedCommRingEquiv {A : Type ℓ} {B : Type ℓ'}
+  (R : OrderedCommRingStr ℓ<≤ A) (e : A ≃ B) (S : OrderedCommRingStr ℓ<≤' B)
+  : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ<≤) ℓ') ℓ<≤')
+  where
+  no-eta-equality
+  private
+    module R = OrderedCommRingStr R
+    module S = OrderedCommRingStr S
+    Rcring = str (OrderedCommRing→CommRing (_ , R))
+    Scring = str (OrderedCommRing→CommRing (_ , S))
+    f = equivFun e
+
+  field
+    pres0 : f R.0r ≡ S.0r
+    pres1 : f R.1r ≡ S.1r
+    pres+ : (x y : A) → f (x R.+ y) ≡ f x S.+ f y
+    pres· : (x y : A) → f (x R.· y) ≡ f x S.· f y
+    pres- : (x : A) → f (R.- x) ≡ S.- (f x)
+    pres≤ : (x y : A) → (x R.≤ y) ≃ (f x S.≤ f y)
+    pres< : (x y : A) → (x R.< y) ≃ (f x S.< f y)
+
+unquoteDecl IsOrderedCommRingEquivIsoΣ = declareRecordIsoΣ IsOrderedCommRingEquivIsoΣ (quote IsOrderedCommRingEquiv)
+
+OrderedCommRingEquiv : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _
+OrderedCommRingEquiv R S =
+  Σ[ e ∈ (R .fst ≃ S .fst) ] IsOrderedCommRingEquiv (R .snd) e (S .snd)
+
+
+OrderedCommRingEquiv→OrderedCommRingMono : {A : OrderedCommRing ℓ  ℓ<≤}
+                                         → {B : OrderedCommRing ℓ' ℓ<≤'}
+                                         → OrderedCommRingEquiv A B
+                                         → OrderedCommRingMono A B
+fst (OrderedCommRingEquiv→OrderedCommRingMono e) = equivFun (fst e)
+snd (OrderedCommRingEquiv→OrderedCommRingMono e) = isOCRMono
+  where
+    module E = IsOrderedCommRingEquiv (snd e)
+    open IsCommRingHom
+    open IsOrderedCommRingHom  renaming (isCommRingHom to isCRHom)
+    open IsOrderedCommRingMono renaming (isOrderedCommRingHom to isOCRHom)
+
+    isOCRMono : IsOrderedCommRingMono _ _ _
+    isOCRMono .isOCRHom .isCRHom .pres0 = E.pres0
+    isOCRMono .isOCRHom .isCRHom .pres1 = E.pres1
+    isOCRMono .isOCRHom .isCRHom .pres+ = E.pres+
+    isOCRMono .isOCRHom .isCRHom .pres· = E.pres·
+    isOCRMono .isOCRHom .isCRHom .pres- = E.pres-
+    isOCRMono .isOCRHom .pres≤          = (equivFun ∘_) ∘ E.pres≤
+    isOCRMono .isOCRHom .reflect<       = (invEq ∘_) ∘ E.pres<
+    isOCRMono .pres<                    = (equivFun ∘_) ∘ E.pres<
+
+OrderedCommRingEquiv→OrderedCommRingHom : {A : OrderedCommRing ℓ  ℓ<≤}
+                                        → {B : OrderedCommRing ℓ' ℓ<≤'}
+                                        → OrderedCommRingEquiv A B
+                                        → OrderedCommRingHom A B
+OrderedCommRingEquiv→OrderedCommRingHom =
+  OrderedCommRingMono→OrderedCommRingHom ∘ OrderedCommRingEquiv→OrderedCommRingMono
+
+OrderedCommRingEquiv→CommRingHom : {A : OrderedCommRing ℓ  ℓ<≤}
+                                 → {B : OrderedCommRing ℓ' ℓ<≤'}
+                                 → OrderedCommRingEquiv A B
+                                 → CommRingHom
+                                    (OrderedCommRing→CommRing A)
+                                    (OrderedCommRing→CommRing B)
+OrderedCommRingEquiv→CommRingHom =
+  OrderedCommRingHom→CommRingHom ∘ OrderedCommRingEquiv→OrderedCommRingHom
+
+isPropIsOrderedCommRingEquiv : {A : Type ℓ} {B : Type ℓ'}
+                             → (R : OrderedCommRingStr ℓ<≤ A)
+                             → (e : A ≃ B)
+                             → (S : OrderedCommRingStr ℓ<≤' B)
+                             → isProp (IsOrderedCommRingEquiv R e S)
+isPropIsOrderedCommRingEquiv R e S = isOfHLevelRetractFromIso 1
+  IsOrderedCommRingEquivIsoΣ $
+  isProp× (S.is-set _ _) $
+  isProp× (S.is-set _ _) $
+  isProp× (isPropΠ2 λ _ _ → S.is-set _ _) $
+  isProp× (isPropΠ2 λ _ _ → S.is-set _ _) $
+  isProp× (isPropΠ  λ _   → S.is-set _ _) $
+  isProp× (isPropΠ2 λ _ _ → isOfHLevel≃ 1 (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _))
+          (isPropΠ2 λ _ _ → isOfHLevel≃ 1 (R.is-prop-valued< _ _) (S.is-prop-valued< _ _))
+  where
+    open module R = OrderedCommRingStr R
+    open module S = OrderedCommRingStr S
+
+isSetOrderedCommRingEquiv : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤')
+                          → isSet (OrderedCommRingEquiv R S)
+isSetOrderedCommRingEquiv R S = isSetΣSndProp (isOfHLevel≃ 2 R.is-set S.is-set) (λ e →
+  isPropIsOrderedCommRingEquiv (snd R) e (snd S))
+    where
+      open module R = OrderedCommRingStr (str R)
+      open module S = OrderedCommRingStr (str S)
+
+-- an easier way of establishing an equivalence of ordered commutative rings
+module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} (e : ⟨ R ⟩ ≃ ⟨ S ⟩)
+  where
+  private
+    module R = OrderedCommRingStr (str R)
+    module S = OrderedCommRingStr (str S)
+
+  module _ (isMono : IsOrderedCommRingMono (str R) (equivFun e) (str S)) where
+
+    private
+      module M = IsOrderedCommRingMono isMono
+
+    open IsOrderedCommRingEquiv
+
+    makeIsOrderedCommRingEquivFromIsMono : IsOrderedCommRingEquiv (str R) e (str S)
+    makeIsOrderedCommRingEquivFromIsMono .pres0 = M.pres0
+    makeIsOrderedCommRingEquivFromIsMono .pres1 = M.pres1
+    makeIsOrderedCommRingEquivFromIsMono .pres+ = M.pres+
+    makeIsOrderedCommRingEquivFromIsMono .pres· = M.pres·
+    makeIsOrderedCommRingEquivFromIsMono .pres- = M.pres-
+    makeIsOrderedCommRingEquivFromIsMono .pres≤ = λ x y → propBiimpl→Equiv
+      (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _)
+      (M.pres≤ x y) (isOrderedCommRingMono→reflect≤ isMono x y)
+    makeIsOrderedCommRingEquivFromIsMono .pres< = λ x y → propBiimpl→Equiv
+      (R.is-prop-valued< _ _) (S.is-prop-valued< _ _)
+      (M.pres< x y) (M.reflect< x y)
+
+  module _
+    (p1  : equivFun e R.1r ≡ S.1r)
+    (p+  : ∀ x y → equivFun e (x R.+ y) ≡ equivFun e x S.+ equivFun e y)
+    (p·  : ∀ x y → equivFun e (x R.· y) ≡ equivFun e x S.· equivFun e y)
+    (p<  : ∀ x y → x R.< y → equivFun e x S.< equivFun e y)
+    (p<⁻ : ∀ x y → equivFun e x S.< equivFun e y → x R.< y)
+    where
+
+    makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S)
+    makeIsOrderedCommRingEquiv = makeIsOrderedCommRingEquivFromIsMono
+      (makeIsOrderedCommRingMono p1 p+ p· p< p<⁻)
diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda
new file mode 100644
index 0000000000..eb1ea38212
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing/Properties.agda
@@ -0,0 +1,685 @@
+module Cubical.Algebra.OrderedCommRing.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommSemiring
+open import Cubical.Algebra.OrderedCommRing.Base
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Semigroup
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Relation.Binary.Order.Apartness
+open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice)
+open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.Quoset
+open import Cubical.Relation.Binary.Order.QuosetReasoning
+open import Cubical.Relation.Binary.Order.StrictOrder
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Tactics.CommRingSolver
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+OrderedCommRing→StrictOrder : OrderedCommRing ℓ ℓ' → StrictOrder ℓ ℓ'
+OrderedCommRing→StrictOrder R .fst = R .fst
+OrderedCommRing→StrictOrder R .snd = strictorderstr _ isStrictOrder where
+  open OrderedCommRingStr (str R)
+
+OrderedCommRing→Ring : OrderedCommRing ℓ ℓ' → Ring ℓ
+OrderedCommRing→Ring = CommRing→Ring ∘ OrderedCommRing→CommRing
+
+OrderedCommRing→Poset : OrderedCommRing ℓ ℓ' → Poset ℓ ℓ'
+OrderedCommRing→Poset = Pseudolattice→Poset ∘ OrderedCommRing→PseudoLattice
+
+OrderedCommRing→Quoset : OrderedCommRing ℓ ℓ' → Quoset ℓ ℓ'
+OrderedCommRing→Quoset = StrictOrder→Quoset ∘ OrderedCommRing→StrictOrder
+
+OrderedCommRing→Apartness : OrderedCommRing ℓ ℓ' → Apartness ℓ ℓ'
+OrderedCommRing→Apartness = StrictOrder→Apartness ∘ OrderedCommRing→StrictOrder
+
+module _ (R' : OrderedCommRing ℓ ℓ') where
+  private
+    R = fst R'
+    RCR = OrderedCommRing→CommRing R'
+  open RingTheory (OrderedCommRing→Ring R')
+  open OrderedCommRingStr (snd R')
+
+  module OrderedCommRingReasoning where
+    open <-≤-Reasoning
+      (fst R')
+      (str (OrderedCommRing→Poset  R'))
+      (str (OrderedCommRing→Quoset R'))
+      (λ x {y} {z} → <-≤-trans x y z)
+      (λ x {y} {z} → ≤-<-trans x y z)
+      (λ   {x} {y} → <-≤-weaken x y)
+      public
+
+    open <-syntax public
+    open ≤-syntax public
+    open ≡-syntax public
+
+    _<+[_] : ∀ {x y} → x < y → ∀ z → x + z < y + z
+    _<+[_] x<y z = +MonoR< _ _ z x<y
+
+    [_]+<_ : ∀ {x y} z → x < y → z + x < z + y
+    [_]+<_ z = subst2 _<_ (+Comm _ z) (+Comm _ z) ∘ +MonoR< _ _ z
+
+    _≤+[_] : ∀ {x y} → x ≤ y → ∀ z → x + z ≤ y + z
+    _≤+[_] x≤y z = +MonoR≤ _ _ z x≤y
+
+    [_]+≤_ : ∀ {x y} z → x ≤ y → z + x ≤ z + y
+    [_]+≤_ z = subst2 _≤_ (+Comm _ z) (+Comm _ z) ∘ +MonoR≤ _ _ z
+
+    _<·[_,_] : ∀ {x y} → x < y → ∀ z → 0r < z → x · z < y · z
+    _<·[_,_] x<y z 0<z = ·MonoR< _ _ z 0<z x<y
+
+    [_,_]·<_ : ∀ {x y} z → 0r < z → x < y → z · x < z · y
+    [_,_]·<_ z = (subst2 _<_ (·Comm _ z) (·Comm _ z) ∘_) ∘ ·MonoR< _ _ z
+
+    _≤·[_,_] : ∀ {x y} → x ≤ y → ∀ z → 0r ≤ z → x · z ≤ y · z
+    _≤·[_,_] x≤y z 0≤z = ·MonoR≤ _ _ z 0≤z x≤y
+
+    [_,_]·≤_ : ∀ {x y} z → 0r ≤ z → x ≤ y → z · x ≤ z · y
+    [_,_]·≤_ z = (subst2 _≤_ (·Comm _ z) (·Comm _ z) ∘_) ∘ ·MonoR≤ _ _ z
+
+    private
+      example : ∀ a b c d e f g
+              → (0r < f) → a < (b + c) → b ≤ d → (d + c) < (e · f) → e < g
+              → a < (g · f)
+      example a b c d e f g 0<f a<b+c b≤d d+c<e·f e<g = begin<
+        a     <⟨ a<b+c ⟩
+        b + c ≤⟨ b≤d ≤+[ c ] ⟩
+        d + c <⟨ d+c<e·f ⟩
+        e · f <⟨ e<g <·[ f , 0<f ] ⟩
+        g · f ◾
+
+  open OrderedCommRingReasoning
+
+  module OrderedCommRingTheory where
+    open ApartnessStr (str (OrderedCommRing→Apartness R')) using (_#_) public
+    open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public using () renaming (
+        L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨Comm to ⊔Comm ; ∨Idem to ⊔Idem ; ∨LUB to ⊔LUB
+      ; ∧≤L to ⊓≤L ; ∧≤R to ⊓≤R ; ∧Comm to ⊓Comm ; ∧Idem to ⊓Idem ; ∧GLB to ⊓GLB)
+
+    0≤1 : 0r ≤ 1r
+    0≤1 = <-≤-weaken 0r 1r 0<1
+
+    ≤→¬> : ∀ x y → x ≤ y → ¬ (y < x)
+    ≤→¬> x y = equivFun (≤≃¬> x y)
+
+    ¬<→≥ : ∀ x y → ¬ (x < y) → y ≤ x
+    ¬<→≥ x y = invEq (≤≃¬> y x)
+
+    +MonoL< : ∀ x y z → x < y → z + x < z + y
+    +MonoL< x y z = subst2 _<_ (+Comm _ _) (+Comm _ _) ∘ +MonoR< x y z
+
+    +Mono< : ∀ x y z w → x < y → z < w → x + z < y + w
+    +Mono< x y z w x<y z<w = is-trans< _ _ _ (+MonoR< _ _ _ x<y) (+MonoL< _ _ _ z<w)
+
+    +MonoL≤ : ∀ x y z → x ≤ y → z + x ≤ z + y
+    +MonoL≤ x y z = subst2 _≤_ (+Comm _ _) (+Comm _ _) ∘ +MonoR≤ x y z
+
+    +Mono≤ : ∀ x y z w → x ≤ y → z ≤ w → x + z ≤ y + w
+    +Mono≤ x y z w x≤y z≤w = is-trans≤ _ _ _ (+MonoR≤ _ _ _ x≤y) (+MonoL≤ _ _ _ z≤w)
+
+    ·MonoL< : ∀ x y z → 0r < z → x < y → z · x < z · y
+    ·MonoL< x y z = (subst2 _<_ (·Comm _ _) (·Comm _ _) ∘_) ∘ ·MonoR< _ _ _
+
+    ·MonoL≤ : ∀ x y z → 0r ≤ z → x ≤ y → z · x ≤ z · y
+    ·MonoL≤ x y z = (subst2 _≤_ (·Comm _ _) (·Comm _ _) ∘_) ∘ ·MonoR≤ _ _ _
+
+    ·CancelL≤ : ∀ x y z → 0r < z → z · x ≤ z · y → x ≤ y
+    ·CancelL≤ x y z 0<z zx≤zy = ¬<→≥ y x $ ≤→¬> _ _ zx≤zy ∘ ·MonoL< _ _ z 0<z
+
+    ·CancelR≤ : ∀ x y z → 0r < z → x · z ≤ y · z → x ≤ y
+    ·CancelR≤ x y z 0<z zx≤zy = ¬<→≥ y x $ ≤→¬> _ _ zx≤zy ∘ ·MonoR< _ _ z 0<z
+
+    -- It is not clear if the properties commented below are constructively derivable.
+    --
+    -- ·CancelL< : ∀ x y z → 0r < z → z · x < z · y → x < y
+    -- ·CancelL< = ?
+    --
+    -- ·CancelR< : ∀ x y z → 0r < z → x · z < y · z → x < y
+    -- ·CancelR< = ?
+
+    -- Howeverer, we can prove their double negations, so they are classically valid
+    ¬¬·CancelL< : ∀ x y z → 0r < z → z · x < z · y → ¬ ¬ (x < y)
+    ¬¬·CancelL< x y z 0<z zx<zy ¬x<y =
+      ≤→¬> _ _ (·MonoL≤ _ _ z (<-≤-weaken 0r z 0<z) (¬<→≥ _ _ ¬x<y)) zx<zy
+
+    ¬¬·CancelR< : ∀ x y z → 0r < z → x · z < y · z → ¬ ¬ (x < y)
+    ¬¬·CancelR< x y z 0<z xz<yz ¬x<y =
+      ≤→¬> _ _ (·MonoR≤ _ _ z (<-≤-weaken 0r z 0<z) (¬<→≥ _ _ ¬x<y)) xz<yz
+
+    ≥Using< : ∀ x y → (x < y → y ≤ x) → y ≤ x
+    ≥Using< x y <→≥ = ¬<→≥ x y (∘diag (≤→¬> y x ∘ <→≥))
+
+    abs ∣_∣ : R → R
+    abs z = z ⊔ (- z)
+    ∣_∣ = abs
+
+    <SumLeftPos : ∀ x y → 0r < y → x < x + y
+    <SumLeftPos x y = subst (_< x + y) (+IdR x) ∘ +MonoL< 0r y x
+
+    <SumRightPos : ∀ x y → 0r < y → x < y + x
+    <SumRightPos x y = subst (_< y + x) (+IdL x) ∘ +MonoR< 0r y x
+
+    ≤SumLeftNonNeg : ∀ x y → 0r ≤ y → x ≤ x + y
+    ≤SumLeftNonNeg x y = subst (_≤ x + y) (+IdR x) ∘ +MonoL≤ 0r y x
+
+    ≤SumRightNonNeg : ∀ x y → 0r ≤ y → x ≤ y + x
+    ≤SumRightNonNeg x y = subst (_≤ y + x) (+IdL x) ∘ +MonoR≤ 0r y x
+
+    -Flip< : ∀ x y → x < y → - y < - x
+    -Flip< x y x<y = begin<
+      - y           ≡→≤⟨ solve! RCR ⟩
+      x + (- x - y)   <⟨ x<y <+[ - x - y ] ⟩
+      y + (- x - y) ≡→≤⟨ solve! RCR ⟩
+      - x             ◾
+
+    -Flip≤ : ∀ x y → x ≤ y → - y ≤ - x
+    -Flip≤ x y x≤y = begin≤
+      - y           ≡→≤⟨ solve! RCR ⟩
+      x + (- x - y)   ≤⟨ x≤y ≤+[ - x - y ] ⟩
+      y + (- x - y) ≡→≤⟨ solve! RCR ⟩
+      - x             ◾
+
+    0<→-<0 : ∀ x → 0r < x → - x < 0r
+    0<→-<0 x = subst (- x <_) 0Selfinverse ∘ -Flip< 0r x
+
+    <0→0<- : ∀ x → x < 0r → 0r < - x
+    <0→0<- x = subst (_< - x) 0Selfinverse ∘ -Flip< x 0r
+
+    0≤→-≤0 : ∀ x → 0r ≤ x → - x ≤ 0r
+    0≤→-≤0 x = subst (- x ≤_) 0Selfinverse ∘ -Flip≤ 0r x
+
+    ≤0→0≤- : ∀ x → x ≤ 0r → 0r ≤ - x
+    ≤0→0≤- x = subst (_≤ - x) 0Selfinverse ∘ -Flip≤ x 0r
+
+    <→0<Δ : ∀ x y → x < y → 0r < y - x
+    <→0<Δ x y = subst (_< (y - x)) (+InvR x) ∘ +MonoR< x y (- x)
+
+    ≤→0≤Δ : ∀ x y → x ≤ y → 0r ≤ y - x
+    ≤→0≤Δ x y = subst (_≤ (y - x)) (+InvR x) ∘ +MonoR≤ x y (- x)
+
+    0<Δ→< : ∀ x y → 0r < y - x → x < y
+    0<Δ→< x y = subst2 _<_ (+IdL x) (solve! RCR) ∘ +MonoR< 0r (y - x) x
+
+    0≤Δ→≤ : ∀ x y → 0r ≤ y - x → x ≤ y
+    0≤Δ→≤ x y = subst2 _≤_ (+IdL x) (solve! RCR) ∘ +MonoR≤ 0r (y - x) x
+
+    0≤² : ∀ x → 0r ≤ x · x
+    0≤² x = ≥Using< (x · x) 0r λ x²<0 →
+      let
+        0≤x : 0r ≤ x
+        0≤x = ¬<→≥ x 0r λ x<0 → is-irrefl 0r $ begin<
+          0r             ≡→≤⟨ sym $ 0LeftAnnihilates (- x) ⟩
+          0r · (- x)       <⟨ ∘diag (·MonoR< _ _ _) (<0→0<- x x<0) ⟩
+          (- x) · (- x)  ≡→≤⟨ solve! RCR ⟩
+          x · x            <⟨ x²<0 ⟩
+          0r               ◾
+      in
+        subst (_≤ x · x) (0LeftAnnihilates x) (∘diag (·MonoR≤ _ _ _) 0≤x)
+
+    #→0<² : ∀ x → x # 0r → 0r < x · x
+    #→0<² x (inl x<0) =
+      subst2 _<_ (0LeftAnnihilates _) (solve! RCR) (∘diag (·MonoR< _ _ _) (<0→0<- x x<0))
+    #→0<² x (inr 0<x) =
+      subst (_< x · x) (0LeftAnnihilates _) (∘diag (·MonoR< _ _ _) 0<x)
+
+    ≤abs : ∀ z → z ≤ abs z
+    ≤abs z = L≤⊔
+
+    -≤abs : ∀ z → - z ≤ abs z
+    -≤abs z = R≤⊔
+
+    0≤abs : ∀ z → 0r ≤ abs z
+    0≤abs z = ¬<→≥ (abs z) 0r λ ∣z∣<0 → is-irrefl 0r $ begin<
+      0r      ≡→≤⟨ sym 0Selfinverse ⟩
+      - 0r      <⟨ -Flip< _ _ ∣z∣<0 ⟩
+      - abs z   ≤⟨ -Flip≤ _ _ (≤abs z) ⟩
+      - z       ≤⟨ -≤abs z ⟩
+      abs z     <⟨ ∣z∣<0 ⟩
+      0r        ◾
+
+    abs≤0→≡0 : ∀ z → abs z ≤ 0r → z ≡ 0r
+    abs≤0→≡0 z ∣z∣≤0 = is-antisym z 0r
+      (begin≤
+        z     ≤⟨ ≤abs z ⟩
+        abs z ≤⟨ ∣z∣≤0 ⟩
+        0r         ◾)
+      (begin≤
+        0r        ≡→≤⟨ sym 0Selfinverse ⟩
+        - 0r        ≤⟨ -Flip≤ _ _ ∣z∣≤0 ⟩
+        - (abs z)   ≤⟨ -Flip≤ _ _ $ -≤abs z ⟩
+        - - z     ≡→≤⟨ -Idempotent z ⟩
+        z           ◾)
+
+    #→0<abs : ∀ z → z # 0r → 0r < abs z
+    #→0<abs z (inl z<0) = begin<
+      0r    ≡→≤⟨ sym 0Selfinverse ⟩
+      - 0r    <⟨ -Flip< z 0r z<0 ⟩
+      - z     ≤⟨ -≤abs _ ⟩
+      abs z   ◾
+    #→0<abs z (inr 0<z) = begin<
+      0r    <⟨ 0<z ⟩
+      z     ≤⟨ ≤abs _ ⟩
+      abs z ◾
+
+    abs- : ∀ x → abs (- x) ≡ abs x
+    abs- x = cong ((- x) ⊔_) (-Idempotent x) ∙ ⊔Comm
+
+    0≤→abs≡id : ∀ x → 0r ≤ x → abs x ≡ x
+    0≤→abs≡id x 0≤x = is-antisym (abs x) x
+      (⊔LUB (is-refl x) (begin≤ - x ≤⟨ 0≤→-≤0 x 0≤x ⟩ 0r ≤⟨ 0≤x ⟩ x ◾))
+      (≤abs x)
+
+    ≤0→abs≡- : ∀ x → x ≤ 0r → abs x ≡ - x
+    ≤0→abs≡- x x≤0 = sym (abs- x) ∙ 0≤→abs≡id (- x) (≤0→0≤- x x≤0)
+
+    0<→abs≡id : ∀ x → 0r < x → abs x ≡ x
+    0<→abs≡id x = 0≤→abs≡id x ∘ <-≤-weaken 0r x
+
+    <0→abs≡- : ∀ x → x < 0r → abs x ≡ - x
+    <0→abs≡- x = ≤0→abs≡- x ∘ <-≤-weaken x 0r
+
+    ²∘abs≡² : ∀ x → abs x · abs x ≡ x · x
+    ²∘abs≡² x = is-antisym (abs x · abs x) (x · x)
+      (¬<→≥ (x · x) (abs x · abs x) λ x²<∣x∣² →
+        let
+          0≤x : 0r ≤ x
+          0≤x = ¬<→≥ x 0r λ x<0 → is-irrefl (x · x) (begin<
+            x · x           <⟨ x²<∣x∣² ⟩
+            abs x · abs x ≡→≤⟨ cong (∘diag _·_) (<0→abs≡- x x<0) ∙ solve! RCR ⟩
+            x · x           ◾)
+        in
+          is-irrefl (x · x) (begin<
+            x · x           <⟨ x²<∣x∣² ⟩
+            abs x · abs x ≡→≤⟨ cong (∘diag _·_) (0≤→abs≡id x 0≤x) ⟩
+            x · x           ◾))
+      (0≤Δ→≤ (x · x) (abs x · abs x) (begin≤
+        0r                          ≡→≤⟨ sym $ 0LeftAnnihilates (abs x - - x) ⟩
+        0r · (abs x - - x)            ≤⟨ ≤→0≤Δ _ _ (≤abs x) ≤·[ _ , ≤→0≤Δ _ _ (-≤abs x) ] ⟩
+        (abs x - x) · (abs x - - x) ≡→≤⟨ solve! RCR ⟩
+        abs x · abs x - x · x         ◾))
+
+    abs∘²≡² : ∀ x → abs(x · x) ≡ x · x
+    abs∘²≡² x = 0≤→abs≡id (x · x) (0≤² x)
+
+    triangularInequality ▵≤ : ∀ x y → abs (x + y) ≤ abs x + abs y
+    triangularInequality x y = ⊔LUB
+      (begin≤
+        x     + y     ≤⟨ +Mono≤ _ _ _ _ (≤abs x) (≤abs y) ⟩
+        abs x + abs y ◾)
+      (begin≤
+        - (x + y)    ≡→≤⟨ solve! RCR ⟩
+        (- x) - y      ≤⟨ +Mono≤ _ _ _ _ (-≤abs x) (-≤abs y) ⟩
+        abs x + abs y ◾)
+
+    ▵≤ = triangularInequality
+
+    triangularInequality- ▵≤- : ∀ x y z → abs (x - y) ≤ abs (x - z) + abs (z - y)
+    triangularInequality- x y z = begin≤
+      abs (x - y)               ≡→≤⟨ cong abs (solve! RCR) ⟩
+      abs ((x - z) + (z - y))     ≤⟨ triangularInequality (x - z) (z - y) ⟩
+      abs (x - z) + abs (z - y)   ◾
+
+    ▵≤- = triangularInequality-
+
+    abs-Comm : ∀ x y → abs (x - y) ≡ abs (y - x)
+    abs-Comm x y =
+      abs (x - y)             ≡⟨⟩
+      (x - y) ⊔ (- (x - y))   ≡⟨ ⊔Comm ⟩
+      (- (x - y)) ⊔ (x - y)   ≡⟨ cong₂ _⊔_ (solve! RCR) (solve! RCR) ⟩
+      (y - x) ⊔ (- (y - x))   ≡⟨⟩
+      abs (y - x)             ∎
+
+    abs0 : abs 0r ≡ 0r
+    abs0 = 0≤→abs≡id 0r (is-refl 0r)
+
+    abs1 : abs 1r ≡ 1r
+    abs1 = 0≤→abs≡id 1r 0≤1
+
+  open OrderedCommRingTheory
+
+  module AdditiveSubType
+    (P : R → Type ℓ'')
+    (P-prop : ∀ x → isProp (P x))
+    (+Closed : (x y : R) → P x → P y → P (x + y))
+    where
+
+    subtype : Type (ℓ-max ℓ ℓ'')
+    subtype = Σ[ x ∈ R ] P x
+
+    isSetSubtype : isSet subtype
+    isSetSubtype = isSetΣSndProp is-set P-prop
+
+    ι : subtype → R
+    ι = fst
+
+    subtype≡ : ∀ {x y} → ι x ≡ ι y → x ≡ y
+    subtype≡ = Σ≡Prop P-prop
+
+    _+subtype_ : subtype → subtype → subtype
+    (x +subtype y) .fst = fst x + fst y
+    (x +subtype y) .snd = +Closed (fst x) (fst y) (snd x) (snd y)
+
+    _-subtype_ : subtype → subtype → R
+    _-subtype_ x y = ι x - ι y
+
+    _<subtype_ : subtype → subtype → Type ℓ'
+    _<subtype_ x y = ι x < ι y
+
+    _≤subtype_ : subtype → subtype → Type ℓ'
+    _≤subtype_ x y = ι x ≤ ι y
+
+    infixl 6 _+subtype_ _-subtype_
+    infix  4 _<subtype_ _≤subtype_
+
+  module AdditiveAndMultiplicativeSubType
+    (P : R → Type ℓ'')
+    (P-prop : ∀ x → isProp (P x))
+    (+Closed : (x y : R) → P x → P y → P (x + y))
+    (·Closed : (x y : R) → P x → P y → P (x · y))
+    where
+    open AdditiveSubType P P-prop +Closed public
+
+    _·subtype_ : subtype → subtype → subtype
+    (x ·subtype y) .fst = fst x · fst y
+    (x ·subtype y) .snd = ·Closed (fst x) (fst y) (snd x) (snd y)
+
+    infixl 7 _·subtype_
+
+  -- 0<+Closed and 0<·Closed are derivable, but for concrete instances
+  -- (like the rationals) it's more efficient to use alternative proofs
+  module Positive
+    (0<+Closed : (x y : R) → 0r < x → 0r < y → 0r < x + y)
+    (0<·Closed : (x y : R) → 0r < x → 0r < y → 0r < x · y)
+    where
+    open AdditiveAndMultiplicativeSubType
+      (0r <_) (is-prop-valued< 0r) 0<+Closed 0<·Closed public renaming (
+        subtype to R₊ ; isSetSubtype to isSetR₊ ; ι to ⟨_⟩₊ ; subtype≡ to R₊≡
+      ; _+subtype_ to _+₊_ ; _·subtype_ to _·₊_ ; _-subtype_ to _-₊_
+      ; _≤subtype_ to _≤₊_ ; _<subtype_ to _<₊_)
+
+    R₊AdditiveSemigroup : Semigroup _
+    fst R₊AdditiveSemigroup = R₊
+    SemigroupStr._·_ (snd R₊AdditiveSemigroup) = _+₊_
+    SemigroupStr.isSemigroup (snd R₊AdditiveSemigroup) = isSG
+      where
+        isSG : IsSemigroup _
+        isSG .IsSemigroup.is-set = isSetR₊
+        isSG .IsSemigroup.·Assoc = λ _ _ _ → R₊≡ (+Assoc _ _ _)
+
+    open SemigroupStr (snd R₊AdditiveSemigroup) using () public renaming (
+      ·Assoc to +₊Assoc)
+
+    R₊MultiplicativeCommMonoid : CommMonoid _
+    fst R₊MultiplicativeCommMonoid = R₊
+    CommMonoidStr.ε   (snd R₊MultiplicativeCommMonoid) = 1r , 0<1
+    CommMonoidStr._·_ (snd R₊MultiplicativeCommMonoid) = _·₊_
+    CommMonoidStr.isCommMonoid (snd R₊MultiplicativeCommMonoid) =
+      makeIsCommMonoid
+        isSetR₊
+        (λ _ _ _ → R₊≡ (·Assoc _ _ _))
+        (λ _     → R₊≡ (·IdR _))
+        (λ _ _   → R₊≡ (·Comm _ _))
+
+    open CommMonoidStr (snd R₊MultiplicativeCommMonoid) using () public renaming (
+      ε to 1₊ ; ·Assoc to ·₊Assoc ; ·IdR to ·₊IdR ; ·Comm to ·₊Comm)
+
+    selfSeparated : ∀ (x y : R) → (∀ (z : R₊) → abs(x - y) < ⟨ z ⟩₊) → x ≡ y
+    selfSeparated x y ∀[•]∣x-y∣<• =
+      let
+        ∣x-y∣≤0 : abs(x - y) ≤ 0r
+        ∣x-y∣≤0 = ¬<→≥ 0r (abs(x - y)) λ 0<∣x-y∣ → is-irrefl (abs(x - y)) $ begin<
+          abs(x - y) <⟨ ∀[•]∣x-y∣<• (abs(x - y) , 0<∣x-y∣) ⟩
+          abs(x - y) ◾
+
+        x-y≡0 : x - y ≡ 0r
+        x-y≡0 = abs≤0→≡0 (x - y) ∣x-y∣≤0
+      in
+        equalByDifference x y x-y≡0
+
+    _⊔₊_ : R₊ → R₊ → R₊
+    (x ⊔₊ y) .fst = ⟨ x ⟩₊ ⊔ ⟨ y ⟩₊
+    (x ⊔₊ y) .snd = begin< 0r <⟨ snd x ⟩ ⟨ x ⟩₊ ≤⟨ L≤⊔ ⟩ ⟨ x ⟩₊ ⊔ ⟨ y ⟩₊ ◾
+
+    plusMinus₊ : ∀ x y → (x +₊ y) -₊ y ≡ ⟨ x ⟩₊
+    plusMinus₊ (x , _) (y , _) = solve! RCR
+
+    minusPlus₊ : ∀ x y → x -₊ y + ⟨ y ⟩₊ ≡ ⟨ x ⟩₊
+    minusPlus₊ (x , _) (y , _) = solve! RCR
+
+    ≡₊→0< : ∀ {x} y → x ≡ ⟨ y ⟩₊ → 0r < x
+    ≡₊→0< y p = subst (0r <_) (sym p) (snd y)
+
+    ≡₊→R₊ : ∀ {x} y → x ≡ ⟨ y ⟩₊ → R₊
+    ≡₊→R₊ y p .fst = _
+    ≡₊→R₊ y p .snd = ≡₊→0< y p
+
+    infixl 6 -₊<
+    -₊< : ∀ x y → y <₊ x → R₊
+    -₊< x y y<x .fst = x -₊ y
+    -₊< x y y<x .snd = <→0<Δ ⟨ y ⟩₊ ⟨ x ⟩₊ y<x
+
+    syntax -₊< x y y<x = x -₊[ y<x ] y
+
+    [_-₊_]⟨_⟩ : ∀ x y → y <₊ x → R₊
+    [_-₊_]⟨_⟩ = -₊<
+
+    <₊SumLeft : ∀ x y → x <₊ x +₊ y
+    <₊SumLeft (x , _) (y , 0<y) = begin<
+      x ≡→≤⟨ sym $ +IdR x ⟩ x + 0r <⟨ [ x ]+< 0<y ⟩ x + y ◾
+
+    <₊SumRight : ∀ x y → x <₊ y +₊ x
+    <₊SumRight (x , _) (y , 0<y) = begin<
+      x ≡→≤⟨ sym $ +IdL x ⟩ 0r + x <⟨ 0<y <+[ x ] ⟩ y + x ◾
+
+    Δ<₊ : ∀ x y → x -₊ y < ⟨ x ⟩₊
+    Δ<₊ (x , _) (y , 0<y) = begin<
+      x - y <⟨ [ x ]+< -Flip< 0r y 0<y ⟩ x - 0r ≡→≤⟨ solve! RCR ⟩ x ◾
+
+  -- 0≤+Closed and 0≤·Closed are derivable, but for concrete instances
+  -- (like the rationals) it's more efficient to use alternative proofs
+  module NonNegative
+    (0≤+Closed : (x y : R) → 0r ≤ x → 0r ≤ y → 0r ≤ x + y)
+    (0≤·Closed : (x y : R) → 0r ≤ x → 0r ≤ y → 0r ≤ x · y)
+    where
+    open AdditiveAndMultiplicativeSubType
+      (0r ≤_) (is-prop-valued≤ 0r) 0≤+Closed 0≤·Closed public renaming (
+        subtype to R₀₊ ; isSetSubtype to isSetR₀₊ ; ι to ⟨_⟩₀₊ ; subtype≡ to R₀₊≡
+      ; _+subtype_ to _+₀₊_ ; _·subtype_ to _·₀₊_ ; _-subtype_ to _-₀₊_
+      ; _≤subtype_ to _≤₀₊_ ; _<subtype_ to _<₀₊_)
+
+    R₀₊CommSemiring : CommSemiring _
+    fst R₀₊CommSemiring = R₀₊
+    CommSemiringStr.0r  (snd R₀₊CommSemiring) = 0r , is-refl _
+    CommSemiringStr.1r  (snd R₀₊CommSemiring) = 1r , 0≤1
+    CommSemiringStr._+_ (snd R₀₊CommSemiring) = _+₀₊_
+    CommSemiringStr._·_ (snd R₀₊CommSemiring) = _·₀₊_
+    CommSemiringStr.isCommSemiring (snd R₀₊CommSemiring) =
+      makeIsCommSemiring
+        isSetR₀₊
+        (λ _ _ _ → R₀₊≡ (+Assoc _ _ _))
+        (λ _     → R₀₊≡ (+IdR _))
+        (λ _ _   → R₀₊≡ (+Comm _ _))
+        (λ _ _ _ → R₀₊≡ (·Assoc _ _ _))
+        (λ _     → R₀₊≡ (·IdR _))
+        (λ _ _ _ → R₀₊≡ (·DistR+ _ _ _))
+        (λ _     → R₀₊≡ (0LeftAnnihilates _))
+        (λ _ _   → R₀₊≡ (·Comm _ _))
+
+    open CommSemiringStr (snd R₀₊CommSemiring) using () public renaming (
+        0r to 0₀₊ ; 1r to 1₀₊
+      ; +Assoc to +₀₊Assoc ; +IdL to +₀₊IdL ; +IdR to +₀₊IdR ; +Comm to +₀₊Comm
+      ; ·Assoc to ·₀₊Assoc ; ·IdL to ·₀₊IdL ; ·IdR to ·₀₊IdR ; ·Comm to ·₀₊Comm
+      ; ·DistL+ to ·₀₊DistL+₀₊ ; ·DistR+ to ·₀₊DistR+₀₊
+      ; AnnihilL to AnnihilL₀₊ ; AnnihilR to AnnihilR₀₊)
+
+    _⊔₀₊_ : R₀₊ → R₀₊ → R₀₊
+    (x ⊔₀₊ y) .fst = ⟨ x ⟩₀₊ ⊔ ⟨ y ⟩₀₊
+    (x ⊔₀₊ y) .snd = begin≤ 0r ≤⟨ snd x ⟩ ⟨ x ⟩₀₊ ≤⟨ L≤⊔ ⟩ ⟨ x ⟩₀₊ ⊔ ⟨ y ⟩₀₊ ◾
+
+    _⊓₀₊_ : R₀₊ → R₀₊ → R₀₊
+    (x ⊓₀₊ y) .fst = ⟨ x ⟩₀₊ ⊓ ⟨ y ⟩₀₊
+    (x ⊓₀₊ y) .snd = ⊓GLB (snd x) (snd y)
+
+    plusMinus₀₊ : ∀ x y → (x +₀₊ y) -₀₊ y ≡ ⟨ x ⟩₀₊
+    plusMinus₀₊ (x , _) (y , _) = solve! RCR
+
+    minusPlus₀₊ : ∀ x y → x -₀₊ y + ⟨ y ⟩₀₊ ≡ ⟨ x ⟩₀₊
+    minusPlus₀₊ (x , _) (y , _) = solve! RCR
+
+    ≡₀₊→0≤ : ∀ {x} y → x ≡ ⟨ y ⟩₀₊ → 0r ≤ x
+    ≡₀₊→0≤ y p = subst (0r ≤_) (sym p) (snd y)
+
+    ≡₀₊→R₀₊ : ∀ {x} y → x ≡ ⟨ y ⟩₀₊ → R₀₊
+    ≡₀₊→R₀₊ y p .fst = _
+    ≡₀₊→R₀₊ y p .snd = ≡₀₊→0≤ y p
+
+    infixl 6 -₀₊≤
+    -₀₊≤ : ∀ x y → y ≤₀₊ x → R₀₊
+    -₀₊≤ x y y≤x .fst = x -₀₊ y
+    -₀₊≤ x y y≤x .snd = ≤→0≤Δ ⟨ y ⟩₀₊ ⟨ x ⟩₀₊ y≤x
+
+    syntax -₀₊≤ x y y≤x = x -₀₊[ y≤x ] y
+
+    [_-₀₊_]⟨_⟩ : ∀ x y → y ≤₀₊ x → R₀₊
+    [_-₀₊_]⟨_⟩ = -₀₊≤
+
+    ≤₀₊SumLeft : ∀ x y → x ≤₀₊ x +₀₊ y
+    ≤₀₊SumLeft (x , _) (y , 0≤y) = begin≤
+      x ≡→≤⟨ sym $ +IdR x ⟩ x + 0r ≤⟨ [ x ]+≤ 0≤y ⟩ x + y ◾
+
+    ≤₀₊SumRight : ∀ x y → x ≤₀₊ y +₀₊ x
+    ≤₀₊SumRight (x , _) (y , 0≤y) = begin≤
+      x ≡→≤⟨ sym $ +IdL x ⟩ 0r + x ≤⟨ 0≤y ≤+[ x ] ⟩ y + x ◾
+
+    Δ≤₀₊ : ∀ x y → x -₀₊ y ≤ ⟨ x ⟩₀₊
+    Δ≤₀₊ (x , _) (y , 0≤y) = begin≤
+      x - y ≤⟨ [ x ]+≤ -Flip≤ 0r y 0≤y ⟩ x - 0r ≡→≤⟨ solve! RCR ⟩ x ◾
+
+  private
+    2r = 1r + 1r
+
+  module 1/2∈R (1/2 : R) (1/2≡2⁻¹ : 1/2 · 2r ≡ 1r) where
+
+    1/2+1/2≡1 : 1/2 + 1/2 ≡ 1r
+    1/2+1/2≡1 =
+      1/2 + 1/2 ≡⟨ solve! RCR ⟩
+      1/2 · 2r  ≡⟨ 1/2≡2⁻¹ ⟩
+      1r        ∎
+
+    0<1/2 : 0r < 1/2
+    0<1/2 = flip (PT.rec (is-prop-valued< 0r 1/2))
+      (posSum→pos∨pos 1/2 1/2 (subst (0r <_) (sym 1/2+1/2≡1) 0<1)) λ
+      { (inl 0<1/2) → 0<1/2
+      ; (inr 0<1/2) → 0<1/2
+      }
+
+    0≤1/2 : 0r ≤ 1/2
+    0≤1/2 = <-≤-weaken _ _ 0<1/2
+
+    _/2 : R → R
+    _/2 = _· 1/2
+
+    _/4 : R → R
+    _/4 = _/2 ∘ _/2
+
+    mean : R → R → R
+    mean x y = (x + y) · 1/2
+
+    /2+/2≡mean : ∀ x y → x /2 + y /2 ≡ mean x y
+    /2+/2≡mean x y = sym (·DistL+ x y 1/2)
+
+    meanIdem : ∀ x → mean x x ≡ x
+    meanIdem x =
+      (x + x) · 1/2     ≡⟨ solve! RCR ⟩
+      x · (1/2 + 1/2)   ≡⟨ cong (x ·_) 1/2+1/2≡1 ⟩
+      x · 1r            ≡⟨ ·IdR x ⟩
+      x                 ∎
+
+    <→<mean : ∀ x y → x < y → x < mean x y
+    <→<mean x y x<y = begin<
+      x             ≡→≤⟨ sym (meanIdem x) ⟩
+      (x + x) · 1/2   <⟨ ([ x ]+< x<y) <·[ 1/2 , 0<1/2 ] ⟩
+      (x + y) · 1/2   ◾
+
+    <→mean< : ∀ x y → x < y → mean x y < y
+    <→mean< x y x<y = begin<
+      (x + y) · 1/2   <⟨ (x<y <+[ y ]) <·[ 1/2 , 0<1/2 ] ⟩
+      (y + y) · 1/2 ≡→≤⟨ meanIdem y ⟩
+      y               ◾
+
+    /2+/2≡id : ∀ x → x /2 + x /2 ≡ x
+    /2+/2≡id x = /2+/2≡mean x x ∙ meanIdem x
+
+    id-/2≡/2 : ∀ x → x - x /2 ≡ x /2
+    id-/2≡/2 x = cong (_- x /2) (sym (/2+/2≡id x)) ∙ solve! RCR
+
+    /4+/4≡/2 : ∀ x → x /4 + x /4 ≡ x /2
+    /4+/4≡/2 = /2+/2≡id ∘ (_/2)
+
+    /4+/4+/4+/4≡id : ∀ x → (x /4 + x /4) + (x /4 + x /4) ≡ x
+    /4+/4+/4+/4≡id x = cong (∘diag _+_) (/4+/4≡/2 x) ∙ /2+/2≡id x
+
+    /2-/4≡/4 : ∀ x → x /2 - x /4 ≡ x /4
+    /2-/4≡/4 = id-/2≡/2 ∘ (_/2)
+
+    id-[/4+/4]≡/2 : ∀ x → x - (x /4 + x /4) ≡ x /2
+    id-[/4+/4]≡/2 x = cong (_-_ x) (/4+/4≡/2 x) ∙ id-/2≡/2 x
+
+  module PositiveHalves
+    (1/2 : R)
+    (1/2≡2⁻¹ : 1/2 · 2r ≡ 1r)
+    (0<+Closed : (x y : R) → 0r < x → 0r < y → 0r < x + y)
+    (0<·Closed : (x y : R) → 0r < x → 0r < y → 0r < x · y)
+    where
+
+    open 1/2∈R 1/2 1/2≡2⁻¹
+    open Positive 0<+Closed 0<·Closed
+
+    _/2₊ : R₊ → R₊
+    _/2₊ = _·₊ (1/2 , 0<1/2)
+
+    _/4₊ : R₊ → R₊
+    _/4₊ = _/2₊ ∘ _/2₊
+
+    mean₊ : R₊ → R₊ → R₊
+    mean₊ x y = (x +₊ y) /2₊
+
+    /2₊<id : ∀ x → (x /2₊) <₊ x
+    /2₊<id x = begin<
+      ⟨ x /2₊ ⟩₊            <⟨ <₊SumLeft (x /2₊) (x /2₊) ⟩
+      ⟨ x /2₊ +₊ x /2₊ ⟩₊ ≡→≤⟨ /2+/2≡id ⟨ x ⟩₊ ⟩
+      ⟨ x ⟩₊                ◾
+
+    /4₊</2₊ : ∀ x → (x /4₊) <₊ (x /2₊)
+    /4₊</2₊ = /2₊<id ∘ _/2₊
+
+    /4₊<id : ∀ x → (x /4₊) <₊ x
+    /4₊<id x = begin<
+      ⟨ x /4₊ ⟩₊ <⟨ /4₊</2₊ x ⟩
+      ⟨ x /2₊ ⟩₊ <⟨ /2₊<id x ⟩
+      ⟨ x ⟩₊     ◾
+
+    id-/2₊ : ∀ x → 0r < x -₊ (x /2₊)
+    id-/2₊ x = subst (0r <_) (sym (id-/2≡/2 ⟨ x ⟩₊)) (snd (x /2₊))
+
+    id-[/4+/4]₊ : ∀ x → 0r < x -₊ (x /4₊ +₊ x /4₊)
+    id-[/4+/4]₊ x = subst (0r <_) (cong (_-_ ⟨ x ⟩₊) (sym (/4+/4≡/2 ⟨ x ⟩₊))) (id-/2₊ x)
diff --git a/Cubical/Algebra/OrderedCommRing/Univalence.agda b/Cubical/Algebra/OrderedCommRing/Univalence.agda
new file mode 100644
index 0000000000..a34fe37db5
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing/Univalence.agda
@@ -0,0 +1,77 @@
+module Cubical.Algebra.OrderedCommRing.Univalence where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.OrderedCommRing.Base
+open import Cubical.Algebra.OrderedCommRing.Morphisms
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Displayed.Base
+open import Cubical.Displayed.Auto
+open import Cubical.Displayed.Record
+open import Cubical.Displayed.Universe
+
+private
+  variable
+    ℓ ℓ' ℓ<≤ ℓ<≤' : Level
+
+open Iso
+
+𝒮ᴰ-OrderedCommRing : DUARel (𝒮-Univ ℓ) (OrderedCommRingStr ℓ') (ℓ-max ℓ ℓ')
+𝒮ᴰ-OrderedCommRing =
+  𝒮ᴰ-Record (𝒮-Univ _) IsOrderedCommRingEquiv
+    (fields:
+      data[ 0r ∣ null ∣ pres0 ]
+      data[ 1r ∣ null ∣ pres1 ]
+      data[ _+_ ∣ bin ∣ pres+ ]
+      data[ _·_ ∣ bin ∣ pres· ]
+      data[ -_ ∣ un ∣ pres- ]
+      data[ _<_ ∣ binRel ∣ pres< ]
+      data[ _≤_ ∣ binRel ∣ pres≤ ]
+      prop[ isOrderedCommRing ∣ (λ _ _ → isPropIsOrderedCommRing _ _ _ _ _ _ _) ])
+  where
+    open OrderedCommRingStr
+    open IsOrderedCommRingEquiv
+
+    -- faster with some sharing
+    null = autoDUARel (𝒮-Univ _) (λ A → A)
+    un = autoDUARel (𝒮-Univ _) (λ A → A → A)
+    bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)
+    binRel = autoDUARel (𝒮-Univ _) (λ A → A → A → Type _)
+
+OrderedCommRingPath : (R S : OrderedCommRing ℓ ℓ') → OrderedCommRingEquiv R S ≃ (R ≡ S)
+OrderedCommRingPath = ∫ 𝒮ᴰ-OrderedCommRing .UARel.ua
+
+uaOrderedCommRing : {A B : OrderedCommRing ℓ ℓ'} → OrderedCommRingEquiv A B → A ≡ B
+uaOrderedCommRing {A = A} {B = B} = equivFun (OrderedCommRingPath A B)
+
+OrderedCommRingIso : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _
+OrderedCommRingIso R S =
+  Σ[ e ∈ Iso (R .fst) (S .fst) ] IsOrderedCommRingMono (R .snd) (e .fun) (S .snd)
+
+OrderedCommRingEquivIsoOrderedCommRingIso : (R : OrderedCommRing ℓ  ℓ<≤)
+                                          → (S : OrderedCommRing ℓ' ℓ<≤')
+                                          → Iso (OrderedCommRingEquiv R S)
+                                                (OrderedCommRingIso R S)
+OrderedCommRingEquivIsoOrderedCommRingIso R S = OCREquivIsoOCRIso
+  where
+    open Iso
+    OCREquivIsoOCRIso : Iso (OrderedCommRingEquiv R S) (OrderedCommRingIso R S)
+    fst (fun OCREquivIsoOCRIso e) = equivToIso (fst e)
+    snd (fun OCREquivIsoOCRIso e) = snd (OrderedCommRingEquiv→OrderedCommRingMono e)
+    fst (inv OCREquivIsoOCRIso e) = isoToEquiv (fst e)
+    snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquivFromIsMono (isoToEquiv (fst e)) (snd e)
+    sec OCREquivIsoOCRIso e =
+      Σ≡Prop (λ f → isPropIsOrderedCommRingMono _ (fun f) _) (
+      Iso≡Set (OrderedCommRingStr.is-set (snd R)) (OrderedCommRingStr.is-set (snd S))
+        _ _ (λ x → refl) (λ x → refl))
+    ret OCREquivIsoOCRIso e =
+      Σ≡Prop (λ f → isPropIsOrderedCommRingEquiv _ f _) (equivEq refl)
+
+isGroupoidOrderedCommRing : isGroupoid (OrderedCommRing ℓ ℓ')
+isGroupoidOrderedCommRing _ _ =
+  isOfHLevelRespectEquiv 2 (OrderedCommRingPath _ _) (isSetOrderedCommRingEquiv _ _)
diff --git a/Cubical/Algebra/Ring/Properties.agda b/Cubical/Algebra/Ring/Properties.agda
index 1f9b90f29e..6c8b1a81ef 100644
--- a/Cubical/Algebra/Ring/Properties.agda
+++ b/Cubical/Algebra/Ring/Properties.agda
@@ -14,6 +14,8 @@ open import Cubical.Foundations.Path
 
 open import Cubical.Functions.Embedding
 
+import Cubical.Data.Nat.Base as ℕ
+import Cubical.Data.Int.Base as ℤ
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Monoid
@@ -154,6 +156,15 @@ module RingTheory (R' : Ring ℓ) where
   ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
   ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ congL _·_ (sym (·Assoc x y z))
 
+  fromℕ : ℕ.ℕ → R
+  fromℕ ℕ.zero = 0r
+  fromℕ (ℕ.suc ℕ.zero) = 1r
+  fromℕ (ℕ.suc (ℕ.suc n)) = 1r + fromℕ (ℕ.suc n)
+
+  fromℤ : ℤ.ℤ → R
+  fromℤ (ℤ.pos n) = fromℕ n
+  fromℤ (ℤ.negsuc n) = - (fromℕ (ℕ.suc n))
+
 Ring→Semiring : Ring ℓ → Semiring ℓ
 Ring→Semiring R =
   let open RingStr (snd R)