diff --git a/CHANGELOG.md b/CHANGELOG.md
index 205f684cb9..78c3c5acc4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -82,6 +82,11 @@ Deprecated names
   homo  ↦  ∙-homo
   ```
 
+* In `Data.DifferenceList.Base`:
+  ```agda
+  lift ↦ _++_
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   _≟_      ↦  _≡?_
@@ -155,6 +160,10 @@ New modules
 * `Data.Bool.ListAction.Properties` for properties of conjunction and
   disjunction of lists.
 
+* `Data.DifferenceList` has been refactored to reexport the contents of two new modules:
+  - `Data.DifferenceList.Base`
+  - `Data.DifferenceList.Properties`
+
 * A new type of lists that grow on the right.
   This is typically useful to model contexts of typing rules
   or type accumulators that need to be reversed in the base case.
diff --git a/src/Data/DifferenceList.agda b/src/Data/DifferenceList.agda
index d65a41bd1d..83b1066eb0 100644
--- a/src/Data/DifferenceList.agda
+++ b/src/Data/DifferenceList.agda
@@ -1,84 +1,15 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Lists with fast append
+-- A DiffList is a List with fast append.
+-- Based on Hughes' 'A NOVEL REPRESENTATION OF LISTS AND ITS APPLICATION
+-- TO THE FUNCTION "REVERSE"'
+-- DiffList is the Cayley representation for the List.++ monoid.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.DifferenceList where
 
-open import Level using (Level)
-open import Data.List.Base as List using (List)
-open import Function.Base using (_⟨_⟩_)
-open import Data.Nat.Base using (ℕ)
-
-private
-  variable
-    a b : Level
-    A : Set a
-    B : Set b
-
-------------------------------------------------------------------------
--- Type definition and list function lifting
-
-DiffList : Set a → Set a
-DiffList A = List A → List A
-
-lift : (List A → List A) → (DiffList A → DiffList A)
-lift f xs = λ k → f (xs k)
-
-------------------------------------------------------------------------
--- Building difference lists
-
-infixr 5 _∷_ _++_
-
-[] : DiffList A
-[] = λ k → k
-
-_∷_ : A → DiffList A → DiffList A
-_∷_ x = lift (x List.∷_)
-
-[_] : A → DiffList A
-[ x ] = x ∷ []
-
-_++_ : DiffList A → DiffList A → DiffList A
-xs ++ ys = λ k → xs (ys k)
-
-infixl 6 _∷ʳ_
-_∷ʳ_ : DiffList A → A → DiffList A
-xs ∷ʳ x = λ k → xs (x List.∷ k)
-
-------------------------------------------------------------------------
--- Conversion back and forth with List
-
-toList : DiffList A → List A
-toList xs = xs List.[]
-
--- fromList xs is linear in the length of xs.
-
-fromList : List A → DiffList A
-fromList xs = λ k → xs ⟨ List._++_ ⟩ k
-
-------------------------------------------------------------------------
--- Transforming difference lists
-
--- It is OK to use List._++_ here, since map is linear in the length of
--- the list anyway.
-
-map : (A → B) → DiffList A → DiffList B
-map f xs = λ k → List.map f (toList xs) ⟨ List._++_ ⟩ k
-
--- concat is linear in the length of the outer list.
-
-concat : DiffList (DiffList A) → DiffList A
-concat xs = concat′ (toList xs)
-  where
-  concat′ : List (DiffList A) → DiffList A
-  concat′ = List.foldr _++_ []
-
-take : ℕ → DiffList A → DiffList A
-take n = lift (List.take n)
-
-drop : ℕ → DiffList A → DiffList A
-drop n = lift (List.drop n)
+open import Data.DifferenceList.Base public
+open import Data.DifferenceList.Properties public
diff --git a/src/Data/DifferenceList/Base.agda b/src/Data/DifferenceList/Base.agda
new file mode 100644
index 0000000000..bfe442511e
--- /dev/null
+++ b/src/Data/DifferenceList/Base.agda
@@ -0,0 +1,94 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- DiffList: basic types and operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.DifferenceList.Base where
+
+open import Data.List.Base as List using (List)
+open import Data.Nat.Base using (ℕ)
+open import Function using (_∘′_; id)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+
+------------------------------------------------------------------------
+-- Type definition
+
+DiffList : Set a → Set a
+DiffList A = List A → List A
+
+------------------------------------------------------------------------
+-- Building difference lists
+
+infixr 5 _∷_ _++_
+
+[] : DiffList A
+[] = id
+
+[_] : A → DiffList A
+[ x ] = x List.∷_
+
+_++_ : DiffList A → DiffList A → DiffList A
+_++_ = _∘′_
+
+_∷_ : A → DiffList A → DiffList A
+x ∷ xs = [ x ] ++ xs
+
+infixl 6 _∷ʳ_
+_∷ʳ_ : DiffList A → A → DiffList A
+xs ∷ʳ x = xs ++ [ x ]
+
+------------------------------------------------------------------------
+-- Conversion back and forth with List
+
+toList : DiffList A → List A
+toList xs = xs List.[]
+
+-- fromList xs is linear in the length of xs.
+
+fromList : List A → DiffList A
+fromList = List._++_
+
+------------------------------------------------------------------------
+-- Transforming difference lists
+
+-- It is OK to use List._++_ here, since map is linear in the length of
+-- the list anyway.
+
+map : (A → B) → DiffList A → DiffList B
+map f = fromList ∘′ List.map f ∘′ toList
+
+-- concat is linear in the length of the outer list.
+
+concat : DiffList (DiffList A) → DiffList A
+concat = List.foldr _++_ [] ∘′ toList
+
+take : ℕ → DiffList A → DiffList A
+take n = List.take n ++_
+
+drop : ℕ → DiffList A → DiffList A
+drop n = List.drop n ++_
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 3.0
+lift : DiffList A → DiffList A → DiffList A
+lift = _++_
+{-# WARNING_ON_USAGE lift
+"Warning: lift was deprecated in v3.0.
+Please use _++_ instead."
+#-}
diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda
new file mode 100644
index 0000000000..2999d813b8
--- /dev/null
+++ b/src/Data/DifferenceList/Properties.agda
@@ -0,0 +1,84 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of operations on DiffList
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.DifferenceList.Properties where
+
+open import Data.DifferenceList.Base
+  using (DiffList; fromList; toList; []; _∷_; [_]; _++_; _∷ʳ_; map)
+open import Data.List as List using (List)
+open import Data.List.Properties using (++-assoc; ++-identityʳ)
+open import Function using (id)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; cong; _≗_; module ≡-Reasoning)
+
+open ≡-Reasoning
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+    xs xs₁ xs₂ : List A
+    ys ys₁ ys₂ : DiffList A
+
+
+------------------------------------------------------------------------
+-- Relation between Lists and equivalent DiffLists
+
+infix 4 _∼_
+_∼_ : List A → DiffList A → Set _
+xs ∼ ys = fromList xs ≗ ys
+
+------------------------------------------------------------------------
+-- Properties of fromList and toList
+
+∼-fromList : xs ∼ fromList xs
+∼-fromList _ = refl
+
+toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
+toList∘fromList = ++-identityʳ
+
+toList⁺ : xs ∼ ys → xs ≡ toList ys
+toList⁺ {xs = xs} {ys} xs∼ys = begin
+  xs                  ≡⟨ ++-identityʳ xs ⟨
+  xs List.++ List.[]  ≡⟨ xs∼ys List.[] ⟩
+  ys List.[]          ≡⟨⟩
+  toList ys           ∎
+
+------------------------------------------------------------------------
+-- Properties of operations that preserve _∼_
+
+[]⁺ : List.[] {A = A} ∼ []
+[]⁺ _ = refl
+
+[_]⁺ : (x : A) → List.[ x ] ∼ [ x ]
+[_]⁺ _ _ = refl
+
+++⁺ : xs₁ ∼ ys₁ → xs₂ ∼ ys₂ → xs₁ List.++ xs₂ ∼ ys₁ ++ ys₂
+++⁺ {xs₁ = xs₁} {ys₁ = ys₁} {xs₂ = xs₂} {ys₂ = ys₂}
+    xs₁∼ys₁ xs₂∼ys₂ k = begin
+  (xs₁ List.++ xs₂) List.++ k  ≡⟨ ++-assoc xs₁ xs₂ k ⟩
+  xs₁ List.++ (xs₂ List.++ k)  ≡⟨ cong (xs₁ List.++_) (xs₂∼ys₂ k) ⟩
+  xs₁ List.++ ys₂ k            ≡⟨ xs₁∼ys₁ (ys₂ k) ⟩
+  ys₁ (ys₂ k)                  ≡⟨⟩
+  (ys₁ ++ ys₂) k               ∎
+
+∷⁺ : (x : A) → xs ∼ ys → x List.∷ xs ∼ x ∷ ys
+∷⁺ {xs = xs} {ys} x xs~ys k = cong (x List.∷_) (xs~ys k)
+
+++-∷⁺ : (x : A) → xs₁ ∼ ys₁ → xs₂ ∼ ys₂ →
+        xs₁ List.++ x List.∷ xs₂ ∼ ys₁ ++ x ∷ ys₂
+++-∷⁺ x xs₁∼ys₁ xs₂∼ys₂ = ++⁺ xs₁∼ys₁ (∷⁺ x xs₂∼ys₂)
+
+∷ʳ⁺ : (x : A) → xs ∼ ys → xs List.∷ʳ x ∼ ys ∷ʳ x
+∷ʳ⁺ {xs = xs} {ys} x xs∼ys k = ++⁺ xs∼ys [ x ]⁺ k
+
+map⁺ : (f : A → B) → xs ∼ ys → List.map f xs ∼ map f ys
+map⁺ f xs∼ys k =
+  cong (λ xs → fromList (List.map f xs) k) (toList⁺ xs∼ys)