diff --git a/Cargo.toml b/Cargo.toml
index dea21ed..7ce42d3 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "open-hypergraphs"
-version = "0.3.1"
+version = "0.3.2"
 edition = "2021"
 description = "Data-Parallel Algorithms for Open Hypergraphs"
 license = "MIT OR Apache-2.0"
diff --git a/src/lax/cycle.rs b/src/lax/cycle.rs
new file mode 100644
index 0000000..589da45
--- /dev/null
+++ b/src/lax/cycle.rs
@@ -0,0 +1,287 @@
+//! Fast cycle-breaking heuristics for lax open hypergraphs.
+
+use super::{NodeId, OpenHypergraph};
+use std::cmp::Reverse;
+use std::collections::{BinaryHeap, VecDeque};
+
+/// Choose nodes whose spiderization is guaranteed to break every directed
+/// cycle.
+///
+/// This computes a greedy directed feedback vertex set on the bipartite
+/// incidence graph
+///
+/// ```text
+/// node -> operation -> node.
+/// ```
+///
+/// Basic idea:
+///
+/// - Construct a bipartite node-operation incidence graph.
+/// - Vertices with indegree zero or outdegree zero cannot participate in a cycle.
+/// - Repeatedly peel those vertices until no more acyclic fringe can be removed.
+/// - Select the remaining wire node with the largest `indegree * outdegree`
+///   score, remove it, and repeat.
+///
+/// Selecting high-degree nodes in this way tends to break several cycles at once.
+///
+/// The result is deterministic and is guaranteed to make
+/// `f.clone().spiderize_nodes(&result)` acyclic. It is a heuristic: the
+/// returned set need not have minimum size.
+///
+/// Returns [`None`] if `f` has pending node identifications. Quotienting can
+/// create cycles, so cycle breaking must operate on the semantic, quotiented
+/// graph. When successful, the returned IDs refer directly to `f`.
+#[must_use]
+pub fn cycle_breaking_nodes<O, A>(f: &OpenHypergraph<O, A>) -> Option<Vec<NodeId>> {
+    if !f.hypergraph.is_strict() {
+        return None;
+    }
+
+    assert_eq!(
+        f.hypergraph.edges.len(),
+        f.hypergraph.adjacency.len(),
+        "malformed hypergraph: edges and adjacency lengths differ"
+    );
+
+    let node_count = f.hypergraph.nodes.len();
+
+    // Allocate a bipartite incidence graph.
+    // Nodes occupy 0..node_count, followed by one vertex for each operation.
+    // Keeping operation vertices avoids expanding an m -> n hyperedge into m*n arcs.
+    let vertex_count = node_count + f.hypergraph.adjacency.len();
+    let mut outgoing = vec![Vec::new(); vertex_count];
+    let mut incoming = vec![Vec::new(); vertex_count];
+
+    // Populate the incidence graph.
+    // Preserve the hypergraph's direction: every source node points to its
+    // operation, and that operation points to each target node.
+    for (operation, adjacency) in f.hypergraph.adjacency.iter().enumerate() {
+        let operation = node_count + operation;
+
+        for source in &adjacency.sources {
+            add_arc(source.0, operation, &mut outgoing, &mut incoming);
+        }
+        for target in &adjacency.targets {
+            add_arc(operation, target.0, &mut outgoing, &mut incoming);
+        }
+    }
+
+    // Only node vertices are selectable; operation vertices may be peeled but
+    // never returned.
+    let selected = greedy_feedback_nodes(node_count, &outgoing, &incoming);
+
+    Some(selected.into_iter().map(NodeId).collect())
+}
+
+/// Add one directed arc to both forward and reverse adjacency lists.
+///
+/// Keeping both directions lets vertex removal update neighboring in- and
+/// out-degrees without searching the whole graph.
+fn add_arc(source: usize, target: usize, outgoing: &mut [Vec<usize>], incoming: &mut [Vec<usize>]) {
+    outgoing[source].push(target);
+    incoming[target].push(source);
+}
+
+////////////////////////////////////////////////////////////////////////////////
+// Cycle breaking logic
+
+/// Greedily select wire vertices that hit every directed cycle.
+///
+/// Vertices `0..selectable_count` are wire nodes and may be selected; the
+/// remaining vertices are operations. Sources and sinks are peeled, then the
+/// highest-scoring wire vertex is selected whenever cyclic structure remains.
+///
+/// Runs in roughly `O((vertices + arcs) log(selectable vertices))` time.
+fn greedy_feedback_nodes(
+    selectable_count: usize,
+    outgoing: &[Vec<usize>],
+    incoming: &[Vec<usize>],
+) -> Vec<usize> {
+    debug_assert_eq!(outgoing.len(), incoming.len());
+
+    // Degrees and `active` describe the current residual graph. Every vertex
+    // is removed exactly once, either freely or as a selected cycle breaker.
+    let vertex_count = outgoing.len();
+    let mut active = vec![true; vertex_count];
+    let mut active_count = vertex_count;
+    let mut indegree: Vec<usize> = incoming.iter().map(Vec::len).collect();
+    let mut outdegree: Vec<usize> = outgoing.iter().map(Vec::len).collect();
+    let mut peel = VecDeque::new();
+    let mut candidates = BinaryHeap::new();
+    let mut selected = Vec::new();
+
+    // Seed both worklists: immediately peelable vertices go in the FIFO queue,
+    // while selectable vertices with two-sided connectivity go in the heap.
+    for vertex in 0..vertex_count {
+        if indegree[vertex] == 0 || outdegree[vertex] == 0 {
+            peel.push_back(vertex);
+        }
+        push_candidate(
+            vertex,
+            selectable_count,
+            &active,
+            &indegree,
+            &outdegree,
+            &mut candidates,
+        );
+    }
+
+    while active_count > 0 {
+        // Exhaust all consequences of previous removals before choosing
+        // another feedback node. This prevents selecting vertices already
+        // proven not to participate in the residual cycles.
+        while let Some(vertex) = peel.pop_front() {
+            if !active[vertex] || (indegree[vertex] > 0 && outdegree[vertex] > 0) {
+                continue;
+            }
+            remove_vertex(
+                vertex,
+                selectable_count,
+                outgoing,
+                incoming,
+                &mut active,
+                &mut indegree,
+                &mut outdegree,
+                &mut peel,
+                &mut candidates,
+            );
+            active_count -= 1;
+        }
+
+        if active_count == 0 {
+            break;
+        }
+
+        // Peeling got stuck, so the residual graph is cyclic. Pop until the
+        // degree snapshot agrees with current state, skipping lazy stale
+        // entries, then choose the best-scoring node.
+        let vertex = loop {
+            let (_, Reverse(vertex), candidate_indegree, candidate_outdegree) = candidates
+                .pop()
+                .expect("cyclic residual incidence graph must contain a selectable node");
+            if active[vertex]
+                && indegree[vertex] == candidate_indegree
+                && outdegree[vertex] == candidate_outdegree
+            {
+                break vertex;
+            }
+        };
+
+        // This is the only non-free removal: record it for spiderization.
+        // Removing it may expose a large acyclic fringe for the next peel.
+        selected.push(vertex);
+        remove_vertex(
+            vertex,
+            selectable_count,
+            outgoing,
+            incoming,
+            &mut active,
+            &mut indegree,
+            &mut outdegree,
+            &mut peel,
+            &mut candidates,
+        );
+        active_count -= 1;
+    }
+
+    // Heap choice order is an implementation detail; node order is a more
+    // stable and convenient public result.
+    selected.sort_unstable();
+    selected
+}
+
+/// Estimate how much cyclic connectivity removing a node will disrupt.
+///
+/// A node with many incoming and outgoing arcs joins many possible paths. The
+/// saturating product avoids overflow for unusually large incidence graphs.
+fn score(indegree: usize, outdegree: usize) -> usize {
+    indegree.saturating_mul(outdegree)
+}
+
+/// A lazily validated heap entry.
+///
+/// Entries contain `(score, node, indegree, outdegree)`. [`Reverse`] makes the
+/// lower node index win deterministic ties in the max-heap. The degree
+/// snapshots let us recognize entries made stale by later removals.
+type Candidate = (usize, Reverse<usize>, usize, usize);
+
+/// Add a selectable vertex's current state to the candidate heap.
+///
+/// The heap is deliberately lazy: degree changes push new entries rather than
+/// locating and updating old ones. Stale entries are discarded when popped.
+fn push_candidate(
+    node: usize,
+    selectable_count: usize,
+    active: &[bool],
+    indegree: &[usize],
+    outdegree: &[usize],
+    candidates: &mut BinaryHeap<Candidate>,
+) {
+    if node < selectable_count && active[node] && indegree[node] > 0 && outdegree[node] > 0 {
+        candidates.push((
+            score(indegree[node], outdegree[node]),
+            Reverse(node),
+            indegree[node],
+            outdegree[node],
+        ));
+    }
+}
+
+/// Remove a vertex from the active graph and update its neighbors.
+///
+/// Removing outgoing arcs lowers target in-degrees; removing incoming arcs
+/// lowers source out-degrees. Neighbors that become sources or sinks enter the
+/// free peeling queue, while still-cyclic node vertices receive refreshed heap
+/// entries.
+#[allow(clippy::too_many_arguments)]
+fn remove_vertex(
+    vertex: usize,
+    selectable_count: usize,
+    outgoing: &[Vec<usize>],
+    incoming: &[Vec<usize>],
+    active: &mut [bool],
+    indegree: &mut [usize],
+    outdegree: &mut [usize],
+    peel: &mut VecDeque<usize>,
+    candidates: &mut BinaryHeap<Candidate>,
+) {
+    // Mark first so a self-arc, if one is ever supplied, cannot update the
+    // removed vertex's own degree.
+    active[vertex] = false;
+
+    // Delete vertex -> target arcs.
+    for &target in &outgoing[vertex] {
+        if active[target] {
+            indegree[target] -= 1;
+            if indegree[target] == 0 || outdegree[target] == 0 {
+                peel.push_back(target);
+            }
+            push_candidate(
+                target,
+                selectable_count,
+                active,
+                indegree,
+                outdegree,
+                candidates,
+            );
+        }
+    }
+
+    // Delete source -> vertex arcs.
+    for &source in &incoming[vertex] {
+        if active[source] {
+            outdegree[source] -= 1;
+            if indegree[source] == 0 || outdegree[source] == 0 {
+                peel.push_back(source);
+            }
+            push_candidate(
+                source,
+                selectable_count,
+                active,
+                indegree,
+                outdegree,
+                candidates,
+            );
+        }
+    }
+}
diff --git a/src/lax/mod.rs b/src/lax/mod.rs
index 4cf746c..e4815fe 100644
--- a/src/lax/mod.rs
+++ b/src/lax/mod.rs
@@ -72,14 +72,18 @@
 //! connected nodes, e.g., x0 and y0. this allows both *checking* (of e.g. equality) and
 //! *inference*: inequal types might be *unified* into a single type.
 pub mod category;
+pub mod cycle;
 pub mod functor;
 pub mod hypergraph;
 pub mod mut_category;
 pub mod open_hypergraph;
+pub mod spider;
 
 pub use crate::category::*;
+pub use cycle::*;
 pub use hypergraph::*;
 pub use open_hypergraph::*;
+pub use spider::*;
 
 pub mod optic;
 pub mod var;
diff --git a/src/lax/spider.rs b/src/lax/spider.rs
new file mode 100644
index 0000000..8ee8f8e
--- /dev/null
+++ b/src/lax/spider.rs
@@ -0,0 +1,201 @@
+//! Make the Frobenius structure of an open hypergraph explicit.
+
+use super::{Hyperedge, NodeId, OpenHypergraph};
+use crate::strict::vec::FiniteFunction;
+
+/// An operation from `A`, or an explicitly represented spider.
+///
+/// A spider's arity is determined by its corresponding [`Hyperedge`].
+#[derive(Debug, Clone, PartialEq, Eq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+pub enum WithSpider<A> {
+    Operation(A),
+    Spider,
+}
+
+impl<O: Clone + PartialEq, A: Clone> OpenHypergraph<O, A> {
+    /// Replace implicit wiring with explicit spider operations.
+    ///
+    /// The result is strict (has no pending quotient), monogamous, and
+    /// acyclic. Each original operation is retained as
+    /// [`WithSpider::Operation`].
+    ///
+    /// For every original node, the construction inserts two spiders:
+    ///
+    /// - `p -> 1 + m` on the left, where `p` is the number of global source
+    ///   occurrences and `m` is the number of operation-source occurrences;
+    /// - `1 + n -> q` on the right, where `n` is the number of
+    ///   operation-target occurrences and `q` is the number of global target
+    ///   occurrences.
+    ///
+    /// The extra leg connects the two spiders. Every other occurrence gets a
+    /// distinct node, making every node occur exactly once as a source and
+    /// exactly once as a target (counting the global interfaces).
+    ///
+    /// Pending identifications in the lax quotient are applied first. An error
+    /// means that the quotient attempted to identify nodes with different
+    /// labels; the returned finite function is the quotient witness, as for
+    /// [`OpenHypergraph::quotient`].
+    pub fn spiderize(self) -> Result<OpenHypergraph<O, WithSpider<A>>, FiniteFunction> {
+        let nodes: Vec<NodeId> = (0..self.hypergraph.nodes.len()).map(NodeId).collect();
+        self.spiderize_nodes(&nodes)
+    }
+
+    /// Replace the chosen nodes' implicit wiring with explicit spider
+    /// operations.
+    ///
+    /// Each selected node is replaced by the same pair of spiders used by
+    /// [`Self::spiderize`]. Unselected nodes retain their implicit wiring.
+    /// Consequently, unlike [`Self::spiderize`], this operation does not by
+    /// itself guarantee that the result is acyclic or monogamous.
+    ///
+    /// `nodes` contains IDs from the input hypergraph. Pending identifications
+    /// are applied first, and IDs in `nodes` are mapped through the resulting
+    /// quotient. Selecting any representative therefore selects its complete
+    /// equivalence class. Duplicate selections are ignored.
+    ///
+    /// # Panics
+    ///
+    /// Panics if a selected node ID is out of bounds.
+    pub fn spiderize_nodes(
+        mut self,
+        nodes: &[NodeId],
+    ) -> Result<OpenHypergraph<O, WithSpider<A>>, FiniteFunction> {
+        let input_node_count = self.hypergraph.nodes.len();
+        for node in nodes {
+            assert!(
+                node.0 < input_node_count,
+                "node id {:?} is out of bounds",
+                node
+            );
+        }
+
+        // Quotient the input if necessary and remap the selected node IDs.
+        let remapped_nodes;
+        let nodes = if self.hypergraph.is_strict() {
+            nodes
+        } else {
+            let quotient = self.quotient()?;
+            remapped_nodes = nodes
+                .iter()
+                .map(|node| NodeId(quotient.table[node.0]))
+                .collect::<Vec<_>>();
+            remapped_nodes.as_slice()
+        };
+
+        assert_eq!(
+            self.hypergraph.edges.len(),
+            self.hypergraph.adjacency.len(),
+            "malformed hypergraph: edges and adjacency lengths differ"
+        );
+
+        // Split selected-node occurrences and record the spiders that reconnect them.
+        let spiders = rewrite_occurrences(
+            nodes,
+            &mut self.hypergraph.nodes,
+            &mut self.hypergraph.adjacency,
+            &mut self.sources,
+            &mut self.targets,
+        );
+
+        // Reuse the input graph, wrapping its existing operation labels.
+        let mut result = self.map_edges(WithSpider::Operation);
+
+        // Append the two explicit operations for each selected node.
+        for (left_spider, right_spider) in spiders {
+            result.new_edge(WithSpider::Spider, left_spider);
+            result.new_edge(WithSpider::Spider, right_spider);
+        }
+
+        Ok(result)
+    }
+}
+
+/// Append a fresh occurrence of `node`, carrying the same label.
+fn new_occurrence<O: Clone>(nodes: &mut Vec<O>, node: NodeId) -> NodeId {
+    let occurrence = NodeId(nodes.len());
+    nodes.push(nodes[node.0].clone());
+    occurrence
+}
+
+/// Replace selected node occurrences and build their spider interfaces.
+///
+/// For every selected node, the returned vector contains a pair consisting of:
+///
+/// - a left spider whose sources are global-source occurrences and whose
+///   targets are the original node followed by operation-source occurrences;
+/// - a right spider whose sources are the original node followed by
+///   operation-target occurrences and whose targets are global-target
+///   occurrences.
+///
+/// Each selected occurrence is replaced in-place with a fresh node carrying
+/// the original label. Unselected occurrences remain unchanged.
+fn rewrite_occurrences<O: Clone>(
+    selected: &[NodeId],
+    nodes: &mut Vec<O>,
+    adjacency: &mut [Hyperedge],
+    sources: &mut [NodeId],
+    targets: &mut [NodeId],
+) -> Vec<(Hyperedge, Hyperedge)> {
+    let node_count = nodes.len();
+
+    // Index spiders by original node while rewriting, but only create selected pairs.
+    let mut spiders: Vec<Option<(Hyperedge, Hyperedge)>> = (0..node_count).map(|_| None).collect();
+    for &node in selected {
+        spiders[node.0].get_or_insert_with(|| {
+            (
+                Hyperedge {
+                    sources: vec![],
+                    targets: vec![node],
+                },
+                Hyperedge {
+                    sources: vec![node],
+                    targets: vec![],
+                },
+            )
+        });
+    }
+
+    // Operation sources leave the left spider; operation targets enter the
+    // right spider.
+    for adjacency in adjacency {
+        for node in &mut adjacency.sources {
+            let original = *node;
+            if let Some((left_spider, _)) = spiders[original.0].as_mut() {
+                let occurrence = new_occurrence(nodes, original);
+                left_spider.targets.push(occurrence);
+                *node = occurrence;
+            }
+        }
+
+        for node in &mut adjacency.targets {
+            let original = *node;
+            if let Some((_, right_spider)) = spiders[original.0].as_mut() {
+                let occurrence = new_occurrence(nodes, original);
+                right_spider.sources.push(occurrence);
+                *node = occurrence;
+            }
+        }
+    }
+
+    // Global sources enter the left spider; global targets leave the right.
+    for node in sources {
+        let original = *node;
+        if let Some((left_spider, _)) = spiders[original.0].as_mut() {
+            let occurrence = new_occurrence(nodes, original);
+            left_spider.sources.push(occurrence);
+            *node = occurrence;
+        }
+    }
+
+    for node in targets {
+        let original = *node;
+        if let Some((_, right_spider)) = spiders[original.0].as_mut() {
+            let occurrence = new_occurrence(nodes, original);
+            right_spider.targets.push(occurrence);
+            *node = occurrence;
+        }
+    }
+
+    spiders.into_iter().flatten().collect()
+}
diff --git a/tests/lax/cycle.rs b/tests/lax/cycle.rs
new file mode 100644
index 0000000..55f8986
--- /dev/null
+++ b/tests/lax/cycle.rs
@@ -0,0 +1,94 @@
+use open_hypergraphs::lax::{cycle_breaking_nodes, NodeId, OpenHypergraph};
+use proptest::proptest;
+
+use crate::theory::meaningless::{arb_open_hypergraph, Arr, Obj};
+
+#[test]
+fn acyclic_graph_needs_no_cycle_breakers() {
+    let f = OpenHypergraph::singleton("edge", vec![()], vec![()]);
+
+    assert!(cycle_breaking_nodes(&f).unwrap().is_empty());
+}
+
+#[test]
+fn self_loop_selects_its_node() {
+    let mut f = OpenHypergraph::empty();
+    let node = f.new_node(());
+    f.new_edge("loop", ([node], [node]));
+
+    let selected = cycle_breaking_nodes(&f).unwrap();
+
+    assert_eq!(selected, vec![node]);
+    assert!(f
+        .spiderize_nodes(&selected)
+        .unwrap()
+        .to_strict()
+        .is_acyclic());
+}
+
+#[test]
+fn one_node_breaks_a_two_node_cycle() {
+    let mut f = OpenHypergraph::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.new_edge("forward", ([x], [y]));
+    f.new_edge("backward", ([y], [x]));
+
+    let selected = cycle_breaking_nodes(&f).unwrap();
+
+    assert_eq!(selected.len(), 1);
+    assert!(f
+        .spiderize_nodes(&selected)
+        .unwrap()
+        .to_strict()
+        .is_acyclic());
+}
+
+#[test]
+fn shared_high_degree_node_breaks_multiple_cycles() {
+    let mut f = OpenHypergraph::empty();
+    let hub = f.new_node(());
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.new_edge("hub-x", ([hub], [x]));
+    f.new_edge("x-hub", ([x], [hub]));
+    f.new_edge("hub-y", ([hub], [y]));
+    f.new_edge("y-hub", ([y], [hub]));
+
+    assert_eq!(cycle_breaking_nodes(&f).unwrap(), vec![hub]);
+}
+
+#[test]
+fn pending_quotient_is_rejected_then_its_cycle_is_broken() {
+    let mut f = OpenHypergraph::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.new_edge("edge", ([x], [y]));
+    f.unify(x, y);
+
+    assert!(cycle_breaking_nodes(&f).is_none());
+
+    f.quotient().unwrap();
+    let selected = cycle_breaking_nodes(&f).unwrap();
+
+    assert_eq!(selected, vec![NodeId(0)]);
+    assert!(f
+        .spiderize_nodes(&selected)
+        .unwrap()
+        .to_strict()
+        .is_acyclic());
+}
+
+proptest! {
+    #[test]
+    fn selected_nodes_always_break_cycles(
+        strict_input in arb_open_hypergraph()
+    ) {
+        let input: OpenHypergraph<Obj, Arr> =
+            OpenHypergraph::from_strict(strict_input);
+        let selected = cycle_breaking_nodes(&input).unwrap();
+        let spiderized = input.spiderize_nodes(&selected).unwrap();
+
+        assert!(spiderized.to_strict().is_acyclic());
+    }
+}
diff --git a/tests/lax/mod.rs b/tests/lax/mod.rs
index 71e4288..f3d62f2 100644
--- a/tests/lax/mod.rs
+++ b/tests/lax/mod.rs
@@ -1,4 +1,6 @@
+pub mod cycle;
 pub mod eval;
 pub mod functor;
 pub mod hypergraph;
 pub mod open_hypergraph;
+pub mod spider;
diff --git a/tests/lax/spider.rs b/tests/lax/spider.rs
new file mode 100644
index 0000000..cdadf48
--- /dev/null
+++ b/tests/lax/spider.rs
@@ -0,0 +1,212 @@
+use open_hypergraphs::lax::{Hyperedge, Hypergraph, NodeId, OpenHypergraph, WithSpider};
+use proptest::proptest;
+
+use crate::theory::meaningless::{arb_open_hypergraph, Arr, Obj};
+
+fn forget_spiders<O: Clone + PartialEq, A: Clone>(
+    f: OpenHypergraph<O, WithSpider<A>>,
+) -> OpenHypergraph<O, A> {
+    let OpenHypergraph {
+        sources,
+        targets,
+        hypergraph,
+    } = f;
+
+    let mut result = OpenHypergraph {
+        sources,
+        targets,
+        hypergraph: Hypergraph {
+            nodes: hypergraph.nodes,
+            edges: vec![],
+            adjacency: vec![],
+            quotient: hypergraph.quotient,
+        },
+    };
+
+    for (operation, adjacency) in hypergraph.edges.into_iter().zip(hypergraph.adjacency) {
+        match operation {
+            WithSpider::Operation(operation) => {
+                result.hypergraph.edges.push(operation);
+                result.hypergraph.adjacency.push(adjacency);
+            }
+            WithSpider::Spider => {
+                let mut incident = adjacency.sources.into_iter().chain(adjacency.targets);
+                if let Some(first) = incident.next() {
+                    for node in incident {
+                        result.unify(first, node);
+                    }
+                }
+            }
+        }
+    }
+
+    result.quotient().expect("spider legs have equal labels");
+    result
+}
+
+#[test]
+fn spiderize_makes_a_cyclic_non_monogamous_hypergraph_syntactic() {
+    let mut f = OpenHypergraph::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+
+    f.new_edge("forward", ([x], [y]));
+    f.new_edge("backward", ([y], [x]));
+    f.sources = vec![x, x];
+    f.targets = vec![y, y];
+
+    let spiderized = f.spiderize().unwrap();
+    let strict = spiderized.clone().to_strict();
+
+    assert!(strict.is_monogamous());
+    assert!(strict.is_acyclic());
+    assert!(spiderized.hypergraph.is_strict());
+    assert_eq!(spiderized.hypergraph.edges.len(), 2 + 2 * 2);
+}
+
+#[test]
+fn spider_arities_count_all_occurrences() {
+    let mut f = OpenHypergraph::empty();
+    let node = f.new_node(());
+    f.new_edge("op", ([node, node], [node]));
+    f.sources = vec![node, node];
+    f.targets = vec![node];
+
+    let spiderized = f.spiderize().unwrap();
+
+    assert_eq!(
+        spiderized.hypergraph.edges,
+        vec![
+            WithSpider::Operation("op"),
+            WithSpider::Spider,
+            WithSpider::Spider,
+        ]
+    );
+
+    assert_eq!(spiderized.sources.len(), 2);
+    assert_ne!(spiderized.sources[0], spiderized.sources[1]);
+
+    let left_spider = &spiderized.hypergraph.adjacency[1];
+    let right_spider = &spiderized.hypergraph.adjacency[2];
+    assert_eq!(
+        (left_spider.sources.len(), left_spider.targets.len()),
+        (2, 3)
+    );
+    assert_eq!(
+        (right_spider.sources.len(), right_spider.targets.len()),
+        (2, 1)
+    );
+    assert_eq!(left_spider.sources, spiderized.sources);
+    assert_eq!(right_spider.targets, spiderized.targets);
+}
+
+#[test]
+fn spiderize_applies_pending_quotients() {
+    let mut f = OpenHypergraph::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.new_edge("loop", ([x], [y]));
+    f.unify(x, y);
+
+    let spiderized = f.spiderize().unwrap();
+
+    assert_eq!(spiderized.hypergraph.edges.len(), 1 + 2);
+    assert!(spiderized.clone().to_strict().is_acyclic());
+    assert_eq!(
+        forget_spiders(spiderized),
+        OpenHypergraph {
+            sources: vec![],
+            targets: vec![],
+            hypergraph: Hypergraph {
+                nodes: vec![()],
+                edges: vec!["loop"],
+                adjacency: vec![Hyperedge {
+                    sources: vec![NodeId(0)],
+                    targets: vec![NodeId(0)],
+                }],
+                quotient: (vec![], vec![]),
+            },
+        }
+    );
+}
+
+#[test]
+fn spiderize_rejects_inconsistent_quotients() {
+    let mut f = OpenHypergraph::<_, ()>::identity(vec!["a", "b"]);
+    f.unify(NodeId(0), NodeId(1));
+
+    assert!(f.spiderize().is_err());
+}
+
+#[test]
+fn spiderize_nodes_only_replaces_selected_nodes() {
+    let mut f = OpenHypergraph::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.new_edge("forward", ([x], [y]));
+    f.new_edge("backward", ([y], [x]));
+
+    let original = f.clone();
+    let spiderized = f.spiderize_nodes(&[x]).unwrap();
+
+    assert_eq!(
+        spiderized
+            .hypergraph
+            .edges
+            .iter()
+            .filter(|edge| matches!(edge, WithSpider::Spider))
+            .count(),
+        2
+    );
+    assert!(spiderized.clone().to_strict().is_acyclic());
+    assert_eq!(forget_spiders(spiderized), original);
+}
+
+#[test]
+fn spiderize_nodes_maps_selections_through_quotient() {
+    let mut f = OpenHypergraph::<(), ()>::empty();
+    let x = f.new_node(());
+    let y = f.new_node(());
+    f.unify(x, y);
+
+    let spiderized = f.spiderize_nodes(&[y, y]).unwrap();
+
+    assert_eq!(spiderized.hypergraph.edges.len(), 2);
+}
+
+proptest! {
+    #[test]
+    fn spiderize_is_acyclic_monogamous_and_forgetful(
+        strict_input in arb_open_hypergraph()
+    ) {
+        let input: OpenHypergraph<Obj, Arr> =
+            OpenHypergraph::from_strict(strict_input);
+        let input_node_count = input.hypergraph.nodes.len();
+        let input_operation_count = input.hypergraph.edges.len();
+        let spiderized = input.clone().spiderize().unwrap();
+        let strict_spiderized = spiderized.clone().to_strict();
+
+        assert!(strict_spiderized.is_monogamous());
+        assert!(strict_spiderized.is_acyclic());
+        assert_eq!(
+            spiderized.hypergraph.edges.len(),
+            input_operation_count + 2 * input_node_count
+        );
+        assert_eq!(forget_spiders(spiderized), input);
+    }
+
+    #[test]
+    fn spiderize_delegates_to_spiderize_nodes(
+        strict_input in arb_open_hypergraph()
+    ) {
+        let input: OpenHypergraph<Obj, Arr> =
+            OpenHypergraph::from_strict(strict_input);
+        let nodes: Vec<NodeId> =
+            (0..input.hypergraph.nodes.len()).map(NodeId).collect();
+
+        assert_eq!(
+            input.clone().spiderize().unwrap(),
+            input.spiderize_nodes(&nodes).unwrap()
+        );
+    }
+}