diff --git a/benchmark/Agents.jl b/benchmark/Agents.jl
index 9120cb1..b0d688b 100644
--- a/benchmark/Agents.jl
+++ b/benchmark/Agents.jl
@@ -207,12 +207,14 @@ const WS = WS_Generic{Int}
 @acset_type WS′_Generic(TheoryWS′, part_type=BitSetParts) <: HasGraph
 const WS′ = WS′_Generic{Int,Tuple{Int,Int}}
 
-F = Migrate(
-  Dict(:Sheep => :Wolf, :Wolf => :Sheep),
-  Dict([:sheep_loc => :wolf_loc, :wolf_loc => :sheep_loc,
-    :sheep_eng => :wolf_eng, :wolf_eng => :sheep_eng,
-    :countdown => :countdown]), TheoryWS, WS)
-F2 = Migrate(TheoryWS, WS, TheoryWS′, WS′; delta=false)
+F = ΔMigration(FinFunctor(
+  Dict(:V=>:V, :E=>:E, :Eng=>:Eng, :Dir=>:Dir, :Sheep => :Wolf, :Wolf => :Sheep, :Time=>:Time),
+  Dict(:src=>:src, :tgt=>:tgt, :dir=>:dir, 
+       :sheep_loc => :wolf_loc, :wolf_loc => :sheep_loc,
+       :sheep_eng => :wolf_eng, :wolf_eng => :sheep_eng, :countdown => :countdown,
+       :sheep_dir => :wolf_dir, :wolf_dir => :sheep_dir), SchLV, SchLV), LV);
+
+F2 = ΣMigration(FinFunctor(SchLV, SchLV′), LV′);
 
 #=
 Create an n × n grid with periodic boundary conditions. Edges in each cardinal
diff --git a/docs/literate/game_of_life.jl b/docs/literate/game_of_life.jl
index 20cf18c..fd6dea9 100644
--- a/docs/literate/game_of_life.jl
+++ b/docs/literate/game_of_life.jl
@@ -80,8 +80,7 @@ and obtain a state of the world with coordinates (the canonical way to do this
 is to assign "variables" for the values of the coordinates).
 =#
 
-F = Migrate(SchLifeCoords, LifeCoords; delta=false); # adds coordinates
-# F⁻¹ = DeltaMigration(FinFunctor(idₒ, idₘ, SchLife, SchLifeCoords)); # removes coordinates
+F = ΣMigration(FinFunctor(SchLife, SchLifeCoords), LifeCoords); # adds coordinates
 
 # # Helper functions
 
diff --git a/docs/literate/lotka_volterra.jl b/docs/literate/lotka_volterra.jl
index 1137cfb..0889c93 100644
--- a/docs/literate/lotka_volterra.jl
+++ b/docs/literate/lotka_volterra.jl
@@ -124,11 +124,12 @@ migration, we can define them in terms of sheep and then migrate along `F` to
 obtain the analogous actions for wolves.
 =#
 
-F = Migrate(
-  Dict(:Sheep => :Wolf, :Wolf => :Sheep, :Time=>:Time),
-  Dict([:sheep_loc => :wolf_loc, :wolf_loc => :sheep_loc,
-    :sheep_eng => :wolf_eng, :wolf_eng => :sheep_eng, :countdown => :countdown,
-    :sheep_dir => :wolf_dir, :wolf_dir => :sheep_dir,]), SchLV, LV);
+F = ΔMigration(FinFunctor(
+  Dict(:V=>:V, :E=>:E, :Eng=>:Eng, :Dir=>:Dir, :Sheep => :Wolf, :Wolf => :Sheep, :Time=>:Time),
+  Dict(:src=>:src, :tgt=>:tgt, :dir=>:dir, 
+       :sheep_loc => :wolf_loc, :wolf_loc => :sheep_loc,
+       :sheep_eng => :wolf_eng, :wolf_eng => :sheep_eng, :countdown => :countdown,
+       :sheep_dir => :wolf_dir, :wolf_dir => :sheep_dir), SchLV, SchLV), LV);
 
 #=
 We ought to be able to take a state of the world (with no coordinate information)
@@ -136,7 +137,7 @@ and obtain a state of the world with coordinates (the canonical way to do this
 is to assign "variables" for the values of the coordinates).
 =#
 
-F2 = Migrate(SchLV, LV, SchLV′, LV′; delta=false);
+F2 = ΣMigration(FinFunctor(SchLV, SchLV′), LV′);
 
 # # Initializing and visualizing world states
 
@@ -479,8 +480,7 @@ s_die_l = @acset_colim yLV begin s::Sheep; sheep_eng(s) == 0 end;
 sheep_die_rule = Rule(hom(G, s_die_l), id(G))
 sheep_starve = (RuleApp(:starve, sheep_die_rule,
   hom(S, s_die_l), create(G))
-                ⋅
-                (id([I]) ⊗ Weaken(create(S))) ⋅ merge_wires(I));
+  ⋅ (id([I]) ⊗ Weaken(create(S))) ⋅ merge_wires(I));
 
 # #### Sheep starvation test
 
diff --git a/docs/literate/ptg_simple.jl b/docs/literate/ptg_simple.jl
index 1c2ce32..6f08f9b 100644
--- a/docs/literate/ptg_simple.jl
+++ b/docs/literate/ptg_simple.jl
@@ -131,4 +131,4 @@ matches = get_matches(moveBreadRule, state)
 match = matches[1]
 
 # Compute the new world state after rewriting
-new_state = rewrite_match(moveBreadRule, match)
\ No newline at end of file
+new_state = rewrite_match(moveBreadRule, match)
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index f95ce42..69923ba 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -1,8 +1,7 @@
 module CSets
 export extend_morphism, pushout_complement,
        can_pushout_complement, dangling_condition, invert_hom, check_pb,
-       gluing_conditions, extend_morphisms, sub_vars,
-       Migrate, invert_iso, deattr, var_pullback
+       gluing_conditions, invert_iso, deattr, var_pullback
 
 using CompTime
 
@@ -305,53 +304,11 @@ function cascade_subobj(X::ACSet, sub)
   end 
   return Dict([k => collect(v) for (k,v) in pairs(sub)])
 end
-
-  
   
 # Variables
 ###########
 
-"""
-Given a value for each variable, create a morphism X → X′ which applies the 
-substitution. We do this via pushout.
-
-  O --> X    where C has AttrVars for `merge` equivalence classes 
-  ↓          and O has only AttrVars (sent to concrete values or eq classes 
-  C          in the map to C.
-
-`subs` and `merge` are dictionaries keyed by attrtype names
-
-`subs` values are int-keyed dictionaries indicating binding, e.g. 
-`; subs = (Weight = Dict(1 => 3.20, 5 => 2.32), ...)`
-
-`merge` values are vectors of vectors indicating equivalence classes, e.g.
-`; merge = (Weight = [[2,3], [4,6]], ...)`
-"""
-function sub_vars(X::ACSet, subs::AbstractDict=Dict(), merge::AbstractDict=Dict()) 
-  S = acset_schema(X)
-  O, C = [constructor(X)() for _ in 1:2]
-  ox_, oc_ = Dict{Symbol, Any}(), Dict{Symbol,Any}()
-  for at in attrtypes(S)
-    d = get(subs, at, Dict())
-    ox_[at] = AttrVar.(filter(p->p ∈ keys(d) && !(d[p] isa AttrVar), parts(X,at)))
-    oc_[at] = Any[d[p.val] for p in ox_[at]]
-    add_parts!(O, at, length(oc_[at]))
-
-    for eq in get(merge, at, [])
-      isempty(eq) && error("Cannot have empty eq class")
-      c = AttrVar(add_part!(C, at))
-      for var in eq
-        add_part!(O, at)
-        push!(ox_[at], AttrVar(var))
-        push!(oc_[at], c)
-      end
-    end
-  end
-  ox = ACSetTransformation(O,X; ox_...)
-  oc = ACSetTransformation(O,C; oc_...)
-  return first(legs(pushout(ox, oc)))
-end 
-
+# TODO check if this can be replaced by pullbacks of CSetTransformations
 """
 Take an ACSet pullback combinatorially and freely add variables for all 
 attribute subparts.
@@ -416,80 +373,13 @@ function homomorphisms(X::Slice,Y::Slice; kw...)
   end |> collect
 end
 
-function homomorphism(X::Slice,Y::Slice; kw...)
+function homomorphism(X::Slice, Y::Slice; kw...)
   hs = homomorphisms(X,Y; kw...)
   return isempty(hs) ? nothing : first(hs)
 end
 
-# Simple Δ migrations (or limited case Σ)
-#########################################
-
-"""TODO: check if functorial"""
-@struct_hash_equal struct Migrate
-  obs::Dict{Symbol, Symbol}
-  homs::Dict{Symbol, Symbol}
-  P1::Presentation
-  T1::Type 
-  P2::Presentation
-  T2::Type 
-  delta::Bool 
-end 
-
-Migrate(s1::Presentation, t1::Type, s2=nothing, t2=nothing; delta=true) = 
-Migrate(Dict(x => x for x in Symbol.(generators(s1, :Ob))),
-        Dict(x => x for x in Symbol.(generators(s1, :Hom))),
-        s1, t1, s2, t2; delta)
-
-Migrate(o::Dict, h::Dict, s1::Presentation, t1::Type, s2=nothing, t2=nothing; 
-        delta::Bool=true) = Migrate(Dict(collect(pairs(o))),
-                                    Dict(collect(pairs(h))), s1, t1, 
-                                    isnothing(s2) ? s1 : s2, 
-                                    isnothing(t2) ? t1 : t2, 
-                                    delta)
-
-
 sparsify(d::Dict{V,<:ACSet}) where V = Dict([k=>sparsify(v) for (k,v) in collect(d)])
 sparsify(d::Dict{<:ACSet,V}) where V = Dict([sparsify(k)=>v for (k,v) in collect(d)])
 sparsify(::Nothing) = nothing
 
-(F::Migrate)(d::Dict{V,<:ACSet}) where V = Dict([k=>F(v) for (k,v) in collect(d)])
-(F::Migrate)(d::Dict{<:ACSet,V}) where V = Dict([F(k)=>v for (k,v) in collect(d)])
-(m::Migrate)(::Nothing) = nothing
-(m::Migrate)(s::Union{String,Symbol}) = s
-function (m::Migrate)(Y::ACSet)
-  if m.delta
-     typeof(Y) <: m.T1 || error("Cannot Δ migrate a $(typeof(Y))")
-  end
-  S = acset_schema(Y)
-  X = m.T2()
-  partsX = Dict(c => add_parts!(X, c, nparts(Y, get(m.obs,c,c)))
-                for c in ob(S) ∪ attrtypes(S))
-  for (f,c,d) in homs(S)
-    set_subpart!(X, partsX[c], f, partsX[d][subpart(Y, get(m.homs,f,f))])
-  end
-  for (f,c,_) in attrs(S)
-    set_subpart!(X, partsX[c], f, subpart(Y, get(m.homs,f,f)))
-  end
-  if !m.delta 
-    # undefined attrs (Σ migration) get replaced with free variables
-    for (f,c,d) in attrs(acset_schema(X))
-      for i in setdiff(parts(X,c), X.subparts[f].m.defined)
-        X[i,f] = AttrVar(add_part!(X,d))
-      end
-    end
-  end 
-  return X
-end 
-
-function (F::Migrate)(f::ACSetTransformation)
-  d = Dict(map(collect(pairs(components(f)))) do (k,v)
-    get(F.obs,k,k) => collect(v)
-  end)
-  only(homomorphisms(F(dom(f)), F(codom(f)), initial=d))
-end
-
-(F::Migrate)(s::Multispan) = Multispan(apex(s), F.(collect(s)))
-(F::Migrate)(s::Multicospan) = Multicospan(apex(s), F.(collect(s)))
-(F::Migrate)(d::AbstractDict) = Dict(get(F.obs,k, k)=>v for (k,v) in collect(d))
-
 end # module
diff --git a/src/rewrite/Constraints.jl b/src/rewrite/Constraints.jl
index ac83e91..ef346d7 100644
--- a/src/rewrite/Constraints.jl
+++ b/src/rewrite/Constraints.jl
@@ -4,10 +4,10 @@ export apply_constraint, Constraint, CGraph, arity,
        AppCond, LiftCond, Trivial, PAC, NAC
 using Catlab
 import Catlab.Theories: ⊗, ⊕
-import Catlab.CategoricalAlgebra: ¬
+import Catlab.CategoricalAlgebra: ¬, incident
 import Catlab.Graphics: to_graphviz
+import Catlab: getvalue
 using StructEquality
-import ...CategoricalAlgebra.CSets: Migrate
 import ACSets: sparsify
 
 """
@@ -40,37 +40,44 @@ end
 @acset_type VELabeledGraph(SchVELabeledGraph) <: AbstractGraph
 @acset_type VLabeledGraph(SchVLabeledGraph) <: AbstractGraph
 
+const CGraphACSet = VELabeledGraph{Union{Nothing, ACSet},
+                                   Union{Nothing, Int, ACSetTransformation}}
 """
 "nothing" means something that will be determined via a quantifier
 Ints are explicit arguments provided when apply_constraint is called
 """
-const CGraph = VELabeledGraph{Union{Nothing, ACSet},
-                              Union{Nothing, Int, ACSetTransformation}}
+@struct_hash_equal struct CGraph 
+  val::CGraphACSet
+  CGraph(val=CGraphACSet()) = new(val)
+end
+getvalue(c::CGraph) = c.val
+Base.getindex(c::CGraph, i...) = getindex(getvalue(c), i...)
+incident(c::CGraph, x...) = incident(getvalue(c), x...)
 
 """Number of variables in a constraint graph"""
 arity(g::CGraph) = maximum(filter(v->v isa Int, g[:elabel]); init=0) 
 
 """Apply migration to all literals in the constraint"""
-function (F::Migrate)(c::CGraph)
-  c = deepcopy(c)
+function (F::SimpleMigration)(c::CGraph)
+  c = deepcopy(getvalue(c))
   c[:vlabel] = [x isa ACSet ? F(x) : x for x in c[:vlabel]]
   c[:elabel] = [x isa ACSetTransformation ? F(x) : x for x in c[:elabel]]
-  return c
+  return CGraph(c)
 end
 function sparsify(c::CGraph)
-  c = deepcopy(c)
+  c = deepcopy(getvalue(c))
   c[:vlabel] = [x isa ACSet ? sparsify(x) : x for x in c[:vlabel]]
   c[:elabel] = [x isa ACSetTransformation ? sparsify(x) : x for x in c[:elabel]]
-  return c
+  return CGraph(c)
 end
 
 """
 Take two CGraphs and merge them along their overlapping vertices and edges
 Returns an ACSetColimit
 """
-function merge_graphs(g1,g2)
+function merge_graphs(g1::CGraphACSet, g2::CGraphACSet)
   # Vertices with literal acsets on them that match
-  overlap_g = CGraph()
+  overlap_g = CGraphACSet()
   p1, p2 = [Dict(:V=>Int[], :E=>Int[]) for _ in 1:2]
   # Merge vertices
   for (v1,X) in filter(x->x[2] isa ACSet, collect(enumerate(g1[:vlabel])))
@@ -339,9 +346,9 @@ map_edges(f,c::Quantifier) = Quantifier(f[:E](c.e),c.kind,map_edges(f,c.expr);
 @struct_hash_equal struct Constraint
   g::CGraph 
   d::BoolExpr 
-  function Constraint(g,d)
-    nparts(g,:VLabel) == 0 || error("No vertex variables allowed")
-    nparts(g,:ELabel) == 0 || error("No edge variables allowed")
+  function Constraint(g::CGraph,d::BoolExpr)
+    nparts(getvalue(g),:VLabel) == 0 || error("No vertex variables allowed")
+    nparts(getvalue(g),:ELabel) == 0 || error("No edge variables allowed")
     # check that all of the object assignments match the defined morphisms 
     for (eind, (s, t, h)) in enumerate(zip(g[:src], g[:tgt], g[:elabel]))
       sv, tv = [g[x,:vlabel] for x in [s,t]]
@@ -366,7 +373,7 @@ map_edges(f,c::Quantifier) = Quantifier(f[:E](c.e),c.kind,map_edges(f,c.expr);
 end
 arity(g::Constraint) = arity(g.g)
 
-(F::Migrate)(c::Constraint) = Constraint(F(c.g),c.d)
+(F::SimpleMigration)(c::Constraint) = Constraint(F(c.g),c.d)
 sparsify(c::Constraint) = Constraint(sparsify(c.g), c.d)
 const Trivial = Constraint(CGraph(), True)
 const Trivial′ = Constraint(CGraph(), False)
@@ -375,15 +382,13 @@ const Trivial′ = Constraint(CGraph(), False)
 Combine two constraints conjunctively, sharing as much of the computation graph 
 as possible (i.e. pushout along the maximum common subgraph)
 """
-function ⊗(c1::Constraint,c2::Constraint) 
-  if c1 == Trivial′ || c2 == Trivial′ return Trivial′ end 
-  if c1 == Trivial  return c2 
-  elseif c2 == Trivial return c1 
-  end  
-
-  new_g = merge_graphs(c1.g, c2.g)
-  l1, l2 = legs(new_g)
-  Constraint(apex(new_g), map_edges(l1,c1.d) ⊗ map_edges(l2,c2.d))
+function ⊗(c1::Constraint, c2::Constraint) 
+  (c1 == Trivial′ || c2 == Trivial′) && return Trivial′ 
+  c1 == Trivial && return c2 
+  c2 == Trivial && return c1 
+
+  l1, l2 = new_g = merge_graphs(getvalue(c1.g), getvalue(c2.g))
+  Constraint(CGraph(apex(new_g)), map_edges(l1, c1.d) ⊗ map_edges(l2, c2.d))
 end
 
 ⊗(cs::Constraint...) = reduce(⊗, cs; init=Trivial) 
@@ -393,14 +398,13 @@ Combine two constraints disjunctively, sharing as much of the computation graph
 as possible.
 """
 function ⊕(c1::Constraint,c2::Constraint) 
-  if c1 == Trivial || c2 == Trivial return Trivial end 
-  if c1 == Trivial′  return c2 
-  elseif c2 == Trivial′ return c1 
-  end  
-  new_g = merge_graphs(c1.g, c2.g)
-  l1, l2 = legs(new_g)
-  new_d = map_edges(l1,c1.d) ⊕ map_edges(l2,c2.d)
-  Constraint(apex(new_g), new_d)
+  (c1 == Trivial || c2 == Trivial) && return Trivial 
+  c1 == Trivial′ && return c2 
+  c2 == Trivial′ && return c1 
+
+  l1, l2 = new_g = merge_graphs(getvalue(c1.g), getvalue(c2.g))
+  new_d = map_edges(l1, c1.d) ⊕ map_edges(l2, c2.d)
+  Constraint(CGraph(apex(new_g)), new_d)
 end
 
 ⊕(cs::Constraint...) = reduce(⊕, cs; init=Trivial′) 
@@ -410,14 +414,14 @@ end
 
 """Get the C-Set associated with a vertex in a CGraph"""
 function get_ob(c::CGraph, v_i::Int, curr::Assgn)
-  if c[v_i, :vlabel] isa ACSet return c[v_i, :vlabel]  end
+  c[v_i, :vlabel] isa ACSet && return c[v_i, :vlabel]
   for e_out in incident(c, v_i, :src)
-    if !isnothing(curr[e_out]) return dom(curr[e_out]) end 
+    isnothing(curr[e_out]) || return dom(curr[e_out]) 
   end
   for e_in in incident(c, v_i, :tgt)
-    if !isnothing(curr[e_in]) return codom(curr[e_in]) end 
+    isnothing(curr[e_in]) || return codom(curr[e_in]) 
   end
-  error("Failed to get ob")
+  error("Failed to get ob $v_i from $c w/ curr $curr")
 end
 
 function apply_constraint(c::Constraint, fs...)
@@ -450,9 +454,9 @@ triangle commuting.
       (3)
 """
 function AppCond(f::ACSetTransformation, pos::Bool=true; monic=false)
-  cg = @acset CGraph begin V=3; E=3; src=[2,1,2]; tgt=[1,3,3];
+  cg = CGraph(@acset CGraphACSet begin V=3; E=3; src=[2,1,2]; tgt=[1,3,3];
     vlabel=[codom(f), dom(f), nothing]; elabel=[f, nothing, 1]
-  end
+  end)
   expr = ∃(2, Commutes([1,2],[3]); monic=monic)
   return Constraint(cg, pos ? expr : ¬(expr))
 end
@@ -473,28 +477,28 @@ function LiftCond(vertical::ACSetTransformation, bottom::ACSetTransformation;
                   monic_all=false, monic_exists=false)
   codom(vertical) == dom(bottom) || error("Composable pair required")
   A, B = dom.([vertical, bottom]); Y = codom(bottom)
-  cg = @acset CGraph begin V=4; E=5; src=[1,1,2,2,3]; tgt=[2,3,3,4,4]
+  g = CGraph(@acset CGraphACSet begin V=4; E=5; src=[1,1,2,2,3]; tgt=[2,3,3,4,4]
     vlabel=[A,B,nothing,Y]; elabel=[vertical, nothing, nothing, bottom, 1]
-  end
+  end)
   expr = ∀(2, ∃(3, Commutes([1,3],[2]) ⊗ Commutes([3,5],[4]); 
                 monic=monic_exists);
            st=Commutes([2,5],[1,4]), monic=monic_all)
-  return Constraint(cg, expr)
+  return Constraint(g, expr)
 end
 
 # Visualize constraints
 #######################
 
 function to_graphviz(c::Constraint)
-  pg = to_graphviz_property_graph(c.g; node_labels=true,
+  pg = to_graphviz_property_graph(getvalue(c.g); node_labels=true,
                                   graph_attrs=Dict(:label=>sprint(show, c.d)))
 
-  for v in vertices(c.g)
+  for v in vertices(getvalue(c.g))
     x = isnothing(c.g[v, :vlabel]) ? "λ" : ""
     set_vprop!(pg, v, :label, "$x$v")
   end
 
-  for e in edges(c.g)
+  for e in edges(getvalue(c.g))
     x = if     c.g[e, :elabel] isa Int    "(λ$(c.g[e, :elabel]))"
         elseif isnothing(c.g[e, :elabel]) getquantifier(c.d, e)
         else                              ""
diff --git a/src/rewrite/PBPO.jl b/src/rewrite/PBPO.jl
index 1f0dd5e..64e0797 100644
--- a/src/rewrite/PBPO.jl
+++ b/src/rewrite/PBPO.jl
@@ -3,7 +3,7 @@ export PBPORule
 
 using Catlab, Catlab.CategoricalAlgebra
 import Catlab.CategoricalAlgebra: left, right
-using Catlab.CategoricalAlgebra.CSets: abstract_attributes
+using Catlab.CategoricalAlgebra.CSets: abstract_attributes, sub_vars
 using Catlab.CategoricalAlgebra.HomSearch: backtracking_search
 using Catlab.CategoricalAlgebra.Chase: extend_morphism_constraints  
 
@@ -69,7 +69,7 @@ ruletype(::PBPORule) = :PBPO
 left(r::PBPORule) = r.l 
 right(r::PBPORule) = r.r
 
-(F::Migrate)(r::PBPORule) =
+(F::SimpleMigration)(r::PBPORule) =
   PBPORule(F(r.l), F(r.r), F(r.tl), F(r.tk), F(r.l′); monic=r.monic,
            acs=F.(r.acs), lcs=F.(r.lcs), expr=F(r.exprs), k_expr=F(r.k_exprs), 
            adherence=r.adherence)
diff --git a/src/rewrite/Utils.jl b/src/rewrite/Utils.jl
index 33befff..79aea17 100644
--- a/src/rewrite/Utils.jl
+++ b/src/rewrite/Utils.jl
@@ -5,16 +5,17 @@ export Rule, ruletype,rewrite, rewrite_match, rewrite_full_output,
 
 using Catlab, Catlab.Theories
 using Catlab.CategoricalAlgebra
+using Catlab.CategoricalAlgebra.CSets: sub_vars
 using Catlab.CategoricalAlgebra.HomSearch: backtracking_search
 import Catlab.CategoricalAlgebra: left, right
 import ACSets: sparsify, acset_schema
 
-using Random
+using Random, DataStructures
 using StructEquality
 
 using ..Constraints
 using ...CategoricalAlgebra
-using ...CategoricalAlgebra.CSets: invert_hom
+using ...CategoricalAlgebra.CSets: invert_hom, var_reference
 
 import Catlab.CategoricalAlgebra.FinSets: is_monic
 is_monic(f::SliceHom) = is_monic(f.f) # UPSTREAM
@@ -81,7 +82,7 @@ condition(s)
           elseif freevar continue 
           else 
             error(
-            "Must set AttrVar value for newly introduced attribute via `exprs`")
+            "Must set AttrVar value for newly-introduced AttrVar $o#$r_var via `exprs` ($exprs)")
           end
         end
       end
@@ -104,8 +105,61 @@ pattern(r::Rule) = codom(left(r))
 acset_schema(r::Rule) = acset_schema(pattern(r))
 
 
-(F::Migrate)(r::Rule{T}) where {T} =
-  Rule{T}(F(r.L), F(r.R); ac=F.(r.conditions), expr=F(r.exprs), monic=r.monic)
+"""
+Some rules involve deleting something and re-adding it. This means Σ
+migrations can introduce variables in L and R that morally should be 
+linked. If not linked, the rule will be invalid (due to introducing 
+variables in R). This can be addressed by 'connecting' the variables via
+adding AttrVars to I and mapping to the left and right. 
+
+This is just a band-aid until patch-graph rewriting or something analogous 
+allows us to avoid spurious deletion + addition rules.
+"""
+function (F::SimpleMigration)(r::Rule{T}; connect=true) where {T}
+  expr = Dict(Symbol(ob_map(functor(F), k)) => v for (k,v) in pairs(r.exprs))
+  Fl, Fr = F(r.L), F(r.R)
+  FL, FR = codom(Fl), codom(Fr)
+  S = acset_schema(FL)
+  connect_dict = DefaultDict(()->[])
+  if connect 
+    for o in attrtypes(S)
+      for r_var in parts(FR, o)
+        preim = preimage(Fr[o], AttrVar(r_var))
+        if isempty(preim) && isnothing(get′(expr, o, r_var))
+          # Assume: new var is *not* floating
+          (f, c, jᵣ) = var_reference(FR, o, r_var) 
+          # Assume: part it's attached to uniquely identified w/ something in L
+          jₗ = only([p for p in parts(FL, c) if isempty(preimage(Fl[c], p))])
+          # And that thing has a fresh attrvar too
+          if isempty(preimage(Fl[o], FL[jₗ, f]))
+            p = add_part!(dom(Fl),o)
+            p2 = add_part!(dom(Fr),o)
+            p == p2 || error("p $p p2 $p2")
+            push!(connect_dict[o], (p, FL[jₗ, f], AttrVar(r_var)))
+          end
+        end
+      end
+    end
+  end 
+  Fl, Fr = map([(Fl,1), (Fr,2)]) do (FMap, var)
+    initial = Dict{Any,Any}(map(types(S)) do t 
+      p(x::Int) = t ∈ ob(S) ? x : AttrVar(x)
+      d =Dict{Any,Any}(map(connect_dict[t]) do (z, lr...)
+        z => lr[var]
+      end)
+      for i in parts(dom(FMap), t)
+        if !haskey(d, i)
+          d[i] = FMap[t](p(i))
+        end
+      end
+      t => d
+    end)
+    homomorphism(dom(FMap), codom(FMap); initial)
+  end
+
+  Rule{T}(Fl, Fr; ac=F.(r.conditions), expr, monic=r.monic)
+end
+
 sparsify(r::Rule{T}) where T = 
   Rule{T}(sparsify(r.L), sparsify(r.R); ac=sparsify.(r.conditions), 
           expr=r.exprs, monic=r.monic)
@@ -277,4 +331,5 @@ rewrite_match(r::AbsRule, m; kw...) =
 
 
 function check_match_var_eqs end # implement in DPO.jl
+
 end # module
diff --git a/src/schedules/Basic.jl b/src/schedules/Basic.jl
index fd591b0..0825172 100644
--- a/src/schedules/Basic.jl
+++ b/src/schedules/Basic.jl
@@ -7,7 +7,7 @@ using Catlab.CategoricalAlgebra, Catlab.Theories
 
 using ...Rewrite
 using ...Rewrite.Inplace: interp_program!
-using ...CategoricalAlgebra.CSets: Migrate
+
 using ..Poly
 using ..Wiring: AgentBox
 import ..Wiring: input_ports, output_ports, initial_state, color, update!
@@ -28,7 +28,7 @@ input_ports(r::Weaken) = [codom(r.agent)]
 output_ports(r::Weaken) = [dom(r.agent)]
 initial_state(::Weaken) = nothing 
 color(::Weaken) = "lavender"
-(F::Migrate)(a::Weaken) =  Weaken(a.name,F(a.agent))
+(F::SimpleMigration)(a::Weaken) =  Weaken(a.name,F(a.agent))
 sparsify(a::Weaken) = Weaken(a.name, sparsify(a.agent))
 
 function update!(::Ref, boxdata::Weaken, g::ACSetTransformation, inport::Int)
@@ -60,7 +60,7 @@ input_ports(r::Strengthen) = [dom(r.agent)]
 output_ports(r::Strengthen) = [codom(r.agent)]
 initial_state(::Strengthen) = nothing 
 color(::Strengthen) = "lightgreen"
-(F::Migrate)(a::Strengthen) =  Strengthen(a.name,F(a.agent))
+(F::SimpleMigration)(a::Strengthen) =  Strengthen(a.name,F(a.agent))
 sparsify(a::Strengthen) = Strengthen(a.name, sparsify(a.agent))
 
 function update!(::Ref, boxdata::Strengthen, g::ACSetTransformation, inport::Int)
@@ -88,7 +88,8 @@ input_ports(r::Initialize) = isnothing(r.in_agent) ? [] : [r.in_agent]
 output_ports(r::Initialize) = [typeof(r.state)()]
 initial_state(::Initialize) = nothing 
 color(::Initialize) = "gray"
-(F::Migrate)(a::Initialize) = Initialize(a.name,F(a.state),F(a.in_agent))
+(F::SimpleMigration)(a::Initialize) = 
+  Initialize(a.name,F(a.state),F(a.in_agent))
 sparsify(a::Initialize) = Initialize(a.name, sparsify([a.state,a.in_agent])...)
 
 function update(i::Initialize, t::PMonad)
@@ -119,7 +120,7 @@ initial_state(::Fail) = nothing
 
 color(::Fail) = "red"
 
-(F::Migrate)(a::Fail) = Fail(F(a.agent), a.silent, a.name)
+(F::SimpleMigration)(a::Fail) = Fail(F(a.agent), a.silent, a.name)
 
 sparsify(a::Fail) = Fail(sparsify(a.agent), a.silent, a.name)
 
diff --git a/src/schedules/Callbacks.jl b/src/schedules/Callbacks.jl
index d2f9cf0..5c9283c 100644
--- a/src/schedules/Callbacks.jl
+++ b/src/schedules/Callbacks.jl
@@ -3,7 +3,6 @@ export CallbackBox
 
 using Catlab, StructEquality
 
-using ...CategoricalAlgebra.CSets: Migrate
 using ..Poly
 using ..Wiring: AgentBox
 import ACSets: sparsify
@@ -25,7 +24,7 @@ initial_state(::CallbackBox) = nothing
 color(b::CallbackBox) = "purple"
 
 # Warning that the callback function cannot be functorially migrated
-(F::Migrate)(b::CallbackBox) = CallbackBox(b.name, b.callback, F(b.agent))
+(F::SimpleMigration)(b::CallbackBox) = CallbackBox(b.name, b.callback, F(b.agent))
 
 sparsify(b::CallbackBox) = CallbackBox(b.name, b.callback, sparsify(b.agent))
 
diff --git a/src/schedules/Conditionals.jl b/src/schedules/Conditionals.jl
index 2af20b2..632d734 100644
--- a/src/schedules/Conditionals.jl
+++ b/src/schedules/Conditionals.jl
@@ -5,7 +5,6 @@ using StructEquality
 
 using Catlab.CategoricalAlgebra, Catlab.WiringDiagrams
 
-using ...CategoricalAlgebra.CSets: Migrate
 using ..Wiring, ..Poly
 using ..Wiring: AgentBox
 import ACSets: sparsify
@@ -49,7 +48,7 @@ color(::Conditional) = "lightpink"
 
 # WARNING: the update/prob functions hide their ACSet dependence in code, so 
 # data migration cannot update these parts which may cause runtime errors.
-(F::Migrate)(a::Conditional) = 
+(F::SimpleMigration)(a::Conditional) = 
   Conditional(a.prob, a.n, F(a.agent); update=a.update, name=a.name, init=a.init)
 
 sparsify(a::Conditional) = 
diff --git a/src/schedules/Queries.jl b/src/schedules/Queries.jl
index a8a8fd9..d621e47 100644
--- a/src/schedules/Queries.jl
+++ b/src/schedules/Queries.jl
@@ -6,7 +6,7 @@ using StructEquality
 using Catlab, Catlab.CategoricalAlgebra, Catlab.WiringDiagrams
 
 using ...Rewrite
-using ...CategoricalAlgebra.CSets: Migrate
+using ...Rewrite.Constraints: CGraphACSet
 using ..Basic: Fail
 using ..Wiring, ..Poly, ..Eval
 using ..Wiring: AgentBox,  str_hom
@@ -63,10 +63,10 @@ and purported new agent. (the new agent is the first argument to the constraint)
   """
   function Query(a::Span, n::Symbol=:Query, ret=nothing; constraint=Trivial)
     in_shape, agent_shape = codom.([left(a),right(a)])
-    cg = @acset CGraph begin V=4; E=4; src=[1,1,2,3]; tgt=[2,3,4,4]
+    cg = CGraph(@acset CGraphACSet begin V=4; E=4; src=[1,1,2,3]; tgt=[2,3,4,4]
       vlabel=[apex(a), in_shape, agent_shape, nothing]
       elabel=[a...,2,1]
-    end
+    end)
     constr = Constraint(cg, Commutes([1,3],[2,4])) ⊗ constraint
     rshape = isnothing(ret) ? agent_shape : ret
     new(n, in_shape, agent_shape, rshape, constr)
@@ -82,10 +82,10 @@ and purported new agent. (the new agent is the first argument to the constraint)
   """
   function Query(a::ACSetTransformation, n::Symbol=:Query, ret=nothing; constraint=Trivial)
     in_shape, agent_shape = [dom(a),codom(a)]
-    cg = @acset CGraph begin V=3; E=3; src=[1,2,1]; tgt=[2,3,3]
+    cg = CGraph(@acset CGraphACSet begin V=3; E=3; src=[1,2,1]; tgt=[2,3,3]
       vlabel=[in_shape, agent_shape, nothing]
       elabel=[a,2,1]
-    end
+    end)
     constr = Constraint(cg, Commutes([3],[1,2])) ⊗ constraint
     rshape = isnothing(ret) ? agent_shape : ret
     new(n, in_shape, agent_shape, rshape, constr)
@@ -110,7 +110,7 @@ color(::Query) = "yellow"
 input_ports(c::Query) = [c.agent, c.return_type] 
 output_ports(c::Query) = [c.agent, c.subagent, typeof(c.agent)()]
 initial_state(c::Query) = (constructor(c.agent)(), ACSetTransformation[])
-(F::Migrate)(a::Query) =  Query(F(a.subagent), F(a.agent), a.name, 
+(F::SimpleMigration)(a::Query) =  Query(F(a.subagent), F(a.agent), a.name, 
                                 F(a.return_type); constraint=F(a.constraint))
 sparsify(q::Query) = Query(q.name, sparsify.([q.subagent,q.agent,q.return_type])...; 
                            constraint=sparsify(q.constraint))
diff --git a/src/schedules/RuleApps.jl b/src/schedules/RuleApps.jl
index 8a49427..01bf5ed 100644
--- a/src/schedules/RuleApps.jl
+++ b/src/schedules/RuleApps.jl
@@ -8,7 +8,7 @@ using Catlab.CategoricalAlgebra, Catlab.Theories
 using ...Rewrite
 using ...Rewrite.Utils: AbsRule, get_rmap, get_pmap, get_expr_binding_map
 using ...Rewrite.Inplace: interp_program!
-using ...CategoricalAlgebra.CSets: Migrate, extend_morphism_constraints
+using ...CategoricalAlgebra.CSets: extend_morphism_constraints
 using ..Wiring, ..Poly, ..Eval, ..Basic
 using ..Wiring: str_hom, mk_sched
 import ..Wiring: AgentBox, input_ports, output_ports, initial_state, color, update!
@@ -56,7 +56,7 @@ input_ports(r::RuleApp) = [dom(r.in_agent)]
 output_ports(r::RuleApp) = [dom(r.out_agent), dom(r.in_agent)]
 color(::RuleApp) = "lightblue"
 initial_state(::RuleApp) = nothing 
-(F::Migrate)(a::RuleApp) = 
+(F::SimpleMigration)(a::RuleApp) = 
   RuleApp(a.name,F(a.rule), F(a.in_agent), F(a.out_agent))
 sparsify(a::RuleApp) = 
   RuleApp(a.name,sparsify(a.rule), sparsify(a.in_agent), sparsify(a.out_agent))
diff --git a/src/schedules/Wiring.jl b/src/schedules/Wiring.jl
index 10b558e..344358c 100644
--- a/src/schedules/Wiring.jl
+++ b/src/schedules/Wiring.jl
@@ -4,6 +4,7 @@ export Schedule, Names, mk_sched, typecheck, merge_wires,
 
 using Catlab, Catlab.CategoricalAlgebra, Catlab.WiringDiagrams, Catlab.Programs,
       Catlab.Theories
+
 import Catlab.WiringDiagrams.DirectedWiringDiagrams: input_ports,output_ports
 import Catlab.Theories: Ob,Hom,id, create, compose, otimes, ⋅, ⊗, ∇,□, trace, 
                         munit, braid, dom, codom, mmerge
@@ -42,7 +43,9 @@ function Base.setindex!(n::Names{T}, y::T, x::String) where T
   n.from_name[x] = y 
   n.to_name[y] = x
 end
-(F::Migrate)(n::Names) = Names(F(n.from_name))
+(F::SimpleMigration)(n::Names) = Names(Dict(map(collect(n.from_name)) do (k,v)
+  k => F(v)
+end))
 sparsify(n::Names) = Names(sparsify(n.from_name))
 
 # General wiring diagram utilities
@@ -189,7 +192,7 @@ otimes(x::Schedule, y::AgentBox) = otimes(x, singleton(y))
 
 
 """Map a functor over the data of a schedule"""
-function (F::Migrate)(wd_::Schedule) 
+function (F::SimpleMigration)(wd_::Schedule) 
   wd = deepcopy(wd_.d)
   for x in [:value, Symbol.(["$(x)_port_type" for x in 
                             [:outer_in,:outer_out,:out,:in]])...,
@@ -209,8 +212,14 @@ function sparsify(wd_::Schedule)
   end 
   return Schedule(wd,wd_.x)
 end
-(F::Migrate)(x::T) where {T<:TM.Ob} = T(F.(x.args), F.(x.type_args))
-(F::Migrate)(x::T) where {T<:TM.Hom} = T(F.(x.args), F.(x.type_args))
+
+function (F::SimpleMigration)(x::T) where {T<:TM.Ob} 
+  T(F.(x.args), F.(x.type_args))
+end
+  
+function (F::SimpleMigration)(x::T) where {T<:TM.Hom} 
+  T([a isa Symbol || a isa String ? a : F(a) for a in x.args], F.(x.type_args))
+end 
 
 const wnames = [
   # Begin   End          Val            BeginType             EndType
diff --git a/test/rewrite/Constraints.jl b/test/rewrite/Constraints.jl
index f780ec1..a70b023 100644
--- a/test/rewrite/Constraints.jl
+++ b/test/rewrite/Constraints.jl
@@ -1,13 +1,11 @@
 module TestConstraints 
-using AlgebraicRewriting
-using Catlab
-using Test 
-
+using AlgebraicRewriting, Catlab, Test 
+using AlgebraicRewriting.Rewrite.Constraints: CGraphACSet
 # Testing arity 2 constraints
 #############################
-cg = @acset CGraph begin V=3; E=3; src=[1,1,2]; tgt=[3,2,3]; 
+cg = (@acset CGraphACSet begin V=3; E=3; src=[1,1,2]; tgt=[3,2,3]; 
   vlabel=Graph.([2,2,2]); elabel=[1,2,nothing] 
-end
+end) |> CGraph
 c = Constraint(cg, ∃(3, Commutes([1],[2,3])))
 h1, hid, hnot, _ = homomorphisms(Graph.([2,2])...)
 @test !apply_constraint(c, hid, h1)
diff --git a/test/rewrite/PBPO.jl b/test/rewrite/PBPO.jl
index 97baaff..5c43631 100644
--- a/test/rewrite/PBPO.jl
+++ b/test/rewrite/PBPO.jl
@@ -3,6 +3,7 @@ module TestPBPO
 using Test, AlgebraicRewriting, Catlab
 
 using AlgebraicRewriting.Rewrite.PBPO: partial_abstract
+using AlgebraicRewriting.Rewrite.Constraints: CGraphACSet
 
 # Partial abstract
 ##################
@@ -113,10 +114,11 @@ vertical = ACSetTransformation(G1, arr; V=[2])
 bottom_5 = homomorphism(arr, L′; initial=(V=[1,2],))
 bottom_6 = homomorphism(arr, L′;initial=(V=[2,2],))
 
-cg = @acset CGraph begin V=4; E=6; src=[2,1,3,1,3,3]; tgt=[4,2,2,3,4,4];
+cg = CGraph(@acset CGraphACSet begin V=4; E=6; 
+  src=[2,1,3,1,3,3]; tgt=[4,2,2,3,4,4];
   vlabel=[G1, nothing, arr, L′]; 
   elabel=[1, nothing,  nothing, vertical, bottom_5, bottom_6]
-end
+end)
 
 expr = ∀(2, ∃(3, 
               ⊗(Commutes([4,3],[2]), 
diff --git a/test/runtests.jl b/test/runtests.jl
index f2ad5ad..4bcdb81 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -13,11 +13,11 @@ using DataMigrations
 #######
 
 @testset "Full Demo" begin
-  # include("../docs/literate/full_demo.jl")
+  include("../docs/literate/full_demo.jl")
 end
 
 @testset "Lotka Volterra" begin
-  # include("../docs/literate/lotka_volterra.jl")
+  include("../docs/literate/lotka_volterra.jl")
 end
 
 @testset "Game of Life" begin