diff --git a/Lattice.agda b/Lattice.agda
index dc170cf..7c6e0ba 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -137,7 +137,7 @@ module _ {a b} {A : Set a} {B : Set b}
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
-    open import Data.List as List using (List; foldr; _∷_)
+    open import Data.List as List using (List; foldr; foldl; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
@@ -150,13 +150,22 @@ module _ {a b} {A : Set a} {B : Set b}
         ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                  (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
 
+    foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
+                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
+                 (∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
+                 (∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
+                 foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
+    foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
+    foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
+        foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
+
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
          (lB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
 
-    open import Data.List as List using (List; foldr; _∷_)
+    open import Data.List as List using (List; foldr; foldl; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
@@ -165,6 +174,12 @@ module _ {a b} {A : Set a} {B : Set b}
     foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
     foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
 
+    foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
+                  (∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
+                  Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
+    foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
+    foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)