diff --git a/Tests/Host.lean b/Tests/Host.lean
index 0bb1e43e..afc1051b 100644
--- a/Tests/Host.lean
+++ b/Tests/Host.lean
@@ -19,15 +19,17 @@ here, since the rule never reads it.
 Unit 1b runs hosts over the sim transport, with the real
 `Noise.securityProtocol` and `Mux.yamux` values (PRINCIPLES 1.4). Every
 host derives its peer id through `libp2p/identity`, and the upgrade runs
-through `libp2p/negotiate`, so the legs wait for W5.3, W5.4, and W5.5
-to merge. Until then the suite names each leg as a skip.
+through `libp2p/negotiate`. The real packages have landed (#53, #76,
+#77), and the upgrade still runs through the negotiate mock of the
+host, whose entries fail. The legs wait for the host swap of issue
+#70. Until then the suite names each leg as a skip.
 -/
 
 set_option autoImplicit false
 
 namespace Tests
 
-open Conc Multiformats Libp2p.Identity Libp2p.Host.Mock.Core Libp2p.Host
+open Conc Multiformats Libp2p.Identity Libp2p.Core Libp2p.Host
 
 /-! ## Helpers -/
 
@@ -298,6 +300,6 @@ def Host.run (r : Runner) : IO Unit := do
   (peerstoreChecks r).run
   errorChecks r
   for leg in swarmLegs do
-    r.skip s!"host: {leg}" "needs W5.3, W5.4, and W5.5 merged"
+    r.skip s!"host: {leg}" "needs the negotiate swap of the host, issue #70"
 
 end Tests
diff --git a/packages/libp2p/host/Libp2p/Host/Dedup.lean b/packages/libp2p/host/Libp2p/Host/Dedup.lean
index 6a88bce4..57e86bd8 100644
--- a/packages/libp2p/host/Libp2p/Host/Dedup.lean
+++ b/packages/libp2p/host/Libp2p/Host/Dedup.lean
@@ -1,5 +1,5 @@
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 import Libp2p.Host.Constants
 import Libp2p.Host.Registry
 
@@ -46,7 +46,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
-open Libp2p.Identity Libp2p.Host.Mock.Core
+open Libp2p.Identity Libp2p.Core
 
 /-- The order of two peer ids by their binary form, byte by byte
 (module doc, "The order on peer ids"). -/
diff --git a/packages/libp2p/host/Libp2p/Host/Error.lean b/packages/libp2p/host/Libp2p/Host/Error.lean
index 854042d6..8eb88b5d 100644
--- a/packages/libp2p/host/Libp2p/Host/Error.lean
+++ b/packages/libp2p/host/Libp2p/Host/Error.lean
@@ -1,6 +1,6 @@
 import Multiformats
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core.Error
 
 /-!
 # `Host.Error`
@@ -20,9 +20,9 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
--- The mock of the unmerged core (RULES.md, "Working ahead of the
--- tree"); `Core.Error` resolves through `Libp2p.Host.Mock`.
-open Multiformats Libp2p.Host.Mock Libp2p.Identity
+-- `Core.Error` resolves to `Libp2p.Core.Error` through the parent
+-- namespace `Libp2p`.
+open Multiformats Libp2p.Identity
 
 /-- The policy checkpoint that refused a connection (§3.4: a closed
 set). The gater answers at the first three (`Core.ConnectionGater`),
diff --git a/packages/libp2p/host/Libp2p/Host/Mock/Core.lean b/packages/libp2p/host/Libp2p/Host/Mock/Core.lean
deleted file mode 100644
index 6678d411..00000000
--- a/packages/libp2p/host/Libp2p/Host/Mock/Core.lean
+++ /dev/null
@@ -1,176 +0,0 @@
-import Conc
-import Streams
-import Libp2p.Identity
-
-/-!
-# Mock: the surface of `libp2p/core` that the host uses
-
-W5.2 (`libp2p/core`) has not merged, so the host builds against a mock
-of its frozen surface (RULES.md, "Working ahead of the tree"). The
-types are copies: the seam shapes of the core ARCHITECTURE, "Public
-surface", with `MuxSession.openStream` carrying a `ProtocolId` (the mux
-ARCHITECTURE, "Public surface"). The mock imports nothing from the real
-package, and it states no axiom.
-
-## The policy shapes
-
-The core ARCHITECTURE fixes the three policy hooks and no signatures:
-"the decision inputs beyond these are the seam's to refine as the host
-lands (W5.6)". This unit fixes them, and the core ARCHITECTURE records
-them. The peer of an inbound connection is unknown until the handshake
-ends, so the gater and the resource manager each take a second decision
-there, with the proved peer, as go-libp2p does:
-`ConnectionGater.InterceptSecured` (`vendor/go-libp2p/core/connmgr/gater.go`)
-and `ResourceScope.SetPeer` (`vendor/go-libp2p/core/network/rcmgr.go`).
-The ranker answers a dial schedule, an address and a delay each, the
-shape of go-libp2p's `AddrDelay` and `DialRanker`
-(`vendor/go-libp2p/core/network/network.go`, lines 212 and 218).
-
-A policy answer runs in `BaseIO`: it has no fault channel, so a policy
-throw cannot lose a dial.
-
-At the integration, the host imports `Libp2p.Core`, and the module goes.
--/
-
-set_option autoImplicit false
-
-namespace Libp2p.Host.Mock.Core
-
-open Conc Streams Multiformats Libp2p.Identity
-
-/-- A protocol id, wrapped (§3.4). -/
-structure ProtocolId where
-  /-- The id text. -/
-  toString : String
-  deriving DecidableEq, Hashable, Ord, Repr
-
-instance : ToString ProtocolId := ⟨ProtocolId.toString⟩
-
-/-- The coarse error every seam returns (§4.9). Each arm carries the
-rendered error of the implementation. -/
-inductive Error where
-  | protocol (detail : String)
-  | authentication (detail : String)
-  | timeout (detail : String)
-  | closed (detail : String)
-  deriving DecidableEq, Repr
-
-/-- The log line of the error: the kind, then the rendered detail. -/
-def Error.render : Error → String
-  | .protocol d => s!"protocol error: {d}"
-  | .authentication d => s!"authentication failure: {d}"
-  | .timeout d => s!"timeout: {d}"
-  | .closed d => s!"closed: {d}"
-
-instance : ToString Error := ⟨Error.render⟩
-
-/-- Our side of a connection (§4.9). -/
-inductive Role where
-  | initiator
-  | responder
-  deriving DecidableEq, Repr
-
-/-- The connection after the handshake: the secure connection, the two
-peer ids, the bytes the handshake read past its end, and the
-completion of its tasks. -/
-structure SecureConn extends Connection where
-  /-- Our peer id. -/
-  localPeer : PeerId
-  /-- The peer id the handshake proved. -/
-  remotePeer : PeerId
-  /-- The bytes the handshake read past its end (§4.7). -/
-  leftover : ByteArray
-  /-- Wait until the secure connection's tasks end. -/
-  join : ExceptT Error Async Unit
-
-/-- The security seam. -/
-structure SecurityProtocol where
-  /-- The negotiated id. -/
-  id : ProtocolId
-  /-- Run the handshake over a connection, with the negotiation's
-  leftover. -/
-  handshake : Role → Connection → ByteArray → ExceptT Error Async SecureConn
-
-/-- A muxer session. -/
-structure MuxSession where
-  /-- Open a stream, labeled with its protocol id. -/
-  openStream : ProtocolId → ExceptT Error Async Stream
-  /-- The next stream the peer opened; `none` once the session ends. -/
-  accept : Async (Option Stream)
-  /-- End the session. -/
-  close : IO Unit
-  /-- Wait until the session loop ends. -/
-  join : ExceptT Error Async Unit
-
-/-- The muxer seam. -/
-structure Muxer where
-  /-- The negotiated id. -/
-  id : ProtocolId
-  /-- Open a session over a secure connection, with the negotiation's
-  leftover. -/
-  «open» : Role → Connection → ByteArray → ExceptT Error Async MuxSession
-
-/-- What the host knows about the connection under a served stream. -/
-structure StreamContext where
-  /-- The peer id the security handshake proved. -/
-  remotePeer : PeerId
-  /-- The peer's transport address, as the connection reports it. -/
-  remoteAddr : Multiaddr
-
-/-- The callback a served stream reaches. -/
-structure StreamHandler where
-  /-- The id the handler serves. -/
-  id : ProtocolId
-  /-- Serve one stream of the connection that `StreamContext`
-  describes. -/
-  handle : StreamContext → Stream → ExceptT Error Async Unit
-
-/-! ## The policy hooks (module doc, "The policy shapes") -/
-
-/-- The connection gater. `true` allows. -/
-structure ConnectionGater where
-  /-- Before an outbound dial, by the expected peer and the address. -/
-  allowDial : Option PeerId → Multiaddr → BaseIO Bool
-  /-- After an accept, before any byte moves, by the two addresses. -/
-  allowInbound : (localAddr remoteAddr : Multiaddr) → BaseIO Bool
-  /-- After the handshake, before the muxer stage, by the proved peer. -/
-  allowSecured : Role → PeerId → (localAddr remoteAddr : Multiaddr) → BaseIO Bool
-
-/-- An admitted share of a limit. A second `release` does nothing. -/
-structure Reservation where
-  /-- Return the share. -/
-  release : BaseIO Unit
-
-/-- The resource scope of one admitted connection. -/
-structure ConnectionScope where
-  /-- Name the proved peer; `false` when the connection does not fit
-  that peer's limits. -/
-  setPeer : PeerId → BaseIO Bool
-  /-- Admit one more stream; `none` when it does not fit. -/
-  reserveStream : BaseIO (Option Reservation)
-  /-- Admit this many more buffered bytes; `none` when they do not fit. -/
-  reserveMemory : Nat → BaseIO (Option Reservation)
-  /-- Return the connection's share and every share it still holds. -/
-  release : BaseIO Unit
-
-/-- The resource manager. -/
-structure ResourceManager where
-  /-- Admit a new connection, by its direction, the expected peer, and
-  the remote address; `none` when it does not fit. -/
-  openConnection : Role → Option PeerId → Multiaddr → BaseIO (Option ConnectionScope)
-
-/-- One address of a dial schedule, with its delay from the start of
-the dial, in milliseconds. -/
-structure AddrDelay where
-  /-- The address to dial. -/
-  addr : Multiaddr
-  /-- The wait before this dial. -/
-  delayMs : Nat
-  deriving DecidableEq, Repr
-
-/-- The address ranker: the dial schedule of a peer's addresses. -/
-structure AddressRanker where
-  /-- The schedule, in dial order. -/
-  rank : List Multiaddr → List AddrDelay
-
-end Libp2p.Host.Mock.Core
diff --git a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
index a399021b..b5d1bf2b 100644
--- a/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
+++ b/packages/libp2p/host/Libp2p/Host/Mock/Negotiate.lean
@@ -1,24 +1,26 @@
 import Conc
 import Streams
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 
 /-!
 # Mock: the surface of `libp2p/negotiate` that the host uses
 
-W5.5 (`libp2p/negotiate`) has not merged, so the host builds against a
-mock (RULES.md, "Working ahead of the tree"). The mock imports nothing
-from the real package, and it states no axiom. Both entries fail with
-the name of the package: no body negotiates, runs a handshake, or opens
-a session.
+The merged `libp2p/negotiate` takes the seam types of `Libp2p.Core`
+(issue #53), so this mock carries those types too. The mock stays
+until the host swap of issue #70 lands (RULES.md, "Working ahead of
+the tree"). It imports nothing from the negotiate package, and it
+states no axiom. Both entries fail with the name of the package: no
+body negotiates, runs a handshake, or opens a session.
 
-The negotiate ARCHITECTURE freezes `Negotiate.upgrade`. The host needs
-two calls beside it, and the negotiate ARCHITECTURE gains both in this
-unit:
+The host needs two calls beside `Negotiate.upgrade`. The merged
+package has neither, so the swap retypes the host's use of them
+(issue #70):
 
 * `upgradeWith`, the upgrade with a checkpoint after the handshake and
   before the muxer stage. The host's gater and resource manager decide
-  there, by the proved peer (the core mock, "The policy shapes"); go's
+  there, by the proved peer (the core ARCHITECTURE, "The policy
+  shapes"); go's
   upgrader calls `InterceptSecured` at the same place
   (`vendor/go-libp2p/p2p/net/upgrader/upgrader.go`, line 176). A refusal is a
   value, `UpgradeResult.refused`, and no `Core.Error` arm (§3.5).
@@ -26,16 +28,13 @@ unit:
   serves each inbound stream through it, and `newStream` negotiates
   each outbound one. The bytes it reads past the selecting message go
   to the stream's front (§4.7, `Stream.prependBytes`).
-
-At the integration, the host imports `Libp2p.Negotiate`, and the module
-goes.
 -/
 
 set_option autoImplicit false
 
 namespace Libp2p.Host.Mock.Negotiate
 
-open Conc Streams Libp2p.Identity Libp2p.Host.Mock.Core
+open Conc Streams Libp2p.Identity Libp2p.Core
 
 /-- How a stream negotiation failed. The host reads two arms: the end of
 the stream before a selection, an orderly end, and the empty proposal
diff --git a/packages/libp2p/host/Libp2p/Host/Policy.lean b/packages/libp2p/host/Libp2p/Host/Policy.lean
index 16665b84..b2a0e513 100644
--- a/packages/libp2p/host/Libp2p/Host/Policy.lean
+++ b/packages/libp2p/host/Libp2p/Host/Policy.lean
@@ -1,4 +1,4 @@
-import Libp2p.Host.Mock.Core
+import Libp2p.Core.Policy
 
 /-!
 # The policy values
@@ -17,7 +17,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host.Policy
 
-open Libp2p.Host.Mock.Core
+open Libp2p.Core
 
 /-- The default gater: it allows every dial, every inbound connection,
 and every proved peer. -/
diff --git a/packages/libp2p/host/Libp2p/Host/Registry.lean b/packages/libp2p/host/Libp2p/Host/Registry.lean
index 5954fdb3..935cf7dc 100644
--- a/packages/libp2p/host/Libp2p/Host/Registry.lean
+++ b/packages/libp2p/host/Libp2p/Host/Registry.lean
@@ -1,6 +1,6 @@
 import Std.Data.HashMap
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 
 /-!
 # The session and handler registries
@@ -44,7 +44,7 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
-open Libp2p.Identity Libp2p.Host.Mock.Core
+open Libp2p.Identity Libp2p.Core
 
 /-! ## The session table -/
 
diff --git a/packages/libp2p/host/Libp2p/Host/Swarm.lean b/packages/libp2p/host/Libp2p/Host/Swarm.lean
index 2294d866..54ffc2ea 100644
--- a/packages/libp2p/host/Libp2p/Host/Swarm.lean
+++ b/packages/libp2p/host/Libp2p/Host/Swarm.lean
@@ -2,7 +2,7 @@ import Std.Data.HashMap
 import Conc
 import Streams
 import Libp2p.Identity
-import Libp2p.Host.Mock.Core
+import Libp2p.Core
 import Libp2p.Host.Mock.Negotiate
 import Libp2p.Host.Error
 import Libp2p.Host.Registry
@@ -69,10 +69,10 @@ set_option autoImplicit false
 
 namespace Libp2p.Host
 
--- The mocks of the unmerged packages (RULES.md, "Working ahead of the
--- tree"); `Negotiate.Error` resolves through `Libp2p.Host.Mock`.
+-- The negotiate mock stays until the host swap of issue #70;
+-- `Negotiate.Error` resolves through `Libp2p.Host.Mock`.
 open Conc Streams Multiformats Libp2p.Host.Mock Libp2p.Identity
-  Libp2p.Host.Mock.Core Libp2p.Host.Mock.Negotiate
+  Libp2p.Core Libp2p.Host.Mock.Negotiate
 
 /-- A failure of a task that no caller awaits: an inbound upgrade, a
 session that ended badly, an inbound stream. -/
diff --git a/packages/libp2p/host/docs/ARCHITECTURE.md b/packages/libp2p/host/docs/ARCHITECTURE.md
index 93db8fb6..10b82a98 100644
--- a/packages/libp2p/host/docs/ARCHITECTURE.md
+++ b/packages/libp2p/host/docs/ARCHITECTURE.md
@@ -24,7 +24,7 @@ libp2p group is §7, row 10).
 | `Libp2p/Host/Swarm.lean` | `Config`, the `Host` state, `dial`, `dialPeer`, `startListening`, `newStream`, the accept loop, the upgrade pipeline, and stream serving |
 | `Libp2p/Host/Shutdown.lean` | `Host.close`, the §5.5 sequence |
 | `Libp2p/Host/Policy.lean` | the permissive default gater, and the permissive and denying test doubles the core pair assigned here; the default resource manager (admits everything) and the default ranker (keeps the order, no delay) |
-| `Libp2p/Host/Mock/{Core,Negotiate}.lean` | the mocks of W5.2 and W5.5 until they merge (see "The mocks") |
+| `Libp2p/Host/Mock/Negotiate.lean` | the mock of the W5.5 surface the host calls, until the host swap of issue #70 (see "The mock") |
 
 All declarations live in the `Libp2p.Host` namespace, and the root
 module re-exports the public submodules.
@@ -298,22 +298,22 @@ fixes them as follows.
   1b milestone. A fault of a joined task does not stop the sequence,
   and `close` throws the first fault at the end.
 
-## The mocks
+## The mock
 
-W5.2 (`libp2p/core`) and W5.5 (`libp2p/negotiate`) have not merged,
-so the package builds against mocks of their frozen surfaces (RULES.md,
-"Working ahead of the tree"), under `Libp2p/Host/Mock/`. A type is a
-copy of the frozen shape; an operation is `opaque`, and its body fails
-with the name of the missing package. No body negotiates or opens a
-session, and the mocks state no axiom. The host modules open
-`Libp2p.Host.Mock`, so `Core.Error` and `Negotiate.upgradeWith` resolve
-as they will against the real packages, and the integration swaps the
-imports and drops the `open`. The keys and the peer id come from the
-merged `libp2p/identity`.
+The seam types come from `libp2p/core`. `libp2p/negotiate` takes the
+real core too (issue #53), so its upgrader takes the values the host
+holds. The host keeps a mock of the negotiate surface,
+`Libp2p/Host/Mock/Negotiate.lean`, until the host swap of issue #70.
+Its operations are `opaque`, and each body fails with the name of the
+package; it states no axiom. Swarm opens `Libp2p.Host.Mock`, so
+`Negotiate.upgradeWith` resolves as it will against the real package.
+The swap (issue #70) is a retype: the merged upgrader takes no `admit`
+checkpoint and exports no `negotiateStream`.
 
-Every upgrade runs through the negotiate mock and fails there, and the
-legs also need the Noise and yamux values (W5.3, W5.4), so the unit 1b
-milestones run at the integration. Unit 1a runs in full.
+Every upgrade runs through the negotiate mock and fails there, so the
+unit 1b milestones run after the host swap of issue #70. The Noise and
+yamux values are on the real core (issues #76 and #77). Unit 1a runs
+in full.
 
 ## What the package must not depend on
 
diff --git a/packages/libp2p/host/docs/PLAN.md b/packages/libp2p/host/docs/PLAN.md
index 647da5dd..c058f57c 100644
--- a/packages/libp2p/host/docs/PLAN.md
+++ b/packages/libp2p/host/docs/PLAN.md
@@ -24,9 +24,9 @@ so unit 1a lands while the upgrader finishes. W5.2 sits outside the
 root row and reaches this unit through the root chain, which finishes
 it before W5.5.
 
-Units 0 and 1a are done, and unit 1b's code builds against the mocks
-of W5.2 and W5.5 (the package ARCHITECTURE, "The mocks"), with the
-merged `libp2p/identity`. The suite is `Tests/Host.lean`; the dedup
+Units 0 and 1a are done. Unit 1b's code builds over `libp2p/core`
+and `libp2p/identity`, and against a mock of W5.5 (the package
+ARCHITECTURE, "The mock"). The suite is `Tests/Host.lean`; the dedup
 rule also carries theorems in `Libp2p/Host/Dedup.lean`. A host
 upgrades through `libp2p/negotiate`, so the unit 1b milestones run at
 the integration, and the suite names each one as a skip until then. Unit 1b needs two