diff --git a/Cubical/Algebra/CommRing/Ideal/Base.agda b/Cubical/Algebra/CommRing/Ideal/Base.agda
index 413d51ff84..89580139a1 100644
--- a/Cubical/Algebra/CommRing/Ideal/Base.agda
+++ b/Cubical/Algebra/CommRing/Ideal/Base.agda
@@ -89,6 +89,12 @@ module CommIdeal (R' : CommRing ℓ) where
  ∑Closed I {n = zero} _ _ = I .snd .contains0
  ∑Closed I {n = suc n} V h = I .snd .+Closed (h zero) (∑Closed I (V ∘ suc) (h ∘ suc))
 
+ open Exponentiation R'
+
+ ^sucClosed : (I : CommIdeal) (x : R) {n : ℕ}
+            → x ∈ I → x ^ suc n ∈ I
+ ^sucClosed I x x∈I = subst-∈ I (·Comm _ x) (·Closed (snd I) _ x∈I)
+
  0Ideal : CommIdeal
  fst 0Ideal x = (x ≡ 0r) , is-set _ _
  +Closed (snd 0Ideal) x≡0 y≡0 = cong₂ (_+_) x≡0 y≡0 ∙ +IdR _
diff --git a/Cubical/Algebra/CommRing/Ideal/Sum.agda b/Cubical/Algebra/CommRing/Ideal/Sum.agda
index 3d8297cef7..edb6d5aa57 100644
--- a/Cubical/Algebra/CommRing/Ideal/Sum.agda
+++ b/Cubical/Algebra/CommRing/Ideal/Sum.agda
@@ -156,6 +156,9 @@ module IdealSum (R' : CommRing ℓ) where
  ·iComm⊆ I J x = map λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
                       → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·Comm (α i) (β i)))
 
+ ·iRincl : ∀ (I J : CommIdeal) → (I ·i J) ⊆ J
+ ·iRincl I J x x∈IJ = ·iLincl J I x (·iComm⊆ I J x x∈IJ)
+
  ·iComm : ∀ (I J : CommIdeal) → I ·i J ≡ J ·i I
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)
 
diff --git a/Cubical/Algebra/CommRing/RadicalIdeal.agda b/Cubical/Algebra/CommRing/RadicalIdeal.agda
index 16faf4c575..0ef3540624 100644
--- a/Cubical/Algebra/CommRing/RadicalIdeal.agda
+++ b/Cubical/Algebra/CommRing/RadicalIdeal.agda
@@ -99,8 +99,12 @@ module RadicalIdeal (R' : CommRing ℓ) where
  1∈√→1∈ : ∀ (I : CommIdeal) → 1r ∈ √ I → 1r ∈ I
  1∈√→1∈ I = PT.rec (∈-isProp (fst I) _) λ (n , 1ⁿ∈I) → subst-∈ I (1ⁿ≡1 n) 1ⁿ∈I
 
+ √Resp⊆ : (I J : CommIdeal) → I ⊆ J → √ I ⊆ √ J
+ √Resp⊆ I J I⊆J x = map (map-snd λ {a} → I⊆J (x ^ a))
+
  -- important lemma for characterization of the Zariski lattice
  open KroneckerDelta (CommRing→Ring R')
+
  √FGIdealCharLImpl : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
          → √ ⟨ V ⟩[ R' ] ⊆ √ I → (∀ i → V i ∈ √ I)
  √FGIdealCharLImpl V I √⟨V⟩⊆√I i = √⟨V⟩⊆√I _ (∈→∈√ ⟨ V ⟩[ R' ] (V i)
@@ -234,3 +238,10 @@ module RadicalIdeal (R' : CommRing ℓ) where
 
  √·Absorb+ : ∀ (I J : CommIdeal) → √ (I ·i (I +i J)) ≡ √ I
  √·Absorb+ I J = CommIdeal≡Char (√·Absorb+LIncl I J) (√·Absorb+RIncl I J)
+
+ √·ContrLIncl : ∀ (I J : CommIdeal) → √ (√ I ·i √ J) ⊆ √ (I ·i J)
+ √·ContrLIncl I J x = √·RContrLIncl I J x ∘ subst (x ∈_) (√·LContr I (√ J))
+
+ √Pres·LIncl : ∀ (I J : CommIdeal) → (√ I ·i √ J) ⊆ √ (I ·i J)
+ √Pres·LIncl I J x = √·ContrLIncl I J x ∘ ∈→∈√ (√ I ·i √ J) x
+
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda
index 273a85f069..6783153981 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Powerset renaming (_∈_ to _∈p_; _⊆_ to _⊆p_; subst-∈ to subst-∈p)
 
 import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Bool
@@ -16,13 +17,17 @@ open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to
                                       ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                       ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                       ; ·-identityʳ to ·ℕ-rid)
-open import Cubical.Data.Sigma.Base
-open import Cubical.Data.Sigma.Properties
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation as PT
+open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Data.FinData
 open import Cubical.Data.Unit
 open import Cubical.Relation.Nullary
 open import Cubical.Relation.Binary
 open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Proset
+open import Cubical.Relation.Binary.Order.Poset.Instances.PosetalReflection as PR
+open import Cubical.Functions.Embedding
 
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Properties
@@ -39,181 +44,208 @@ open import Cubical.Algebra.DistLattice
 open import Cubical.Algebra.Matrix
 
 open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Tactics.CommRingSolver
 
 open Iso
 open BinaryRelation
 open isEquivRel
 
-private
-  variable
-    ℓ ℓ' : Level
+private variable
+  ℓ ℓ' : Level
 
 
 module ZarLat (R' : CommRing ℓ) where
- open CommRingStr (snd R')
- open RingTheory (CommRing→Ring R')
- open Sum (CommRing→Ring R')
- open CommRingTheory R'
- open Exponentiation R'
- open BinomialThm R'
- open CommIdeal R'
- open RadicalIdeal R'
- open isCommIdeal
- open ProdFin R'
- open IdealSum R'
-
- private
-  R = fst R'
-  A = Σ[ n ∈ ℕ ] (FinVec R n)
-  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
-  ⟨ V ⟩ = ⟨ V ⟩[ R' ]
-
- -- This is small!
- _≼_ : A → A → Type ℓ
- (_ , α) ≼ (_ , β) = ∀ i → α i ∈ √ ⟨ β ⟩
-
- private
+  open CommRingStr (snd R')
+  open RingTheory (CommRing→Ring R')
+  open Sum (CommRing→Ring R')
+  open CommRingTheory R'
+  open Exponentiation R'
+  open BinomialThm R'
+  open CommIdeal R'
+  open RadicalIdeal R'
+  open isCommIdeal
+  open ProdFin R'
+  open IdealSum R'
+
+  private
+    R = fst R'
+    A = Σ[ n ∈ ℕ ] (FinVec R n)
+    ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
+    ⟨ V ⟩ = ⟨ V ⟩[ R' ]
+
+  -- This is small!
+  _≼_ : A → A → Type ℓ
+  (_ , α) ≼ (_ , β) = √ ⟨ α ⟩ ⊆ √ ⟨ β ⟩
+
   isRefl≼ : ∀ {a} → a ≼ a
-  isRefl≼ i = ∈→∈√ _ _ (indInIdeal _ _ i)
+  isRefl≼ = ⊆-refl _
 
   isTrans≼ : ∀ {a b c : A} → a ≼ b → b ≼ c → a ≼ c
-  isTrans≼ a≼b b≼c i = (√FGIdealCharRImpl _ _ b≼c) _ (a≼b i)
-
- _∼_ :  A → A → Type ℓ -- \sim
- α ∼ β = (α ≼ β) × (β ≼ α)
-
- ∼PropValued : isPropValued (_∼_)
- ∼PropValued (_ , α) (_ , β) = isProp× (isPropΠ (λ i → √ ⟨ β ⟩ .fst (α i) .snd))
-                                       (isPropΠ (λ i → √ ⟨ α ⟩ .fst (β i) .snd))
-
- ∼EquivRel : isEquivRel (_∼_)
- reflexive ∼EquivRel _ = isRefl≼ , isRefl≼
- symmetric ∼EquivRel _ _ = Σ-swap-Iso .fun
- transitive ∼EquivRel _ _ _ a∼b b∼c = isTrans≼ (fst a∼b) (fst b∼c) , isTrans≼ (snd b∼c) (snd a∼b)
-
- -- lives in the same universe as R
- ZL : Type ℓ
- ZL = A / (_∼_)
-
- --  need something big in our proofs though:
- _∼≡_ : A → A → Type (ℓ-suc ℓ)
- (_ , α) ∼≡ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩
-
- ≡→∼ : ∀ {a b : A} → a ∼≡ b → a ∼ b
- ≡→∼ r = √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) r h)
-       , √FGIdealCharLImpl _ ⟨ _ ⟩ (λ x h → subst (λ p → x ∈ p) (sym r) h)
-
- ∼→≡ : ∀ {a b : A} → a ∼ b → a ∼≡ b
- ∼→≡ r = CommIdeal≡Char (√FGIdealCharRImpl _ ⟨ _ ⟩ (fst r))
-                        (√FGIdealCharRImpl _ ⟨ _ ⟩ (snd r))
-
- ∼≃≡ : ∀ {a b : A} → (a ∼ b) ≃ (a ∼≡ b)
- ∼≃≡ = propBiimpl→Equiv (∼PropValued _ _) (isSetCommIdeal _ _) ∼→≡ ≡→∼
-
- 0z : ZL
- 0z = [ 0 , (λ ()) ]
-
- 1z : ZL
- 1z = [ 1 , (replicateFinVec 1 1r) ]
-
- _∨z_ : ZL → ZL → ZL
- _∨z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
-                          (λ (_ , α) (_ , β) → (_ , α ++Fin β))
-                          (λ (_ , α) (_ , β) → ≡→∼ (cong √
-                             (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
-    λ (_ , α) (_ , β) (_ , γ) α∼β → ≡→∼ (--need to show α∨γ ∼ β∨γ
-      √ ⟨ α ++Fin γ ⟩      ≡⟨ cong √ (FGIdealAddLemma _ α γ) ⟩
-      √ (⟨ α ⟩ +i ⟨ γ ⟩)    ≡⟨ sym (√+LContr _ _) ⟩
-      √ (√ ⟨ α ⟩ +i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I +i ⟨ γ ⟩)) (∼→≡ α∼β) ⟩
-      √ (√ ⟨ β ⟩ +i ⟨ γ ⟩) ≡⟨ √+LContr _ _ ⟩
-      √ (⟨ β ⟩ +i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealAddLemma _ β γ)) ⟩
-      √ ⟨ β ++Fin γ ⟩ ∎)
-
- _∧z_ : ZL → ZL → ZL
- _∧z_ = setQuotSymmBinOp (reflexive ∼EquivRel) (transitive ∼EquivRel)
-                          (λ (_ , α) (_ , β) → (_ , α ··Fin β))
-                          (λ (_ , α) (_ , β) → ≡→∼ (cong √
-                             (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α))))
-    λ (_ , α) (_ , β) (_ , γ) α∼β → ≡→∼ (--need to show α∧γ ∼ β∧γ
-      √ ⟨ α ··Fin γ ⟩       ≡⟨ cong √ (FGIdealMultLemma _ α γ) ⟩
-      √ (⟨ α ⟩ ·i ⟨ γ ⟩)    ≡⟨ sym (√·LContr _ _) ⟩
-      √ (√ ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong (λ I → √ (I ·i ⟨ γ ⟩)) (∼→≡ α∼β) ⟩
-      √ (√ ⟨ β ⟩ ·i ⟨ γ ⟩) ≡⟨ √·LContr _ _ ⟩
-      √ (⟨ β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ β γ)) ⟩
-      √ ⟨ β ··Fin γ ⟩ ∎)
-
- -- join axioms
- ∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
- ∨zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
-          λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼ (cong √ (IdealAddAssoc _ _ _ _)))
-
- ∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
- ∨zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
-        λ (_ , α) (_ , β) → eq/ _ _
-          (≡→∼ (cong √ (FGIdealAddLemma _ α β ∙∙ +iComm _ _ ∙∙ sym (FGIdealAddLemma _ β α))))
-
- ∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
- ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → eq/ _ _ (reflexive ∼EquivRel _)
-
- ∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
- ∨zRid _ = ∨zComm _ _ ∙ ∨zLid _
-
-
- -- -- meet axioms
- ∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
- ∧zAssoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
+  isTrans≼ = ⊆-trans _ _ _
+
+  ≼PropValued : isPropValued _≼_
+  ≼PropValued x y = ⊆-isProp _ _
+
+  isProset≼ : IsProset _≼_
+  isProset≼ = isproset (isSetΣ isSetℕ λ x → isSet→ is-set) ≼PropValued (λ _ → isRefl≼) (λ _ _ _ → isTrans≼)
+
+  _∼_ : A → A → Type ℓ -- \sim
+  _∼_ = SymKernel _≼_
+
+  ∼PropValued : isPropValued (_∼_)
+  ∼PropValued _ _ = isProp× (≼PropValued _ _) (≼PropValued _ _)
+
+  ∼EquivRel : isEquivRel (_∼_)
+  ∼EquivRel = isProset→isEquivRelSymKernel isProset≼
+
+  private
+    AProset : Proset ℓ ℓ
+    AProset = _ , prosetstr _≼_ isProset≼
+
+  -- lives in the same universe as R
+  ZLPoset : Poset ℓ ℓ
+  ZLPoset = ReflectionPoset AProset
+
+  ZL : Type ℓ
+  ZL = ZLPoset .fst
+
+  _≤ZL_ = ZLPoset .snd .PosetStr._≤_
+  isPosetZL = ZLPoset .snd .PosetStr.isPoset
+  isProsetZL = isPoset→isProset isPosetZL
+
+  0a : A
+  0a = 0 , λ ()
+
+  1a : A
+  1a = 1 , λ _ → 1r
+
+  --  need something big in our proofs though:
+
+  _∼≡_ : A → A → Type (ℓ-suc ℓ)
+  (_ , α) ∼≡ (_ , β) = √ ⟨ α ⟩ ≡ √ ⟨ β ⟩
+
+  ≡→∼ : ∀ {a b : A} → a ∼≡ b → a ∼ b
+  ≡→∼ r = ⊆-refl-consequence _ _ (cong fst r)
+
+  ∼→≡ : ∀ {a b : A} → a ∼ b → a ∼≡ b
+  ∼→≡ r = CommIdeal≡Char (r .fst) (r .snd)
+
+  ∼≃≡ : ∀ {a b : A} → (a ∼ b) ≃ (a ∼≡ b)
+  ∼≃≡ = propBiimpl→Equiv (∼PropValued _ _) (isSetCommIdeal _ _) ∼→≡ ≡→∼
+
+  0z : ZL
+  0z = [ 0a ]
+
+  0z-least : isLeast isProsetZL (_ , id↪ _) 0z
+  0z-least = []presLeast AProset 0a λ x → √FGIdealCharRImpl _ _ λ ()
+
+  1z : ZL
+  1z = [ 1a ]
+
+  1z-greatest : isGreatest isProsetZL (_ , id↪ _) 1z
+  1z-greatest = []presGreatest AProset 1a λ x → √FGIdealCharRImpl _ _ λ _ →
+    ∣ 0 , ∣ (λ _ → 1r) , solve! R' ∣₁ ∣₁
+
+  _∨a_ : A → A → A
+  (_ , α) ∨a (_ , β) = _ , α ++Fin β
+
+  ∨a-join : ∀ x y → isJoin isProset≼ x y (x ∨a y)
+  ∨a-join (_ , α) (_ , β) (_ , γ) = propBiimpl→Equiv (≼PropValued _ _) (isProp× (≼PropValued _ _) (≼PropValued _ _)) to fo
+    where
+      to : _
+      to α∨β⊆γ .fst = ⊆-trans _ _ _
+        (√Resp⊆ ⟨ α ⟩ ⟨ α ++Fin β ⟩ (⊆-trans _ _ _ (+iLincl ⟨ α ⟩ ⟨ β ⟩) (FGIdealAddLemmaRIncl _ α β))) α∨β⊆γ
+      to α∨β⊆γ .snd = ⊆-trans _ _ _
+        (√Resp⊆ ⟨ β ⟩ ⟨ α ++Fin β ⟩ (⊆-trans _ _ _ (+iRincl ⟨ α ⟩ ⟨ β ⟩) (FGIdealAddLemmaRIncl _ α β))) α∨β⊆γ
+      fo : _
+      fo (α⊆γ , β⊆γ) = ⊆-trans _ _ _ (√Resp⊆ ⟨ α ++Fin β ⟩ (⟨ α ⟩ +i ⟨ β ⟩) $ FGIdealAddLemmaLIncl _ α β) λ x x∈√α+β → do
+        (n , x^n∈α+β) ← x∈√α+β
+        ((y , z) , y∈α , z∈β , x^n≡y+z) ← x^n∈α+β
+        ^∈√→∈√ _ x n $ subst-∈ (√ ⟨ γ ⟩) (sym x^n≡y+z) $
+          √ ⟨ γ ⟩ .snd .+Closed (α⊆γ y (∈→∈√ _ y y∈α)) (β⊆γ z (∈→∈√ _ z z∈β))
+
+  ZL-joins : isJoinSemipseudolattice ZLPoset
+  ZL-joins = hasBinJoins AProset λ x y → _ , ∨a-join x y
+
+  _∨z_ : ZL → ZL → ZL
+  x ∨z y = ZL-joins x y .fst
+
+  _∧a_ : A → A → A
+  (_ , α) ∧a (_ , β) = _ , α ··Fin β
+
+  ∧a-meet : ∀ x y → isMeet isProset≼ x y (x ∧a y)
+  ∧a-meet (_ , α) (_ , β) (_ , γ) = propBiimpl→Equiv (≼PropValued _ _) (isProp× (≼PropValued _ _) (≼PropValued _ _)) to fo
+    where
+      to : _
+      to γ≼α∧β .fst = ⊆-trans _ _ _ γ≼α∧β $ √Resp⊆ ⟨ α ··Fin β ⟩ ⟨ α ⟩ $
+                      ⊆-trans _ _ _ (FGIdealMultLemmaLIncl _ α β) (·iLincl ⟨ α ⟩ ⟨ β ⟩)
+      to γ≼α∧β .snd = ⊆-trans _ _ _ γ≼α∧β $ √Resp⊆ ⟨ α ··Fin β ⟩ ⟨ β ⟩ $
+                      ⊆-trans _ _ _ (FGIdealMultLemmaLIncl _ α β) (·iRincl ⟨ α ⟩ ⟨ β ⟩)
+      fo : _
+      fo (γ≼α , γ≼β) = ⊆-trans _ _ _ (λ x x∈√γ →
+          ∣ 2 , subst-∈ (√ ⟨ α ⟩ ·i √ ⟨ β ⟩) (solve! R') (prodInProd _ _ x x (γ≼α x x∈√γ) (γ≼β x x∈√γ)) ∣₁
+        ) $ ⊆-trans _ _ _ (√·ContrLIncl ⟨ α ⟩ ⟨ β ⟩) $
+        √Resp⊆ (⟨ α ⟩ ·i ⟨ β ⟩) ⟨ α ··Fin β ⟩ $ FGIdealMultLemmaRIncl _ α β
+
+  ZL-meets : isMeetSemipseudolattice ZLPoset
+  ZL-meets = hasBinMeets AProset λ x y → _ , ∧a-meet x y
+
+  _∧z_ : ZL → ZL → ZL
+  x ∧z y = ZL-meets x y .fst
+
+  -- join axioms
+  ∨zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∨z (𝔟 ∨z 𝔠) ≡ (𝔞 ∨z 𝔟) ∨z 𝔠
+  ∨zAssoc = joinAssoc isPosetZL ZL-joins
+
+  ∨zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∨z 𝔟 ≡ 𝔟 ∨z 𝔞
+  ∨zComm = joinComm isPosetZL ZL-joins
+
+  ∨zLid : ∀ (𝔞 : ZL) → 0z ∨z 𝔞 ≡ 𝔞
+  ∨zLid = SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
+
+  ∨zRid : ∀ (𝔞 : ZL) → 𝔞 ∨z 0z ≡ 𝔞
+  ∨zRid _ = ∨zComm _ _ ∙ ∨zLid _
+
+  -- -- meet axioms
+  ∧zAssoc : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∧z 𝔠) ≡ (𝔞 ∧z 𝔟) ∧z 𝔠
+  ∧zAssoc = meetAssoc isPosetZL ZL-meets
+
+  ∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
+  ∧zComm = meetComm isPosetZL ZL-meets
+
+  ∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
+  ∧zRid = SQ.elimProp (λ _ → squash/ _ _) λ (_ , α) → eq/ _ _ $ ≡→∼ $ cong √ $
+    ⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
+    ⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
+    ⟨ α ⟩ ·i 1Ideal                     ≡⟨ ·iRid _ ⟩
+    ⟨ α ⟩ ∎
+
+  -- absorption and distributivity
+  ∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
+  ∧zAbsorb∨z = MeetAbsorbLJoin ZLPoset (ZL-meets , ZL-joins)
+
+  ∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
+  ∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
     λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼
-      (√ ⟨ α ··Fin (β ··Fin γ) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
-       √ (⟨ α ⟩ ·i ⟨ β ··Fin γ ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealMultLemma _ _ _) ⟩
-       √ (⟨ α ⟩ ·i (⟨ β ⟩ ·i ⟨ γ ⟩)) ≡⟨ cong √ (·iAssoc _ _ _) ⟩
-       √ ((⟨ α ⟩ ·i ⟨ β ⟩) ·i ⟨ γ ⟩) ≡⟨ cong (λ x → √ (x ·i ⟨ γ ⟩)) (sym (FGIdealMultLemma _ _ _)) ⟩
-       √ (⟨ α ··Fin β ⟩ ·i ⟨ γ ⟩)    ≡⟨ cong √ (sym (FGIdealMultLemma _ _ _)) ⟩
-       √ ⟨ (α ··Fin β) ··Fin γ ⟩     ∎))
-
- ∧zComm : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z 𝔟 ≡ 𝔟 ∧z 𝔞
- ∧zComm = SQ.elimProp2 (λ _ _ → squash/ _ _)
-        λ (_ , α) (_ , β) → eq/ _ _ (≡→∼
-          (cong √ (FGIdealMultLemma _ α β ∙∙ ·iComm _ _ ∙∙ sym (FGIdealMultLemma _ β α))))
-
- ∧zRid : ∀ (𝔞 : ZL) → 𝔞 ∧z 1z ≡ 𝔞
- ∧zRid = SQ.elimProp (λ _ → squash/ _ _)
-   λ (_ , α) → eq/ _ _ (≡→∼ (cong √
-     (⟨ α ··Fin (replicateFinVec 1 1r) ⟩ ≡⟨ FGIdealMultLemma _ _ _ ⟩
-      ⟨ α ⟩ ·i ⟨ (replicateFinVec 1 1r) ⟩ ≡⟨ cong (⟨ α ⟩ ·i_) (contains1Is1 _ (indInIdeal _ _ zero)) ⟩
-      ⟨ α ⟩ ·i 1Ideal                     ≡⟨ ·iRid _ ⟩
-      ⟨ α ⟩ ∎)))
-
-
- -- absorption and distributivity
- ∧zAbsorb∨z : ∀ (𝔞 𝔟 : ZL) → 𝔞 ∧z (𝔞 ∨z 𝔟) ≡ 𝔞
- ∧zAbsorb∨z = SQ.elimProp2 (λ _ _ → squash/ _ _)
-            λ (_ , α) (_ , β) → eq/ _ _ (≡→∼
-              (√ ⟨ α ··Fin (α ++Fin β) ⟩     ≡⟨ cong √ (FGIdealMultLemma _ α (α ++Fin β)) ⟩
-               √ (⟨ α ⟩ ·i ⟨ α ++Fin β ⟩)    ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ α β) ⟩
-               √ (⟨ α ⟩ ·i (⟨ α ⟩ +i ⟨ β ⟩)) ≡⟨ √·Absorb+ _ _ ⟩
-               √ ⟨ α ⟩ ∎))
-
- ∧zLDist∨z : ∀ (𝔞 𝔟 𝔠 : ZL) → 𝔞 ∧z (𝔟 ∨z 𝔠) ≡ (𝔞 ∧z 𝔟) ∨z (𝔞 ∧z 𝔠)
- ∧zLDist∨z = SQ.elimProp3 (λ _ _ _ → squash/ _ _)
-   λ (_ , α) (_ , β) (_ , γ) → eq/ _ _ (≡→∼
-     (√ ⟨ α ··Fin (β ++Fin γ) ⟩            ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
-      √ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩)           ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
-      √ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩))        ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
-      -- L/R-dist are swapped
-      -- in Lattices vs Rings
-      √ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
-                                                     (sym (FGIdealMultLemma _ _ _))
-                                                     (sym (FGIdealMultLemma _ _ _)) ⟩
-      √ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩)   ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
-      √ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩  ∎))
-
-
- ZariskiLattice : DistLattice ℓ
- fst ZariskiLattice = ZL
- DistLatticeStr.0l (snd ZariskiLattice) = 0z
- DistLatticeStr.1l (snd ZariskiLattice) = 1z
- DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
- DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
- DistLatticeStr.isDistLattice (snd ZariskiLattice) =
-   makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
-                                       ∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z
+      (√ ⟨ α ··Fin (β ++Fin γ) ⟩            ≡⟨ cong √ (FGIdealMultLemma _ _ _) ⟩
+        √ (⟨ α ⟩ ·i ⟨ β ++Fin γ ⟩)           ≡⟨ cong (λ x → √ (⟨ α ⟩ ·i x)) (FGIdealAddLemma _ _ _) ⟩
+        √ (⟨ α ⟩ ·i (⟨ β ⟩ +i ⟨ γ ⟩))        ≡⟨ cong √ (·iRdist+i _ _ _) ⟩
+        -- L/R-dist are swapped
+        -- in Lattices vs Rings
+        √ (⟨ α ⟩ ·i ⟨ β ⟩ +i ⟨ α ⟩ ·i ⟨ γ ⟩) ≡⟨ cong₂ (λ x y → √ (x +i y))
+                                                      (sym (FGIdealMultLemma _ _ _))
+                                                      (sym (FGIdealMultLemma _ _ _)) ⟩
+        √ (⟨ α ··Fin β ⟩ +i ⟨ α ··Fin γ ⟩)   ≡⟨ cong √ (sym (FGIdealAddLemma _ _ _)) ⟩
+        √ ⟨ (α ··Fin β) ++Fin (α ··Fin γ) ⟩  ∎))
+
+  ZariskiLattice : DistLattice ℓ
+  fst ZariskiLattice = ZL
+  DistLatticeStr.0l (snd ZariskiLattice) = 0z
+  DistLatticeStr.1l (snd ZariskiLattice) = 1z
+  DistLatticeStr._∨l_ (snd ZariskiLattice) = _∨z_
+  DistLatticeStr._∧l_ (snd ZariskiLattice) = _∧z_
+  DistLatticeStr.isDistLattice (snd ZariskiLattice) =
+    makeIsDistLattice∧lOver∨l squash/ ∨zAssoc ∨zRid ∨zComm
+                                        ∧zAssoc ∧zRid ∧zComm ∧zAbsorb∨z ∧zLDist∨z
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda
index 5427849bf4..843ab15d0d 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda
@@ -65,7 +65,7 @@ module _ (R : CommRing ℓ) where
     D1≤Df = subst (_≤ D f) Df≡D1 (is-refl _)
 
     1∈√⟨f⟩ : 1r ∈ √ ⟨ replicateFinVec 1 f ⟩
-    1∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst zero
+    1∈√⟨f⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst) zero
 
 
   module _ {n : ℕ} (f₁,⋯,fₙ : FinVec (fst R) n) where
@@ -80,9 +80,8 @@ module _ (R : CommRing ℓ) where
       D1≤D[f₁,⋯,fₙ] = subst (_≤ D[f₁,⋯,fₙ]) D[f₁,⋯,fₙ]≡D1 (is-refl _)
 
       1∈√⟨f₁,⋯,fₙ⟩ : 1r ∈ √ ⟨ f₁,⋯,fₙ ⟩
-      1∈√⟨f₁,⋯,fₙ⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
-                       D1≤D[f₁,⋯,fₙ] .fst zero
-
+      1∈√⟨f₁,⋯,fₙ⟩ = √FGIdealCharLImpl _ _
+        (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤D[f₁,⋯,fₙ] .fst) zero
 
 
 module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
index 0ca7597380..ed5b7a20ea 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
@@ -142,7 +142,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       _ = snd R[1/ f ]AsCommRing
 
     f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩ₛ
-    f∈√⟨g⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst zero
+    f∈√⟨g⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst) zero
 
 
  -- The structure presheaf on BO
@@ -251,11 +251,11 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
 
       -- crucial facts about radical ideals
       h∈√⟨f⟩ : h ∈ √ ⟨ f ⟩[ R' ]
-      h∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst zero
+      h∈√⟨f⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst) zero
 
       f∈√⟨h⟩ : ∀ i → f i ∈ √ ⟨ h ⟩ₛ
-      f∈√⟨h⟩ i = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
-                   (sym DHelper) .fst i
+      f∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
+                   (sym DHelper) .fst)
 
       ff∈√⟨h⟩ : ∀ i j → f i · f j ∈ √ ⟨ h ⟩ₛ
       ff∈√⟨h⟩ i j = √ ⟨ h ⟩ₛ .snd .·Closed (f i) (f∈√⟨h⟩ j)
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
index 41695c786a..079716ee6b 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
@@ -166,7 +166,7 @@ module _ (R' : CommRing ℓ) where
     Df≤Dg = subst2 _≤_ (sym p) (sym q) 𝔞≤𝔟
 
     f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩
-    f∈√⟨g⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst zero
+    f∈√⟨g⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst) zero
 
 
  open PreSheafFromUniversalProp ZariskiCat P 𝓕 uniqueHom
@@ -278,16 +278,16 @@ module _ (R' : CommRing ℓ) where
     DHelper = Dh≡𝔞∨𝔟 ∙ cong₂ (_∨z_) (sym Df≡𝔞) (sym Dg≡𝔟)
 
     f∈√⟨h⟩ : f ∈ √ ⟨ h ⟩
-    f∈√⟨h⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst zero
+    f∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst) zero
 
     g∈√⟨h⟩ : g ∈ √ ⟨ h ⟩
-    g∈√⟨h⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst one
+    g∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst) one
 
     fg∈√⟨h⟩ : (f · g) ∈ √ ⟨ h ⟩
     fg∈√⟨h⟩ = √ ⟨ h ⟩ .snd .·Closed f g∈√⟨h⟩
 
     1∈fgIdeal : 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
-    1∈fgIdeal = helper1 (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst zero)
+    1∈fgIdeal = helper1 $ √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst) zero
      where
      helper1 : h ∈ √ ⟨ f , g ⟩ₚ
              → 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
index 043a0dfed8..8825a4f8c9 100644
--- a/Cubical/Foundations/Powerset.agda
+++ b/Cubical/Foundations/Powerset.agda
@@ -58,6 +58,12 @@ subst-∈ A = subst (_∈ A)
 ⊆-extensionality A B (φ , ψ) =
   funExt (λ x → TypeOfHLevel≡ 1 (hPropExt (A x .snd) (B x .snd) (φ x) (ψ x)))
 
+⊆-trans : (A B C : ℙ X) → A ⊆ B → B ⊆ C → A ⊆ C
+⊆-trans A B C φ ψ x = ψ x ∘ φ x
+
+⊆-antisym : (A B : ℙ X) → A ⊆ B → B ⊆ A → A ≡ B
+⊆-antisym A B φ ψ = ⊆-extensionality A B (φ , ψ)
+
 ⊆-extensionalityEquiv : (A B : ℙ X) → (A ⊆ B) × (B ⊆ A) ≃ (A ≡ B)
 ⊆-extensionalityEquiv A B = isoToEquiv (iso (⊆-extensionality A B)
                                             (⊆-refl-consequence A B)
diff --git a/Cubical/Relation/Binary/Order/Poset/Instances/PosetalReflection.agda b/Cubical/Relation/Binary/Order/Poset/Instances/PosetalReflection.agda
new file mode 100644
index 0000000000..f0c16d8173
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Poset/Instances/PosetalReflection.agda
@@ -0,0 +1,115 @@
+{-# OPTIONS --cubical --safe #-}
+
+-- The posetal reflection is the universal way to turn a preorder into a poset
+-- In abstract-nonsense terms, the posetal reflection exhibits Pos as a reflective subcategory of preorders.
+-- https://ncatlab.org/nlab/show/posetal+reflection
+-- When a preorder is viewed as a category, posets are univalent categories
+-- and the posetal reflection is a special case of the Rezk completion.
+
+module Cubical.Relation.Binary.Order.Poset.Instances.PosetalReflection where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+open import Cubical.Functions.Logic
+open import Cubical.Functions.Embedding
+open import Cubical.HITs.SetQuotients as SetQuot using (_/_; [_]; eq/; squash/)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Order.Poset.Base
+open import Cubical.Relation.Binary.Order.Poset.Properties
+open import Cubical.Relation.Binary.Order.Proset
+
+private variable
+  ℓ ℓ' ℓ'' : Level
+
+module _ (P : Proset ℓ ℓ') where
+  open module P = ProsetStr (P .snd) using (_≲_)
+  open ProsetReasoning P renaming (_◾ to _≲∎)
+  open BinaryRelation
+
+  private variable
+    a b c : ⟨ P ⟩
+
+  _~_ : Rel ⟨ P ⟩ ⟨ P ⟩ ℓ'
+  _~_ = SymKernel _≲_
+
+  isEquivRel~ : isEquivRel _~_
+  isEquivRel~ = isProset→isEquivRelSymKernel P.isProset
+
+  Reflection : Type (ℓ-max ℓ ℓ')
+  Reflection = ⟨ P ⟩ / _~_
+
+  _≤'_ : Reflection → Reflection → hProp ℓ'
+  _≤'_ = SetQuot.rec2 isSetHProp (λ a b → a ≲ b , P.is-prop-valued a b)
+    (λ a b c (a≲b , b≲a) → ⇔toPath (λ a≲c → b ≲⟨ b≲a ⟩ a ≲⟨ a≲c ⟩ c ≲∎) (λ b≲c → a ≲⟨ a≲b ⟩ b ≲⟨ b≲c ⟩ c ≲∎))
+    (λ a b c (b≲c , c≲b) → ⇔toPath (λ a≲b → a ≲⟨ a≲b ⟩ b ≲⟨ b≲c ⟩ c ≲∎) (λ a≲c → a ≲⟨ a≲c ⟩ c ≲⟨ c≲b ⟩ b ≲∎))
+
+  _≤_ : Reflection → Reflection → Type ℓ'
+  a ≤ b = ⟨ a ≤' b ⟩
+
+  isPropValued≤ : isPropValued _≤_
+  isPropValued≤ a b = snd (a ≤' b)
+
+  isRefl≤ : isRefl _≤_
+  isRefl≤ = SetQuot.elimProp (λ a → isPropValued≤ a a) P.is-refl
+
+  isTrans≤ : isTrans _≤_
+  isTrans≤ = SetQuot.elimProp3 (λ a b c → isPropΠ2 λ _ _ → isPropValued≤ a c) P.is-trans
+
+  isAntisym≤ : isAntisym _≤_
+  isAntisym≤ = SetQuot.elimProp2 (λ a b → isPropΠ2 λ _ _ → squash/ a b) λ a b a≲b b≲a → eq/ a b (a≲b , b≲a)
+
+  isPoset≤ : IsPoset _≤_
+  isPoset≤ .IsPoset.is-set = squash/
+  isPoset≤ .IsPoset.is-prop-valued = isPropValued≤
+  isPoset≤ .IsPoset.is-refl = isRefl≤
+  isPoset≤ .IsPoset.is-trans = isTrans≤
+  isPoset≤ .IsPoset.is-antisym = isAntisym≤
+
+  ReflectionPoset : Poset (ℓ-max ℓ ℓ') ℓ'
+  ReflectionPoset = Reflection , posetstr _≤_ isPoset≤
+
+  isProset≤ : IsProset _≤_
+  isProset≤ = isPoset→isProset isPoset≤
+
+  private
+    idEmb : {A : Type ℓ''} → Embedding A ℓ''
+    idEmb = _ , id↪ _
+
+  -- if a preorder is bounded, then so is its posetal reflection
+
+  []presLeast : ∀ least → isLeast P.isProset idEmb least → isLeast isProset≤ idEmb [ least ]
+  []presLeast least is-least = SetQuot.elimProp (λ x → isPropValued≤ [ least ] x) is-least
+
+  hasLeast : Least P.isProset idEmb → Least isProset≤ idEmb
+  hasLeast least = [ least .fst ] , []presLeast (least .fst) (least .snd)
+
+  []presGreatest : ∀ greatest → isGreatest P.isProset idEmb greatest → isGreatest isProset≤ idEmb [ greatest ]
+  []presGreatest greatest is-greatest = SetQuot.elimProp (λ x → isPropValued≤ x [ greatest ]) is-greatest
+
+  hasGreatest : Greatest P.isProset idEmb → Greatest isProset≤ idEmb
+  hasGreatest greatest = [ greatest .fst ] , []presGreatest (greatest .fst) (greatest .snd)
+
+  -- if a preorder has binary meets, then so does its posetal reflection
+
+  []presMeets : ∀ meet → isMeet P.isProset a b meet → isMeet isProset≤ [ a ] [ b ] [ meet ]
+  []presMeets meet is-meet = SetQuot.elimProp (λ x → isOfHLevel⁺≃ₗ 0 (isPropValued≤ x [ meet ])) is-meet
+
+  []presHasMeet : Meet P.isProset a b → Meet isProset≤ [ a ] [ b ]
+  []presHasMeet meet = [ meet .fst ] , []presMeets (meet .fst) (meet .snd)
+
+  hasBinMeets : (∀ a b → Meet P.isProset a b) → isMeetSemipseudolattice ReflectionPoset
+  hasBinMeets bin-meets = SetQuot.elimProp2 (MeetUnique isPoset≤) λ a b → []presHasMeet (bin-meets a b)
+
+  -- if a preorder has binary joins, then so does its posetal reflection
+
+  []presJoins : ∀ join → isJoin P.isProset a b join → isJoin isProset≤ [ a ] [ b ] [ join ]
+  []presJoins join is-join = SetQuot.elimProp (λ x → isOfHLevel⁺≃ₗ 0 (isPropValued≤ [ join ] x)) is-join
+
+  []presHasJoin : Join P.isProset a b → Join isProset≤ [ a ] [ b ]
+  []presHasJoin join = [ join .fst ] , []presJoins (join .fst) (join .snd)
+
+  hasBinJoins : (∀ a b → Join P.isProset a b) → isJoinSemipseudolattice ReflectionPoset
+  hasBinJoins bin-joins = SetQuot.elimProp2 (JoinUnique isPoset≤) λ a b → []presHasJoin (bin-joins a b)
+