diff --git a/Cubical/Algebra/OrderedCommRing.agda b/Cubical/Algebra/OrderedCommRing.agda
new file mode 100644
index 0000000000..2aca413aff
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing.agda
@@ -0,0 +1,3 @@
+module Cubical.Algebra.OrderedCommRing where
+
+open import Cubical.Algebra.OrderedCommRing.Base public
diff --git a/Cubical/Algebra/OrderedCommRing/Base.agda b/Cubical/Algebra/OrderedCommRing/Base.agda
new file mode 100644
index 0000000000..98c46bd005
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing/Base.agda
@@ -0,0 +1,136 @@
+module Cubical.Algebra.OrderedCommRing.Base where
+{-
+  Definition of an commutative ordered ring.
+-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.SIP
+
+import Cubical.Functions.Logic as L
+
+open import Cubical.Relation.Nullary.Base
+
+open import Cubical.Algebra.CommRing.Base
+
+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.Pseudolattice
+
+open BinaryRelation
+
+private
+  variable
+    ℓ ℓ' : Level
+
+record IsOrderedCommRing
+  {R : Type ℓ}
+  (0r 1r : R )
+  (_+_ _·_ : R → R → R)
+  (-_ : R → R)
+  (_<_ _≤_ : R → R → Type ℓ') : Type (ℓ-max ℓ ℓ') where
+  constructor isorderedcommring
+  field
+    isCommRing      : IsCommRing 0r 1r _+_ _·_ -_
+    isPseudolattice : IsPseudolattice _≤_
+    isStrictOrder   : IsStrictOrder _<_
+    <-≤-weaken      : ∀ x y → x < y → x ≤ y
+    ≤≃¬>            : ∀ x y → (x ≤ y) ≃ (¬ (y < x))
+    +MonoR≤         : ∀ x y z → x ≤ y → (x + z) ≤ (y + z)
+    +MonoR<         : ∀ x y z → x < y → (x + z) < (y + z)
+    posSum→pos∨pos  : ∀ x y → 0r < (x + y) → (0r < x) L.⊔′ (0r < y)
+    <-≤-trans       : ∀ x y z → x < y → y ≤ z → x < z
+    ≤-<-trans       : ∀ x y z → x ≤ y → y < z → x < z
+    ·MonoR≤         : ∀ x y z → 0r ≤ z → x ≤ y → (x · z) ≤ (y · z)
+    ·MonoR<         : ∀ x y z → 0r < z → x < y → (x · z) < (y · z)
+    0<1             : 0r < 1r
+
+  open IsCommRing isCommRing public
+  open IsPseudolattice isPseudolattice hiding (is-set) renaming (is-prop-valued to is-prop-valued≤ ; is-trans to is-trans≤
+                                                                ; isPseudolattice to is-pseudolattice
+                                                                ; _∧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
+
+record OrderedCommRingStr (ℓ' : Level) (R : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  constructor orderedcommringstr
+  field
+    0r 1r : R
+    _+_ _·_ : R → R → R
+    -_ : R → R
+    _<_ _≤_ : R → R → Type ℓ'
+    isOrderedCommRing : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
+
+  open IsOrderedCommRing isOrderedCommRing public
+
+  infix  8 -_
+  infixl 7 _·_
+  infixl 6 _+_
+  infix 4 _<_ _≤_
+
+OrderedCommRing : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
+OrderedCommRing ℓ ℓ' = TypeWithStr ℓ (OrderedCommRingStr ℓ')
+
+module _ {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R }
+  {_<_ _≤_ : R → R → Type ℓ'}
+  (is-setR : isSet R)
+  (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
+  (+IdR : (x : R) → x + 0r ≡ x)
+  (+InvR : (x : R) → x + (- x) ≡ 0r)
+  (+Comm : (x y : R) → x + y ≡ y + x)
+  (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
+  (·IdR : (x : R) → x · 1r ≡ x)
+  (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
+  (·Comm : (x y : R) → x · y ≡ y · x)
+  (is-prop-valued≤ : isPropValued _≤_)
+  (is-refl : isRefl _≤_)
+  (is-trans≤ : isTrans _≤_)
+  (is-antisym : isAntisym _≤_)
+  (is-meet-semipseudolattice : isMeetSemipseudolattice (poset R _≤_ (isposet is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym)))
+  (is-join-semipseudolattice : isJoinSemipseudolattice (poset R _≤_ (isposet is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym)))
+  (is-prop-valued : isPropValued _<_)
+  (is-irrefl : isIrrefl _<_)
+  (is-trans : isTrans _<_)
+  (is-asym : isAsym _<_)
+  (is-weakly-linear : isWeaklyLinear _<_)
+  (<-≤-weaken : ∀ x y → x < y → x ≤ y)
+  (≤≃¬> : ∀ x y → (x ≤ y) ≃ (¬ (y < x)))
+  (+MonoR≤ : ∀ x y z → x ≤ y → (x + z) ≤ (y + z))
+  (+MonoR< : ∀ x y z → x < y → (x + z) < (y + z))
+  (posSum→pos∨pos : ∀ x y → 0r < (x + y) → 0r < x L.⊔′ 0r < y)
+  (<-≤-trans : ∀ x y z → x < y → y ≤ z → x < z)
+  (≤-<-trans : ∀ x y z → x ≤ y → y < z → x < z)
+  (·MonoR≤ : ∀ x y z → 0r ≤ z → x ≤ y → (x · z) ≤ (y · z))
+  (·MonoR< : ∀ x y z → 0r < z → x < y → (x · z) < (y · z))
+  (0<1 : 0r < 1r) where
+  makeIsOrderedCommRing : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
+  makeIsOrderedCommRing = OCR where
+    OCR : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
+    IsOrderedCommRing.isCommRing OCR = makeIsCommRing
+      is-setR +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistR+ ·Comm
+    IsOrderedCommRing.isPseudolattice OCR = makeIsPseudolattice
+      is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym
+      is-meet-semipseudolattice is-join-semipseudolattice
+    IsOrderedCommRing.isStrictOrder OCR =
+      isstrictorder is-setR is-prop-valued is-irrefl is-trans is-asym is-weakly-linear
+    IsOrderedCommRing.<-≤-weaken OCR = <-≤-weaken
+    IsOrderedCommRing.≤≃¬> OCR = ≤≃¬>
+    IsOrderedCommRing.+MonoR≤ OCR = +MonoR≤
+    IsOrderedCommRing.+MonoR< OCR = +MonoR<
+    IsOrderedCommRing.posSum→pos∨pos OCR = posSum→pos∨pos
+    IsOrderedCommRing.<-≤-trans OCR = <-≤-trans
+    IsOrderedCommRing.≤-<-trans OCR = ≤-<-trans
+    IsOrderedCommRing.·MonoR≤ OCR = ·MonoR≤
+    IsOrderedCommRing.·MonoR< OCR = ·MonoR<
+    IsOrderedCommRing.0<1 OCR = 0<1
+
+OrderedCommRing→PseudoLattice : OrderedCommRing ℓ ℓ' → Pseudolattice ℓ ℓ'
+OrderedCommRing→PseudoLattice R .fst = R .fst
+OrderedCommRing→PseudoLattice R .snd = pseudolatticestr _ isPseudolattice where
+  open OrderedCommRingStr (str R)
+
+OrderedCommRing→CommRing : OrderedCommRing ℓ ℓ' → CommRing ℓ
+OrderedCommRing→CommRing R .fst = R .fst
+OrderedCommRing→CommRing R .snd = commringstr _ _ _ _ _ isCommRing where
+  open OrderedCommRingStr (str R)
diff --git a/Cubical/Relation/Binary/Order/Pseudolattice.agda b/Cubical/Relation/Binary/Order/Pseudolattice.agda
new file mode 100644
index 0000000000..1f6af66b77
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Pseudolattice.agda
@@ -0,0 +1,3 @@
+module Cubical.Relation.Binary.Order.Pseudolattice where
+
+open import Cubical.Relation.Binary.Order.Pseudolattice.Base public
diff --git a/Cubical/Relation/Binary/Order/Pseudolattice/Base.agda b/Cubical/Relation/Binary/Order/Pseudolattice/Base.agda
new file mode 100644
index 0000000000..a4938e09be
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Pseudolattice/Base.agda
@@ -0,0 +1,59 @@
+module Cubical.Relation.Binary.Order.Pseudolattice.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.SIP
+
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Order.Poset renaming (isPseudolattice to pseudolattice)
+open import Cubical.Relation.Binary.Order.StrictOrder
+
+open BinaryRelation
+
+private
+  variable
+    ℓ ℓ' : Level
+
+record IsPseudolattice {L : Type ℓ} (_≤_ : L → L → Type ℓ') : Type (ℓ-max ℓ ℓ') where
+  constructor ispseudolattice
+
+  field
+    isPoset : IsPoset _≤_
+    isPseudolattice : pseudolattice (poset L _≤_ isPoset)
+
+  open IsPoset isPoset public
+
+  _∧l_ : L → L → L
+  a ∧l b = (isPseudolattice .fst a b) .fst
+
+  _∨l_ : L → L → L
+  a ∨l b = (isPseudolattice .snd a b) .fst
+
+  infixl 7 _∧l_
+  infixl 6 _∨l_
+
+record PseudolatticeStr (ℓ' : Level) (L : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  constructor pseudolatticestr
+
+  field
+    _≤_ : L → L → Type ℓ'
+    is-pseudolattice : IsPseudolattice _≤_
+
+  open IsPseudolattice is-pseudolattice public
+
+Pseudolattice : ∀ ℓ ℓ' → Type (ℓ-suc (ℓ-max ℓ ℓ'))
+Pseudolattice ℓ ℓ' = TypeWithStr ℓ (PseudolatticeStr ℓ')
+
+makeIsPseudolattice : {L : Type ℓ} {_≤_ : L → L → Type ℓ'}
+                      (is-setL : isSet L)
+                      (is-prop-valued : isPropValued _≤_)
+                      (is-refl : isRefl _≤_)
+                      (is-trans : isTrans _≤_)
+                      (is-antisym : isAntisym _≤_)
+                      (is-meet-semipseudolattice : isMeetSemipseudolattice (poset L _≤_ (isposet is-setL is-prop-valued is-refl is-trans is-antisym)))
+                      (is-join-semipseudolattice : isJoinSemipseudolattice (poset L _≤_ (isposet is-setL is-prop-valued is-refl is-trans is-antisym)))
+                      → IsPseudolattice _≤_
+makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-antisym is-meet-semipseudolattice is-join-semipseudolattice = PS
+  where
+    PS : IsPseudolattice _≤_
+    PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
+    PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice