diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 6e03f57..7aaeec3 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -356,16 +356,6 @@ lvCombine-homo₂ plt plts f (e₁ ∨ e₂)
 ...   | just x₁ | nothing = refl
 ...   | nothing | just x₂ = refl
 
-lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
-                 (∀ plt →  PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
-                 ∀ (L : List (PartialLatticeType a)) →
-                 PartialComm (eqL L) (lvCombine f L)
-lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
-    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
-lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
-lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
-lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
-
 lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
                   (∀ plt →  PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
                   ∀ (L : List (PartialLatticeType a)) →
@@ -397,18 +387,41 @@ lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₂
     rewrite lvCombine-homo₂ plt plts f ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
     = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-assoc f f-assoc plts lv₁ lv₂ lv₃)
 
-lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
-lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm
+lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
+                 (∀ plt →  PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
+                 ∀ (L : List (PartialLatticeType a)) →
+                 PartialComm (eqL L) (lvCombine f L)
+lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
+    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
+lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
+lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
+lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
+
+lvCombine-idemp : ∀ {a} (f : CombineForPLT a) →
+                  (∀ plt →  PartialIdemp (PartialLatticeType._≈_ plt) (f plt)) →
+                  ∀ (L : List (PartialLatticeType a)) →
+                  PartialIdemp (eqL L) (lvCombine f L)
+lvCombine-idemp f f-idemp (plt ∷ plts) (inj₁ v) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-idemp plt v)
+lvCombine-idemp f f-idemp (plt ∷ plts) (inj₂ lv) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-idemp f f-idemp plts lv)
 
 lvJoin-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvJoin L)
 lvJoin-assoc = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc
 
-lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
-lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm
+lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
+lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm
+
+lvJoin-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvJoin L)
+lvJoin-idemp = lvCombine-idemp PartialLatticeType._⊔?_ PartialLatticeType.⊔-idemp
 
 lvMeet-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvMeet L)
 lvMeet-assoc = lvCombine-assoc PartialLatticeType._⊓?_ PartialLatticeType.⊓-assoc
 
+lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
+lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm
+
+lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
+lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp
+
 pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls)
 pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂
 pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)