diff --git a/CHANGELOG.md b/CHANGELOG.md
index 82c677d186..df954bc614 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,7 +48,16 @@ Deprecated names
 
 New modules
 -----------
-* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
+
+* Raw bundles for module-like algebraic structures:
+  ```
+  Algebra.Module.Bundles.Raw
+  ```
+
+* Prime factorisation of natural numbers.
+  ```
+  Data.Nat.Primality.Factorisation
+  ```
 
 * Nagata's construction of the "idealization of a module":
   ```agda
@@ -226,6 +235,18 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
+  
+* Added new proofs to `Data.Nat.Primality`:
+  ```agda
+  rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
+  productOfPrimes≢0 : All Prime as → NonZero (product as)
+  productOfPrimes≥1 : All Prime as → product as ≥ 1
+  ```
+
+* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  product-↭ : product Preserves _↭_ ⟶ _≡_
+  ```
 
 * Added new functions in `Data.String.Base`:
   ```agda
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 781de1cc36..d56bdb7fb3 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -12,7 +12,8 @@ open import Algebra.Bundles
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Nat using (suc)
+open import Data.Nat.Base using (suc; _*_)
+open import Data.Nat.Properties using (*-assoc; *-comm)
 open import Data.Product.Base using (-,_; proj₂)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
@@ -25,14 +26,13 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Function.Base using (_∘_; _⟨_⟩_)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
-open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Definitions using (_Respects_; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl ; cong; cong₂; _≢_)
+open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Relation.Nullary
 
-open PermutationReasoning
-
 private
   variable
     a b p : Level
@@ -172,6 +172,7 @@ shift v (x ∷ xs) ys = begin
   x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩
   x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
   v ∷ x ∷ xs ++ ys        ∎
+  where open PermutationReasoning
 
 drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
              ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
@@ -216,11 +217,13 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
       _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
       _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
       _ ∷ _ ∷ xs ++ _   ∎
+      where open PermutationReasoning
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
       _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
       _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
       _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
       _ ∷ _             ∎
+      where open PermutationReasoning
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl)
   drop-mid′ (trans p₁ p₂) ws  xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws))
   ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl)
@@ -245,6 +248,7 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
   x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
   x ∷ ys ++ xs   ↭⟨ shift x ys xs ⟨
   ys ++ (x ∷ xs) ∎
+  where open PermutationReasoning
 
 ++-isMagma : IsMagma {A = List A} _↭_ _++_
 ++-isMagma = record
@@ -300,6 +304,7 @@ shifts xs ys {zs} = begin
   (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
   (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
    ys ++ xs  ++ zs ∎
+   where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- _∷_
@@ -315,6 +320,7 @@ drop-∷ = drop-mid [] []
   xs ++ [ x ]   ↭⟨ shift x xs [] ⟩
   x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
   x ∷ xs        ∎)
+  where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- ʳ++
@@ -353,3 +359,17 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     (x ∷ xs) ++ y ∷ ys       ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
+
+------------------------------------------------------------------------
+-- product
+
+product-↭ : product Preserves _↭_ ⟶ _≡_
+product-↭ refl = refl
+product-↭ (prep x r) = cong (x *_) (product-↭ r)
+product-↭ (trans r s) = ≡.trans (product-↭ r) (product-↭ s)
+product-↭ (swap {xs} {ys} x y r) = begin
+  x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩
+  (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (product-↭ r) ⟩
+  (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
+  y * (x * product ys) ∎
+  where open ≡-Reasoning
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 683c7d8a87..1a491fdf93 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -8,6 +8,8 @@
 
 module Data.Nat.Primality where
 
+open import Data.List.Base using ([]; _∷_; product)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
@@ -294,6 +296,17 @@ prime⇒rough (prime pr) = pr
 rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p
 rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n)
 
+-- If a number n is m-rough, and m * m > n, then n must be prime.
+rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
+rough∧square>⇒prime rough m*m>n = prime ¬composite
+  where
+    ¬composite : ¬ Composite _
+    ¬composite (composite d<n d∣n) = contradiction (m∣n⇒n≡quotient*m d∣n)
+      (<⇒≢ (<-≤-trans m*m>n (*-mono-≤
+        (rough⇒≤ (rough∧∣⇒rough rough (quotient-∣ d∣n)))
+        (rough⇒≤ (rough∧∣⇒rough rough d∣n)))))
+      where instance _ = n>1⇒nonTrivial (quotient>1 d∣n d<n)
+
 -- Relationship between compositeness and primality.
 composite⇒¬prime : Composite n → ¬ Prime n
 composite⇒¬prime composite[d] (prime p) = p composite[d]
@@ -309,6 +322,16 @@ prime⇒¬composite (prime p) = p
 ¬prime⇒composite {n} ¬prime[n] =
   decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime)
 
+productOfPrimes≢0 : ∀ {as} → All Prime as → NonZero (product as)
+productOfPrimes≢0 pas = product≢0 (All.map prime⇒nonZero pas)
+  where
+  product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
+  product≢0 [] = _
+  product≢0 {n ∷ ns} (nzn ∷ nzns) = m*n≢0 n _ {{nzn}} {{product≢0 nzns}}
+
+productOfPrimes≥1 : ∀ {as} → All Prime as → product as ≥ 1
+productOfPrimes≥1 {as} pas = >-nonZero⁻¹ _ {{productOfPrimes≢0 pas}}
+
 ------------------------------------------------------------------------
 -- Basic (counter-)examples of Irreducible
 
diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
new file mode 100644
index 0000000000..fed89d7d45
--- /dev/null
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -0,0 +1,198 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Prime factorisation of natural numbers and its properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Primality.Factorisation where
+
+open import Data.Empty using (⊥-elim)
+open import Data.Nat.Base
+open import Data.Nat.Divisibility
+open import Data.Nat.Properties
+open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
+open import Data.Nat.Primality
+open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂)
+open import Data.List.Base using (List; []; _∷_; _++_; product)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (∈-∃++)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.List.Relation.Binary.Permutation.Propositional
+  using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_$_; _∘_; _|>_; flip)
+open import Induction using (build)
+open import Induction.Lexicographic using (_⊗_; [_⊗_])
+open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
+
+private
+  variable
+    n : ℕ
+    
+------------------------------------------------------------------------
+-- Core definition
+
+record PrimeFactorisation (n : ℕ) : Set where
+  field
+    factors : List ℕ
+    isFactorisation : n ≡ product factors
+    factorsPrime : All Prime factors
+
+open PrimeFactorisation public using (factors)
+open PrimeFactorisation
+
+------------------------------------------------------------------------
+-- Finding a factorisation
+
+primeFactorisation[1] : PrimeFactorisation 1
+primeFactorisation[1] = record
+  { factors = []
+  ; isFactorisation = refl
+  ; factorsPrime = []
+  }
+
+primeFactorisation[p] : Prime n → PrimeFactorisation n
+primeFactorisation[p] {n} pr = record
+  { factors = n ∷ []
+  ; isFactorisation = sym (*-identityʳ n)
+  ; factorsPrime = pr ∷ []
+  }
+
+-- This builds up three important things:
+-- * a proof that every number we've gotten to so far has increasingly higher
+--   possible least prime factor, so we don't have to repeat smaller factors
+--   over and over (this is the "m" and "rough" parameters)
+-- * a witness that this limit is getting closer to the number of interest, in a
+--   way that helps the termination checker (the "k" and "eq" parameters)
+-- * a proof that we can factorise any smaller number, which is useful when we
+--   encounter a factor, as we can then divide by that factor and continue from
+--   there without termination issues
+factorise : ∀ n → .{{NonZero n}} → PrimeFactorisation n
+factorise 1 = primeFactorisation[1]
+factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , suc n₀ ∸ 4) 2-rough refl
+  where
+  P : ℕ × ℕ → Set
+  P (n , k) = ∀ {m} → .{{NonTrivial n}} → .{{NonTrivial m}} → m Rough n → suc n ∸ m * m ≡ k → PrimeFactorisation n
+
+  facRec : ∀ n×k → (<-Rec ⊗ <-Rec) P n×k → P n×k
+  facRec (n , zero) _ rough eq =
+  -- Case 1: m * m > n, ∴ Prime n
+    primeFactorisation[p] (rough∧square>⇒prime rough (m∸n≡0⇒m≤n eq))
+  facRec (n@(2+ _) , suc k) (recFactor , recQuotient) {m@(2+ _)} rough eq with m ∣? n
+  -- Case 2: m ∤ n, try larger m, reducing k accordingly
+  ... | no m∤n = recFactor (≤-<-trans (m∸n≤m k (m + m)) (n<1+n k)) {suc m} (∤⇒rough-suc m∤n rough) $ begin
+    suc n ∸ (suc m + m * suc m)   ≡⟨ cong (λ # → suc n ∸ (suc m + #)) (*-suc m m) ⟩
+    suc n ∸ (suc m + (m + m * m)) ≡⟨ cong (suc n ∸_) (+-assoc (suc m) m (m * m)) ⟨
+    suc n ∸ (suc (m + m) + m * m) ≡⟨ cong (suc n ∸_) (+-comm (suc (m + m)) (m * m)) ⟩
+    suc n ∸ (m * m + suc (m + m)) ≡⟨ ∸-+-assoc (suc n) (m * m) (suc (m + m)) ⟨
+    (suc n ∸ m * m) ∸ suc (m + m) ≡⟨ cong (_∸ suc (m + m)) eq ⟩
+    suc k ∸ suc (m + m)           ∎
+    where open ≡-Reasoning
+  -- Case 3: m ∣ n, record m and recurse on the quotient
+  ... | yes m∣n = record
+    { factors = m ∷ ps
+    ; isFactorisation = sym m*Πps≡n
+    ; factorsPrime = rough∧∣⇒prime rough m∣n ∷ primes
+    }
+    where
+      m<n : m < n
+      m<n = begin-strict
+        m            <⟨ s≤s (≤-trans (m≤n+m m _) (+-monoʳ-≤ _ (m≤m+n m _))) ⟩
+        pred (m * m) <⟨ s<s⁻¹ (m∸n≢0⇒n<m λ eq′ → 0≢1+n (trans (sym eq′) eq)) ⟩
+        n            ∎
+        where open ≤-Reasoning
+        
+      q = quotient m∣n
+      
+      instance _  = n>1⇒nonTrivial (quotient>1 m∣n m<n)
+      
+      factorisation[q] : PrimeFactorisation q
+      factorisation[q] = recQuotient (quotient-< m∣n) (suc q ∸ m * m) (rough∧∣⇒rough rough (quotient-∣ m∣n)) refl
+      
+      ps = factors factorisation[q]
+      
+      primes = factorsPrime factorisation[q]
+      
+      m*Πps≡n : m * product ps ≡ n
+      m*Πps≡n = begin
+        m * product ps ≡⟨ cong (m *_) (isFactorisation factorisation[q]) ⟨
+        m * q          ≡⟨ m∣n⇒n≡m*quotient m∣n ⟨
+        n              ∎
+        where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of a factorisation
+
+factorisationHasAllPrimeFactors : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → p ∈ as
+factorisationHasAllPrimeFactors {[]} {2+ p} pPrime p∣Πas [] = contradiction (∣1⇒≡1 p∣Πas) λ ()
+factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime) with euclidsLemma a (product as) pPrime p∣aΠas
+... | inj₂ p∣Πas = there (factorisationHasAllPrimeFactors pPrime p∣Πas asPrime)
+... | inj₁ p∣a with prime⇒irreducible aPrime p∣a
+...   | inj₁ refl = contradiction pPrime ¬prime[1]
+...   | inj₂ refl = here refl
+
+private
+  factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs
+  factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl
+  factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) =
+    contradiction Πas≡Πbs (<⇒≢ Πas<Πbs)
+    where
+      Πas<Πbs : product [] < product (b ∷ bs)
+      Πas<Πbs = begin-strict
+        1                ≡⟨⟩
+        1 * 1            <⟨ *-monoˡ-< 1 {1} {b} sz<ss ⟩
+        b * 1            ≤⟨ *-monoʳ-≤ b (productOfPrimes≥1 prime[bs]) ⟩
+        b * product bs   ≡⟨⟩
+        product (b ∷ bs) ∎
+        where open ≤-Reasoning
+
+  factorisationUnique′ (a ∷ as) bs Πas≡Πbs (prime[a] ∷ prime[as]) prime[bs] = a∷as↭bs
+    where
+      a∣Πbs : a ∣ product bs
+      a∣Πbs = divides (product as) $ begin
+        product bs       ≡⟨ Πas≡Πbs ⟨
+        product (a ∷ as) ≡⟨⟩
+        a * product as   ≡⟨ *-comm a (product as) ⟩
+        product as * a   ∎
+        where open ≡-Reasoning
+
+      shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′
+      shuffle with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs])
+        = ys ++ zs , ↭-trans (↭-reflexive p) (shift a ys zs)
+
+      bs′ = proj₁ shuffle
+      bs↭a∷bs′ = proj₂ shuffle
+
+      Πas≡Πbs′ : product as ≡ product bs′
+      Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{prime⇒nonZero prime[a]}} $ begin
+        a * product as  ≡⟨ Πas≡Πbs ⟩
+        product bs      ≡⟨ product-↭ bs↭a∷bs′ ⟩
+        a * product bs′ ∎
+        where open ≡-Reasoning
+
+      prime[bs'] : All Prime bs′
+      prime[bs'] = All.tail (All-resp-↭ bs↭a∷bs′ prime[bs])
+
+      a∷as↭bs : a ∷ as ↭ bs
+      a∷as↭bs = begin
+        a ∷ as  <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs'] ⟩
+        a ∷ bs′ ↭⟨ bs↭a∷bs′ ⟨
+        bs      ∎
+        where open PermutationReasoning
+
+factorisationUnique : (f f′ : PrimeFactorisation n) → factors f ↭ factors f′
+factorisationUnique {n} f f′ =
+  factorisationUnique′ (factors f) (factors f′) Πf≡Πf′ (factorsPrime f) (factorsPrime f′)
+  where
+    Πf≡Πf′ : product (factors f) ≡ product (factors f′)
+    Πf≡Πf′ = begin
+      product (factors f)  ≡⟨ isFactorisation f ⟨
+      n                    ≡⟨ isFactorisation f′ ⟩
+      product (factors f′) ∎
+      where open ≡-Reasoning