The @acset_colim macro is a beloved method of constructing individual ACSets. But, when people try to create rewrite rules, they need to specify a whole diagram of ACSets. After constructing the objects, they have lost the nice names they wrote down in the @acset_colim macro. The solution seems to be to use the @migration macro to directly specify the diagram. Something like:1
@migration(SchGraph, begin
L => @join begin
(e1,e2)::E
src(e2)==tgt(e1)
end
I => @join begin
(e1,e2)::E
(v1,v2)::V
src(e1)==v2
end
R => @join begin
e::E
src(e)==tgt(e)
end
left::(I=>L) => begin
e1 => e1
e2 => e1
v1 => v2
end
right::(I=>R) => begin end
end)
Here, the maps left and right are uniquely determined by these particular generators. A homomorphisms search with those values initialized would return exactly one morphism (for starters, anything else could throw an error).
The
@acset_colimmacro is a beloved method of constructing individual ACSets. But, when people try to create rewrite rules, they need to specify a whole diagram of ACSets. After constructing the objects, they have lost the nice names they wrote down in the@acset_colimmacro. The solution seems to be to use the@migrationmacro to directly specify the diagram. Something like:1Here, the maps
leftandrightare uniquely determined by these particular generators. Ahomomorphismssearch with those values initialized would return exactly one morphism (for starters, anything else could throw an error).Footnotes
Maybe this syntax isn't exactly compatible with
@migrationbecause it's defining the shape category at the same time. You could ignore the::(I=>L)stuff and pretend we have a macro specific for the span diagram. It would be helpful, though for a syntax which lets you do the shape on the fly since we may have negative/positive application conditions as well as other sorts of morphisms showing up relevant to rewriting. ↩