diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 92ec778..834cca1 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,16 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14)
+
+* `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of
+  hyperpolymath/occupancy-types#11. The old pin was a commit on that PR's
+  branch, which was deleted at merge, so a fresh clone could no longer fetch
+  it (`fatal: reference is not a tree`) and the kernel-proofs gate could not
+  start. The two trees differ only in occupancy-types' own
+  `scripts/check-agda.sh`; the Agda sources this gate checks are identical.
+* `ResourceAlgebra/MinMax.idr`: a header comment loses a stray "and".
+
 ==== MinMax joins the grade kernel (2026-10-14)
 
 * New `ResourceAlgebra/MinMax.idr` transcribes resource-algebra
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
index 7c72800..5d5d3ea 100755
--- a/scripts/fetch-siblings.sh
+++ b/scripts/fetch-siblings.sh
@@ -22,7 +22,7 @@ set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}"
-OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-60134839efe2c6f51a31d977a72c1cf94457e71d}"
+OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-8f09c0bb319dee99d532e261cd5da4d04ace479a}"
 CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}"
 
 fetch() { # fetch <name> <commit>
diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr
index d3c9b8e..2258ad5 100644
--- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr
+++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MinMax.idr
@@ -20,7 +20,7 @@
 --   minMaxSeq = sequence     = MAX (the worst hop)       — the "⊗", unit Finite 0
 --   lossAlt   = alternatives = MIN (the better path)     — the "⊕", unit Infinity
 -- Infinity absorbs under sequence but is the identity for alternatives:
--- and an unreachable alternative is never chosen.
+-- an unreachable alternative is never chosen.
 --
 -- The carrier is shared with Loss ON PURPOSE (upstream Morphism.agda,
 -- `loss-bottleneck`: the identity on the carrier is a lax morphism Loss →