diff --git a/src/DiagrammaticEquations.jl b/src/DiagrammaticEquations.jl
index d0ef187..be9cace 100644
--- a/src/DiagrammaticEquations.jl
+++ b/src/DiagrammaticEquations.jl
@@ -61,13 +61,12 @@ include("rewrite.jl")
 include("pretty.jl")
 include("colanguage.jl")
 include("openoperators.jl")
+include("symbolictheoryutils.jl")
 include("deca/Deca.jl")
 include("learn/Learn.jl")
-include("ThDEC.jl")
-include("decasymbolic.jl")
+include("SymbolicUtilsInterop.jl")
 
-@reexport using .ThDEC
-@reexport using .SymbolicUtilsInterop
 @reexport using .Deca
+@reexport using .SymbolicUtilsInterop
 
 end
diff --git a/src/SymbolicUtilsInterop.jl b/src/SymbolicUtilsInterop.jl
new file mode 100644
index 0000000..c3c9b5a
--- /dev/null
+++ b/src/SymbolicUtilsInterop.jl
@@ -0,0 +1,154 @@
+module SymbolicUtilsInterop
+
+using ..DiagrammaticEquations: AbstractDecapode, Quantity
+import ..DiagrammaticEquations: eval_eq!, SummationDecapode
+using ..decapodes
+using ..Deca
+
+using MLStyle
+using SymbolicUtils
+using SymbolicUtils: Symbolic, BasicSymbolic, FnType, Sym
+
+# name collision with decapodes.Equation
+struct SymbolicEquation{E}
+    lhs::E
+    rhs::E
+end
+
+Base.show(io::IO, e::SymbolicEquation) = begin
+    print(io, e.lhs); print(io, " == "); print(io, e.rhs)
+end
+
+## a struct carry the symbolic variables and their equations
+struct SymbolicContext
+    vars::Vector{Symbolic}
+    equations::Vector{SymbolicEquation{Symbolic}}
+end
+export SymbolicContext
+
+Base.show(io::IO, d::SymbolicContext) = begin
+    println(io, "SymbolicContext(")
+    println(io, "  Variables: [$(join(d.vars, ", "))]")
+    println(io, "  Equations: [")
+    eqns = map(d.equations) do op
+      "    $(op)"
+    end
+    println(io, "$(join(eqns,",\n"))])")
+  end
+
+## BasicSymbolic -> DecaExpr
+function decapodes.Term(t::SymbolicUtils.BasicSymbolic)
+    if SymbolicUtils.issym(t)
+        decapodes.Var(nameof(t))
+    else
+        op = SymbolicUtils.head(t)
+        args = SymbolicUtils.arguments(t)
+        termargs = Term.(args)
+        if op == +
+            decapodes.Plus(termargs)
+        elseif op == *
+            decapodes.Mult(termargs)
+        elseif op == ∂ₜ
+            decapodes.Tan(only(termargs))
+        elseif length(args) == 1
+            decapodes.App1(nameof(op, args...), termargs...)
+        elseif length(args) == 2
+            decapodes.App2(nameof(op, args...), termargs...)
+        else
+            error("was unable to convert $t into a Term")
+        end
+    end
+end
+
+decapodes.Term(x::Real) = decapodes.Lit(Symbol(x))
+
+function decapodes.DecaExpr(d::SymbolicContext)
+    context = map(d.vars) do var
+        decapodes.Judgement(nameof(var), nameof(Sort(var)), :X)
+    end
+    equations = map(d.equations) do eq
+        decapodes.Eq(decapodes.Term(eq.lhs), decapodes.Term(eq.rhs))
+    end
+    decapodes.DecaExpr(context, equations)
+end
+
+"""
+Retrieve the SymbolicUtils expression of a DecaExpr term `t` from a context of variables in ThDEC
+
+Example:
+```
+  a = @syms a::Real
+  context = Dict(:a => Scalar(), :u => PrimalForm(0))
+  SymbolicUtils.BasicSymbolic(context, Term(a))
+```
+"""
+function SymbolicUtils.BasicSymbolic(context::Dict{Symbol,Quantity}, t::decapodes.Term, __module__=@__MODULE__)
+    # user must import symbols into scope
+    ! = (f -> getfield(__module__, f))
+    @match t begin
+        Var(name) => SymbolicUtils.Sym{context[name]}(name)
+        Lit(v) => Meta.parse(string(v))
+        # see heat_eq test: eqs had AppCirc1, but this returns
+        # App1(f, App1(...)
+        AppCirc1(fs, arg) => foldr(
+            # panics with constants like :k
+            # see test/language.jl
+            (f, x) -> (!(f))(x),
+            fs;
+            init=BasicSymbolic(context, arg, __module__)
+        )
+        App1(f, x) => (!(f))(BasicSymbolic(context, x, __module__))
+        App2(f, x, y) => (!(f))(BasicSymbolic(context, x, __module__), BasicSymbolic(context, y, __module__))
+        Plus(xs) => +(BasicSymbolic.(Ref(context), xs, Ref(__module__))...)
+        Mult(xs) => *(BasicSymbolic.(Ref(context), xs, Ref(__module__))...)
+        Tan(x) => ∂ₜ(BasicSymbolic(context, x, __module__))
+    end
+end
+
+function SymbolicContext(d::decapodes.DecaExpr, __module__=@__MODULE__)
+    # associates each var to its sort...
+    context = map(d.context) do j
+        @info j.var
+        j.var => j.var
+    end
+    # ... which we then produce a vector of symbolic vars
+    vars = map(context) do (v, s)
+        SymbolicUtils.Sym{s}(v)
+    end
+    context = Dict{Symbol,Quantity}(context)
+    eqs = map(d.equations) do eq
+        SymbolicEquation{Symbolic}(BasicSymbolic.(Ref(context), [eq.lhs, eq.rhs], Ref(__module__))...)
+    end
+    SymbolicContext(vars, eqs)
+end
+
+function eval_eq!(eq::SymbolicEquation, d::AbstractDecapode, syms::Dict{Symbol, Int}, deletions::Vector{Int})
+    eval_eq!(Equation(Term(eq.lhs), Term(eq.rhs)), d, syms, deletions)
+end
+
+"""    function SummationDecapode(e::SymbolicContext) """
+function SummationDecapode(e::SymbolicContext)
+    d = SummationDecapode{Any, Any, Symbol}()
+    symbol_table = Dict{Symbol, Int}()
+
+    foreach(e.vars) do var
+        # convert Sort(var)::PrimalForm0 --> :Form0
+        var_id = add_part!(d, :Var, name=var.name, type=nameof(Sort(var)))
+        symbol_table[var.name] = var_id
+    end
+
+    deletions = Vector{Int}()
+    foreach(e.equations) do eq
+        eval_eq!(eq, d, symbol_table, deletions)
+    end
+    rem_parts!(d, :Var, sort(deletions))
+
+    recognize_types(d)
+
+    fill_names!(d)
+    d[:name] = normalize_unicode.(d[:name])
+    make_sum_mult_unique!(d)
+    return d
+end
+
+end
diff --git a/src/ThDEC.jl b/src/ThDEC.jl
deleted file mode 100644
index 6cb25e0..0000000
--- a/src/ThDEC.jl
+++ /dev/null
@@ -1,283 +0,0 @@
-module ThDEC
-
-using MLStyle
-using StructEquality
-
-import Base: +, -, *
-
-"""
-Given a tuple of symbols ("aliases") and their canonical name (or "rep"), produces
-for each alias typechecking and nameof methods which call those for their rep.
-Example:
-@alias d₀, d₁, += d
-"""
-macro alias(body)
-    (rep, aliases) = @match body begin
-        Expr(:tuple, rep, Expr(:tuple, aliases...)) => (rep, aliases)
-        _ => nothing
-    end
-    result = quote end
-    foreach(aliases) do alias
-        push!(result.args,
-            quote
-                function $(esc(alias))(s...)
-                    $(esc(rep))(s...) 
-                end
-                export $(esc(alias))
-                Base.nameof(::typeof($alias), s) = nameof($rep, s)
-            end)
-    end
-    result
-end
-
-struct SortError <: Exception
-    message::String
-end
-
-@struct_hash_equal struct Space
-    name::Symbol
-    dim::Int
-end
-export Space
-
-dim(s::Space) = s.dim
-Base.nameof(s::Space) = s.name
-
-struct SpaceLookup
-    default::Space
-    named::Dict{Symbol,Space}
-end
-export SpaceLookup
-
-function SpaceLookup(default::Space)
-    SpaceLookup(default, Dict{Symbol, Space}(nameof(default) => default))
-end
-
-@data Sort begin
-    Scalar()
-    Form(dim::Int, isdual::Bool, space::Space)
-    VField(isdual::Bool, space::Space)
-end
-export Sort, Scalar, Form, VField
-
-function fromexpr(lookup::SpaceLookup, e, ::Type{Sort})
-    (name, spacename) = @match e begin
-        name::Symbol => (name, nothing)
-        :($name{$spacename}) => (name, spacename)
-    end
-    space = @match spacename begin
-        ::Nothing => lookup.default
-        name::Symbol => lookup.named[name]
-    end
-    @match name begin
-        :Form0 => Form(0, false, space)
-        :Form1 => Form(1, false, space)
-        :Form2 => Form(2, false, space)
-        :DualForm0 => Form(0, true, space)
-        :DualForm1 => Form(1, true, space)
-        :DualForm2 => Form(2, true, space)
-        :Constant => Scalar()
-    end
-end
-
-Base.nameof(s::Scalar) = :Constant
-
-function Base.nameof(f::Form; with_dim_parameter=false)
-    dual = isdual(f) ? "Dual" : ""
-    formname = Symbol("$(dual)Form$(dim(f))")
-    if with_dim_parameter
-        return Expr(:curly, formname, dim(space(f)))
-    else
-        return formname
-    end
-end
-
-const VF = VField
-
-dim(ω::Form) = ω.dim
-isdual(ω::Form) = ω.isdual
-space(ω::Form) = ω.space
-export space
-
-isdual(v::VField) = v.isdual
-space(v::VField) = v.space
-
-# convenience functions
-PrimalForm(i::Int, space::Space) = Form(i, false, space)
-export PrimalForm
-
-DualForm(i::Int, space::Space) = Form(i, true, space)
-export DualForm
-
-PrimalVF(space::Space) = VF(false, space)
-export PrimalVF
-
-DualVF(space::Space) = VF(true, space)
-export DualVF
-
-# show methods
-show_duality(ω::Form) = isdual(ω) ? "dual" : "primal"
-
-function Base.show(io::IO, ω::Form)
-    print(io, isdual(ω) ? "DualForm($(dim(ω))) on $(space(ω))" : "PrimalForm($(dim(ω))) on $(space(ω))")
-end
-
-# TODO: VField
-@nospecialize
-function +(s1::Sort, s2::Sort)
-    @match (s1, s2) begin
-        (Scalar(), Scalar()) => Scalar()
-        (Scalar(), Form(i, isdual, space)) ||
-            (Form(i, isdual, space), Scalar()) => Form(i, isdual, space)
-        (Form(i1, isdual1, space1), Form(i2, isdual2, space2)) =>
-            if (i1 == i2) && (isdual1 == isdual2) && (space1 == space2)
-                Form(i1, isdual1, space1)
-            else
-                throw(SortError(
-                    """
-                    Can not add two forms of different dimensions/dualities/spaces:
-                    $((i1,isdual1,space1)) and $((i2,isdual2,space2))
-                    """)
-                )
-            end
-    end
-end
-
-# Type-checking inverse of addition follows addition
--(s1::Sort, s2::Sort) = +(s1, s2)
-
-# TODO error for Forms
-
-# Negation is always valid
--(s::Sort) = s
-
-# TODO: VField
-@nospecialize
-function *(s1::Sort, s2::Sort)
-    @match (s1, s2) begin
-        (Scalar(), Scalar()) => Scalar()
-        (Scalar(), Form(i, isdual, space)) ||
-            (Form(i, isdual, space), Scalar()) => Form(i, isdual, space)
-        (Form(_, _, _), Form(_, _, _)) =>
-            throw(SortError("Cannot scalar multiply a form with a form. Maybe try `∧`??"))
-    end
-end
-
-const SUBSCRIPT_DIGIT_0 = '₀'
-
-as_sub(n::Int) = join(map(d -> SUBSCRIPT_DIGIT_0 + d, digits(n)))
-
-# TODO: VField
-@nospecialize
-function ∧(s1::Sort, s2::Sort)
-    @match (s1, s2) begin
-        (Form(i, isdual, space), Scalar()) || (Scalar(), Form(i, isdual, space)) =>
-            Form(i, isdual, space)
-        (Form(i1, isdual1, space1), Form(i2, isdual2, space2)) => begin
-            (isdual1 == isdual2) && (space1 == space2) || throw(SortError("Can only take a wedge product of two forms of the same duality on the same space"))
-            if i1 + i2 <= dim(space1)
-                Form(i1 + i2, isdual1, space1)
-            else
-                throw(SortError("Can only take a wedge product when the dimensions of the forms add to less than n, where n = $(dim(space1)) is the dimension of the ambient space: tried to wedge product $i1 and $i2"))
-            end
-        end
-        (VF(isdual, _), _) || (_, VF(isdual, _)) => throw(SortError("Can only take a wedge product of forms. Flatten (♭) your vector field before applying")) 
-    end
-end
-
-function Base.nameof(::typeof(∧), s1, s2)
-    Symbol("∧$(as_sub(dim(s1)))$(as_sub(dim(s2)))")
-end
-
-@nospecialize
-∂ₜ(s::Sort) = s
-
-@nospecialize
-function d(s::Sort)
-    @match s begin
-        Scalar() => throw(SortError("Cannot take exterior derivative of a scalar"))
-        Form(i, isdual, space) =>
-            if i < dim(space)
-                Form(i + 1, isdual, space)
-            else
-                throw(SortError("Cannot take exterior derivative of a k-form for k >= n, where n = $(dim(space)) is the dimension of its ambient space"))
-            end
-    end
-end
-
-@alias d, (d₀, d₁)
-
-Base.nameof(::typeof(d), s) = Symbol("d$(as_sub(dim(s)))")
-
-@nospecialize
-function ⋆(s::Sort)
-    @match s begin
-        Scalar() => throw(SortError("Cannot take Hodge star of a scalar"))
-        VF(isdual, space) => throw(SortError("Cannot take the Hodge star of a vector field"))
-        Form(i, isdual, space) => Form(dim(space) - i, !isdual, space)
-    end
-end
-export ⋆
-
-@alias ⋆, (⋆₀, ⋆₁, ⋆₂, ⋆₀⁻¹, ⋆₁⁻¹, ⋆₂⁻¹)
-
-function Base.nameof(::typeof(⋆), s)
-    inv = isdual(s) ? "⁻¹" : ""
-    Symbol("★$(as_sub(isdual(s) ? dim(space(s)) - dim(s) : dim(s)))$(inv)")
-end
-
-@nospecialize
-function ι(s1::Sort, s2::Sort)
-    @match (s1, s2) begin
-        (VF(true, space), Form(i, true, space)) => Form(i, false, space) # wrong
-        (VF(true, space), Form(i, false, space)) => DualForm(i, true, space)
-        _ => throw(SortError("Can only define the discrete interior product on:
-                PrimalVF, DualForm(i)
-                DualVF(), PrimalForm(i)
-                ."))
-    end
-end
-
-# in practice, a scalar may be treated as a constant 0-form.
-function ♯(s::Sort)
-    @match s begin
-        Scalar() => PrimalVF()
-        Form(1, isdual, space) => VF(isdual, space)
-        _ => throw(SortError("Can only take ♯ to 1-forms"))
-    end
-end
-# musical isos may be defined for any combination of (primal/dual) form -> (primal/dual) vf.
-
-Base.nameof(::typeof(♯), s) = Symbol("♯$s")
-
-function ♭(s::Sort)
-    @match s begin
-        VF(true, space) => Form(1, false, space)
-        _ => throw(SortError("Can only apply ♭ to dual vector fields"))
-    end
-end
-
-Base.nameof(::typeof(♭), s) = Symbol("♭$s")
-
-# OTHER
-
-function ♭♯(s::Sort)
-    @match s begin
-        Form(i, isdual, space) => Form(i, !isdual, space)
-        _ => throw(SortError("♭♯ is only defined on forms."))
-    end
-end
-
-# Δ = ★d⋆d, but we check signature here to throw a more helpful error
-function Δ(s::Sort)
-    @match s begin
-        Scalar() => Scalar()
-        Form(0, isdual, space) => Form(0, isdual, space)
-        Form(1, isdual, space) => Form(1, isdual, space)
-        _ => throw(SortError("Δ is not defined for $s"))
-    end
-end
-
-Base.nameof(::typeof(Δ), s) = Symbol("Δ")
-
-end
diff --git a/src/deca/Deca.jl b/src/deca/Deca.jl
index 8202704..48d5c8b 100644
--- a/src/deca/Deca.jl
+++ b/src/deca/Deca.jl
@@ -4,12 +4,17 @@ using DataStructures
 using ..DiagrammaticEquations
 using Catlab
 
+using Reexport
+
 import ..infer_types!, ..resolve_overloads!
 
 export normalize_unicode, varname, infer_types!, resolve_overloads!, typename, spacename, recursive_delete_parents, recursive_delete_parents!, unicode!, op1_res_rules_1D, op2_res_rules_1D, op1_res_rules_2D, op2_res_rules_2D, op1_inf_rules_1D, op2_inf_rules_1D, op1_inf_rules_2D, op2_inf_rules_2D, vec_to_dec!
 
 include("deca_acset.jl")
 include("deca_visualization.jl")
+include("ThDEC.jl")
+
+@reexport using .TheoryDEC
 
 """    function recursive_delete_parents!(d::SummationDecapode, to_delete::Vector{Int64})
 
diff --git a/src/deca/ThDEC.jl b/src/deca/ThDEC.jl
new file mode 100644
index 0000000..4fe93c7
--- /dev/null
+++ b/src/deca/ThDEC.jl
@@ -0,0 +1,229 @@
+module TheoryDEC
+
+using ..DiagrammaticEquations: @register, @alias, Quantity
+
+using MLStyle
+using StructEquality
+using SymbolicUtils
+using SymbolicUtils: Symbolic, BasicSymbolic, FnType, Sym, Term, symtype
+
+import Base: +, -, *
+import Catlab: Δ, ∧
+
+# ##########################
+# ThDEC
+#
+# Type necessary for symbolic utils
+# ##########################
+
+abstract type ThDEC <: Quantity end
+
+struct Scalar <: ThDEC end
+export Scalar
+
+struct FormParams
+    dim::Int
+    duality::Bool
+    space::Symbol
+    spacedim::Int
+end
+
+dim(fp::FormParams) = getproperty(fp, :dim)
+duality(fp::FormParams) = getproperty(fp, :duality)
+space(fp::FormParams) = getproperty(fp, :space)
+spacedim(fp::FormParams) = getproperty(fp, :spacedim)
+
+"""
+i: dimension: 0,1,2, etc.
+d: duality: true = dual, false = primal
+s: name of the space (a symbol)
+n: dimension of the space
+"""
+struct Form{i,d,s,n} <: ThDEC end
+export Form
+
+# parameter accessors
+dim(::Type{<:Form{i,d,s,n}}) where {i,d,s,n} = i
+isdual(::Type{<:Form{i,d,s,n}}) where {i,d,s,n} = d
+space(::Type{<:Form{i,d,s,n}}) where {i,d,s,n} = s
+spacedim(::Type{<:Form{i,d,s,n}}) where {i,d,s,n} = n
+
+export dim, isdual, space, spacedim
+
+# convert form to form params
+FormParams(::Type{<:Form{i,d,s,n}}) where {i,s,d,n} = FormParams(i,d,s,n)
+
+struct VField{d,s,n} <: ThDEC end
+export VField
+
+# parameter accessors
+isdual(::Type{<:VField{d,s,n}}) where {d,s,n} = d
+space(::Type{VField{d,s,n}}) where {d,s,n} = s
+spacedim(::Type{VField{d,s,n}}) where {d,s,n} = n
+
+
+# convenience functions
+const PrimalForm{i,s,n} = Form{i,false,s,n}
+export PrimalForm
+
+const DualForm{i,s,n} = Form{i,true,s,n}
+export DualForm
+
+const PrimalVF{s,n} = VField{false,s,n}
+export PrimalVF
+
+const DualVF{s,n} = VField{true,s,n}
+export DualVF
+
+# ACTIVE PATTERNS
+
+@active ActForm(T) begin
+    if T <: Form
+        Some(T)
+    end
+end
+
+@active ActFormParams(T) begin
+    if T <: Form
+        Some([T.parameters...])
+    end
+end
+
+@active ActFormDim(T) begin
+    if T <: Form
+        Some(dim(T))
+    end
+end
+
+@active ActScalar(T) begin
+    if T <: Scalar
+        Some(T)
+    end
+end
+
+@active ActVFParams(T) begin
+    if T <: VField
+        Some([T.parameters...])
+    end
+end
+
+# HERE WE DEFINE THE SYMBOLICUTILS
+
+# for every unary operator in our theory, take a BasicSymbolic type, convert its type parameter to a Sort in our theory, and return a term
+unops = [:♯, :♭]
+
+@register -(S)::ThDEC begin S end
+
+@register ∂ₜ(S)::ThDEC begin S end
+
+@register d(S)::ThDEC begin
+    @match S begin
+        ActFormParams([i,d,s,n]) => Form{i+1,d,s,n}
+        _ => throw(SortError("Cannot apply the exterior derivative to $S"))
+    end
+end
+
+@alias (d₀, d₁) => d
+
+@register ⋆(S)::ThDEC begin
+    @match S begin
+        ActFormParams([i,d,s,n]) => Form{n-i,d,s,n}
+        _ => throw(SortError("Cannot take the hodge star of $S"))
+    end
+end
+
+@alias (⋆₀, ⋆₁, ⋆₂, ⋆₀⁻¹, ⋆₁⁻¹, ⋆₂⁻¹) => ⋆
+
+@register Δ(S)::ThDEC begin
+    @match S begin
+        ActForm(x) => ⋆(d(⋆(d(x))))
+        _ => throw(SortError("Cannot take the Laplacian of $S"))
+    end
+end
+
+@register +(S1, S2)::ThDEC begin
+    @match (S1, S2) begin
+        (ActScalar, ActScalar) => Scalar
+        (ActScalar, ActFormParams([i,d,s,n])) || (ActFormParams([i,d,s,n]), ActScalar) => S1 # commutativity
+        (ActFormParams([i1,d1,s1,n1]), ActFormParams([i2,d2,s2,n2])) => begin
+            if (i1 == i2) && (d1 == d2) && (s1 == s2) && (n1 == n2)
+                Form{i1, d1, s1, n1}
+            else
+                throw(SortError("""
+                    Can not add two forms of different dimensions/dualities/spaces:
+                        $((i1,d1,s1)) and $((i2,d2,s2))
+                    """))
+            end
+        end
+        _ => error("Nay!")
+    end
+end
+
+@register -(S1, S2)::ThDEC begin +(S1, S2) end
+
+@register *(S1, S2)::ThDEC begin
+    @match (S1, S2) begin
+        (Scalar, Scalar) => Scalar
+        (Scalar, ActFormParams([i,d,s,n])) || (ActFormParams([i,d,s,n]), Scalar) => Form{i,d,s,n}
+        _ => throw(SortError("Cannot multiple $S1 and $S2"))
+    end
+end
+
+@register ∧(S1, S2)::ThDEC begin
+    @match (S1, S2) begin
+        (ActFormParams([i1,d1,s1,n1]), ActFormParams([i2,d2,s2,n2])) => begin
+            (d1 == d2) && (s1 == s2) && (n1 == n2) || throw(SortError("Can only take a wedge product of two forms of the same duality on the same space"))
+            if i1 + i2 <= n1
+                Form{i1 + i2, d1, s1, n1}
+            else
+                throw(SortError("Can only take a wedge product when the dimensions of the forms add to less than n, where n = $n1 is the dimension of the ambient space: tried to wedge product $i1 and $i2"))
+            end
+        end
+    end
+end
+
+struct SortError <: Exception
+    message::String
+end
+
+Base.nameof(s::Scalar) = :Constant
+
+function Base.nameof(f::Form; with_dim_parameter=false)
+    dual = isdual(f) ? "Dual" : ""
+    formname = Symbol("$(dual)Form$(dim(f))")
+    if with_dim_parameter
+        return Expr(:curly, formname, dim(space(f)))
+    else
+        return formname
+    end
+end
+
+# show methods
+show_duality(ω::Form) = isdual(ω) ? "dual" : "primal"
+
+function Base.show(io::IO, ω::Form)
+    print(io, isdual(ω) ? "DualForm($(dim(ω))) on $(space(ω))" : "PrimalForm($(dim(ω))) on $(space(ω))")
+end
+
+Base.nameof(::typeof(-), s1, s2) = Symbol("$(as_sub(dim(s1)))-$(as_sub(dim(s2)))")
+
+const SUBSCRIPT_DIGIT_0 = '₀'
+
+as_sub(n::Int) = join(map(d -> SUBSCRIPT_DIGIT_0 + d, digits(n)))
+
+function Base.nameof(::typeof(∧), s1::B1, s2::B2) where {S1,S2,B1<:BasicSymbolic{S1}, B2<:BasicSymbolic{S2}}
+    Symbol("∧$(as_sub(dim(symtype(s1))))$(as_sub(dim(symtype(s2))))")
+end
+
+function Base.nameof(::typeof(∧), s1, s2)
+    Symbol("∧$(as_sub(dim(s1)))$(as_sub(dim(s2)))")
+end
+
+Base.nameof(::typeof(d), s) = Symbol("d$(as_sub(dim(s)))")
+
+function Base.nameof(::typeof(⋆), s)
+    inv = isdual(s) ? "⁻¹" : ""
+    Symbol("★$(as_sub(isdual(s) ? dim(space(s)) - dim(s) : dim(s)))$(inv)")
+end
+
+end
diff --git a/src/decasymbolic.jl b/src/decasymbolic.jl
deleted file mode 100644
index 8933ae4..0000000
--- a/src/decasymbolic.jl
+++ /dev/null
@@ -1,340 +0,0 @@
-module SymbolicUtilsInterop
-
-using ..DiagrammaticEquations: AbstractDecapode
-import ..DiagrammaticEquations: eval_eq!, SummationDecapode
-using ..ThDEC
-import ..ThDEC: Sort, dim, isdual
-using ..decapodes
-
-using MLStyle
-using SymbolicUtils
-using SymbolicUtils: Symbolic, BasicSymbolic, FnType, Sym
-
-# ##########################
-# DECType
-#
-# Type necessary for symbolic utils
-# ##########################
-
-# define DECType as a Number. Necessary for SymbolicUtils
-abstract type DECType <: Number end
-
-"""
-i: dimension: 0,1,2, etc.
-d: duality: true = dual, false = primal
-s: name of the space (a symbol)
-n: dimension of the space
-"""
-struct FormT{i,d,s,n} <: DECType end
-export FormT
-
-struct VFieldT{d,s,n} <: DECType end
-export VFieldT
-
-dim(::Type{<:FormT{i,d,s,n}}) where {i,d,s,n} = d
-isdual(::Type{FormT{i,d,s,n}}) where {i,d,s,n} = d
-
-# convenience functions
-const PrimalFormT{i,s,n} = FormT{i,false,s,n}
-export PrimalFormT
-
-const DualFormT{i,s,n} = FormT{i,true,s,n}
-export DualFormT
-
-const PrimalVFT{s,n} = VFieldT{false,s,n}
-export PrimalVFT
-
-const DualVFT{s,n} = VFieldT{true,s,n}
-export DualVFT
-
-"""
-converts ThDEC Sorts into DECType
-"""
-function Sort end
-
-Sort(::Type{<:Real}) = Scalar()
-Sort(::Real) = Scalar()
-
-function Sort(::Type{FormT{i,d,s,n}}) where {i,d,s,n}
-    Form(i, d, Space(s, n))
-end
-
-function Sort(::Type{VFieldT{d,s,n}}) where {d,s,n}
-    VField(d, Space(s, n))
-end
-
-Sort(::BasicSymbolic{T}) where {T} = Sort(T)
-
-"""
-converts ThDEC Sorts into DecaSymbolic types
-"""
-Number(s::Scalar) = Real
-
-Number(f::Form) = FormT{dim(f),isdual(f), nameof(space(f)), dim(space(f))}
-
-Number(v::VField) = VFieldT{isdual(v), nameof(space(v)), dim(space(v))}
-
-# HERE WE DEFINE THE SYMBOLICUTILS
-
-# for every unary operator in our theory, take a BasicSymbolic type, convert its type parameter to a Sort in our theory, and return a term
-unop_dec = [:∂ₜ, :d, :d₀, :d₁
-            , :⋆, :⋆₀, :⋆₁, :⋆₂, :⋆₀⁻¹, :⋆₁⁻¹, :⋆₂⁻¹
-            , :♯, :♭, :-]
-
-for unop in unop_dec
-    @eval begin
-        @nospecialize
-        function ThDEC.$unop(
-            v::BasicSymbolic{T}
-        ) where {T<:DECType}
-            s = ThDEC.$unop(Sort(T))
-            SymbolicUtils.Term{Number(s)}(ThDEC.$unop, [v])
-        end
-    end
-end
-
-# BasicSymbolic{FnType{Tuple{PrimalFormT{0}}}, PrimalFormT{0}}
-
-binop_dec = [:+, :-, :*, :∧, :^]
-export +,-,*,∧,^
-
-for binop in binop_dec
-    @eval begin
-        @nospecialize
-        function ThDEC.$binop(
-            v::BasicSymbolic{T1},
-            w::BasicSymbolic{T2}
-        ) where {T1<:DECType,T2<:DECType}
-            s = ThDEC.$binop(Sort(T1), Sort(T2))
-            SymbolicUtils.Term{Number(s)}(ThDEC.$binop, [v, w])
-        end
-
-        @nospecialize
-        function ThDEC.$binop(
-            v::BasicSymbolic{T1},
-            w::BasicSymbolic{T2}
-        ) where {T1<:DECType,T2<:Real}
-            s = ThDEC.$binop(Sort(T1), Sort(T2))
-            SymbolicUtils.Term{Number(s)}(ThDEC.$binop, [v, w])
-        end
-
-        @nospecialize
-        function ThDEC.$binop(
-            v::BasicSymbolic{T1},
-            w::BasicSymbolic{T2}
-        ) where {T1<:Real,T2<:DECType}
-            s = ThDEC.$binop(Sort(T1), Sort(T2))
-            SymbolicUtils.Term{Number(s)}(ThDEC.$binop, [v, w])
-        end
-    end
-end
-
-# name collision with decapodes.Equation
-struct DecaEquation{E}
-    lhs::E
-    rhs::E
-end
-export DecaEquation
-
-Base.show(io::IO, e::DecaEquation) = begin
-    print(io, e.lhs)
-    print(io, " == ")
-    print(io, e.rhs)
-end
-
-# a struct carry the symbolic variables and their equations
-struct DecaSymbolic
-    vars::Vector{Symbolic}
-    equations::Vector{DecaEquation{Symbolic}}
-end
-export DecaSymbolic
-
-Base.show(io::IO, d::DecaSymbolic) = begin
-    println(io, "DecaSymbolic(")
-    println(io, "  Variables: [$(join(d.vars, ", "))]")
-    println(io, "  Equations: [")
-    eqns = map(d.equations) do op
-      "    $(op)"
-    end
-    println(io, "$(join(eqns,",\n"))])")
-  end
-
-# BasicSymbolic -> DecaExpr
-function decapodes.Term(t::SymbolicUtils.BasicSymbolic)
-    if SymbolicUtils.issym(t)
-        decapodes.Var(nameof(t))
-    else
-        op = SymbolicUtils.head(t)
-        args = SymbolicUtils.arguments(t)
-        termargs = Term.(args)
-        sorts = ThDEC.Sort.(args)
-        if op == +
-            decapodes.Plus(termargs)
-        elseif op == *
-            decapodes.Mult(termargs)
-        elseif op == ThDEC.∂ₜ
-            decapodes.Tan(only(termargs))
-        elseif length(args) == 1
-            decapodes.App1(nameof(op, sorts...), termargs...)
-        elseif length(args) == 2
-            decapodes.App2(nameof(op, sorts...), termargs...)
-        else
-            error("was unable to convert $t into a Term")
-        end
-    end
-end
-
-decapodes.Term(x::Real) = decapodes.Lit(Symbol(x))
-
-function decapodes.DecaExpr(d::DecaSymbolic)
-    context = map(d.vars) do var
-        decapodes.Judgement(nameof(var), nameof(Sort(var)), :X)
-    end
-    equations = map(d.equations) do eq
-        decapodes.Eq(decapodes.Term(eq.lhs), decapodes.Term(eq.rhs))
-    end
-    decapodes.DecaExpr(context, equations)
-end
-
-"""
-Retrieve the SymbolicUtils expression of a DecaExpr term `t` from a context of variables in ThDEC
-
-Example:
-```
-  a = @syms a::Real
-  context = Dict(:a => Scalar(), :u => PrimalForm(0))
-  SymbolicUtils.BasicSymbolic(context, Term(a))
-```
-"""
-function SymbolicUtils.BasicSymbolic(context::Dict{Symbol,Sort}, t::decapodes.Term)
-    # user must import symbols into scope
-    ! = (f -> getfield(Main, f))
-    @match t begin
-        Var(name) => SymbolicUtils.Sym{Number(context[name])}(name)
-        Lit(v) => Meta.parse(string(v))
-        # see heat_eq test: eqs had AppCirc1, but this returns
-        # App1(f, App1(...)
-        AppCirc1(fs, arg) => foldr(
-            # panics with constants like :k
-            # see test/language.jl
-            (f, x) -> (!(f))(x),
-            fs;
-            init=BasicSymbolic(context, arg)
-        )
-        # getfield(Main, 
-        App1(f, x) => (!(f))(BasicSymbolic(context, x))
-        App2(f, x, y) => (!(f))(BasicSymbolic(context, x), BasicSymbolic(context, y))
-        Plus(xs) => +(BasicSymbolic.(Ref(context), xs)...)
-        Mult(xs) => *(BasicSymbolic.(Ref(context), xs)...)
-        Tan(x) => ThDEC.∂ₜ(BasicSymbolic(context, x))
-    end
-end
-
-function DecaSymbolic(lookup::SpaceLookup, d::decapodes.DecaExpr)
-    # associates each var to its sort...
-    context = map(d.context) do j
-        j.var => ThDEC.fromexpr(lookup, j.dim, Sort)
-    end
-    # ... which we then produce a vector of symbolic vars
-    vars = map(context) do (v, s)
-        SymbolicUtils.Sym{Number(s)}(v)
-    end
-    context = Dict{Symbol,Sort}(context)
-    eqs = map(d.equations) do eq
-        DecaEquation{Symbolic}(BasicSymbolic.(Ref(context), [eq.lhs, eq.rhs])...)
-    end
-    DecaSymbolic(vars, eqs)
-end
-
-function eval_eq!(eq::DecaEquation, d::AbstractDecapode, syms::Dict{Symbol, Int}, deletions::Vector{Int})
-    eval_eq!(Equation(Term(eq.lhs), Term(eq.rhs)), d, syms, deletions)
-end
-
-"""    function SummationDecapode(e::DecaSymbolic) """
-function SummationDecapode(e::DecaSymbolic)
-    d = SummationDecapode{Any, Any, Symbol}()
-    symbol_table = Dict{Symbol, Int}()
-
-    foreach(e.vars) do var
-        # convert Sort(var)::PrimalForm0 --> :Form0
-        var_id = add_part!(d, :Var, name=var.name, type=nameof(Sort(var)))
-        symbol_table[var.name] = var_id
-    end
-
-    deletions = Vector{Int}()
-    foreach(e.equations) do eq
-        eval_eq!(eq, d, symbol_table, deletions)
-    end
-    rem_parts!(d, :Var, sort(deletions))
-
-    recognize_types(d)
-
-    fill_names!(d)
-    d[:name] = normalize_unicode.(d[:name])
-    make_sum_mult_unique!(d)
-    return d
-end
-
-"""
-Registers a new function
-
-```
-@register Δ(s::Sort) begin
-    @match s begin
-        ::Scalar => error("Invalid")
-        ::VField => error("Invalid")
-        ::Form => ⋆(d(⋆(d(s))))
-    end
-end
-```
-
-will create an additional method for Δ for operating on BasicSymbolic 
-"""
-macro register(head, body)
-    # parse head
-    parsehead = @λ begin
-        Expr(:call, f, types...) => (f, parsehead.(types))
-        Expr(:(::), var, type) => (var, type)
-        s => s
-    end
-    (f, args) = parsehead(head)
-    matchargs = [:($(x[1])::$(x[2])) for x in args]
-
-    result = quote end
-    push!(result.args,
-          esc(quote
-              function $f($(matchargs...))
-                  $body
-              end
-          end))
-
-    # e.g., given [(:x, :Scalar), (:ω, :Form)]...
-    vs = enumerate(unique(getindex.(args, 2)))
-    theargs =
-    Dict{Symbol,Symbol}(
-        [v => Symbol("T$k") for (k,v) in vs]
-    )
-    # ...[(Scalar=>:T1, :Form=>:T2)]
-
-    # reassociate vars with their BasicSymbolic Generic Types
-    binding = map(args) do (var, type)
-        (var, :(BasicSymbolic{$(theargs[type])}))
-    end
-    newargs = [:($(x[1])::$(x[2])) for x in binding]
-    constraints = [:($T<:DECType) for T in values(theargs)]
-    innerargs = [:(Sort($T)) for T in values(theargs)]
-
-    push!(result.args,
-          quote
-              @nospecialize
-              function $(esc(f))($(newargs...)) where $(constraints...)
-                  s = $(esc(f))($(innerargs...))
-                  SymbolicUtils.Term{Number(s)}($(esc(f)), [$(getindex.(binding, 1)...)])
-              end
-          end)
-
-    return result
-end
-export @register
-
-end
diff --git a/src/symbolictheoryutils.jl b/src/symbolictheoryutils.jl
new file mode 100644
index 0000000..b6448eb
--- /dev/null
+++ b/src/symbolictheoryutils.jl
@@ -0,0 +1,161 @@
+using MLStyle
+using SymbolicUtils
+using SymbolicUtils: Symbolic, BasicSymbolic, FnType, Sym
+
+abstract type Quantity <: Number end
+export Quantity
+
+"""
+Registers a new function
+
+```
+@register foo(S1, S2, ...)::ThDEC begin
+    (body of function)
+end     
+```
+builds
+```
+foo(::Type{S1}, ::Type{S2}, ...) where {S1<:ThDEC, S2<:ThDEC, ...}
+    (body of function)
+end
+```
+as well as
+```
+foo(S1::BasicSymbolic{T1}, S2::BasicSymbolic{T2}, ...) where {T1<:ThDEC, ...}
+    s = foo(T1, T2, ...)
+    SymbolicUtils.Term{s}(foo, [S1, S2, ...])
+end
+```
+
+```
+@register Δ(s::ThDEC) begin
+    @match s begin
+        ::Scalar => error("Invalid")
+        ::VField => error("Invalid")
+        ::Form => ⋆(d(⋆(d(s))))
+    end
+end
+```
+
+Δ(S1, S2) begin
+    @match (S1, S2)
+        
+
+will create an additional method for Δ for operating on BasicSymbolic 
+"""
+macro register(head, body)
+
+    # parse body
+    ph = @λ begin
+        Expr(:call, foo, Expr(:(::), vars..., theory)) => (foo, vars, theory)
+        Expr(:(::), Expr(:call, foo, vars...), theory) => (foo, vars, theory)
+        _ => error("$head")
+    end
+    (f, vars, Theory) = ph(head)
+
+    symbolic_args = [:(::Type{$S}) for S in vars]
+    symbolic_constraints = [:($S<:$Theory) for S in vars]
+    
+    # initialize the result
+    result = quote end
+    
+    # DEFINE TYPE INFERENCE IN THE ThDEC SYSTEM
+    
+    # TODO this just accepts whatever the body is
+    push!(result.args,
+          esc(quote
+                function $f($(symbolic_args...)) where {$(symbolic_constraints...)}
+                    $body
+              end
+          end))
+
+    # CONSTRUCT THE FUNCTION ON BASIC SYMBOLICS
+
+    # ...associate each var (S1) to a generic. this will be used in the
+    # type constraint of the new function.
+    generic_vars = [(v, Symbol("T$k")) for (k,v) in enumerate(vars)]
+
+    # reassociate vars with their BasicSymbolic Generic Types
+    basicsym_bindings = map(generic_vars) do (var, T)
+        (var, :(BasicSymbolic{$T}))
+    end
+
+    # binding type bindings to the basicsymbolics
+    basicsym_args = [:($var::$basicsym_generic) for (var, basicsym_generic) in basicsym_bindings]
+
+    # build constraints
+    constraints_expr = [:($T<:$Theory) for T in getindex.(generic_vars, 2)]
+ 
+    push!(result.args,
+          esc(quote
+              @nospecialize
+              function $f($(basicsym_args...)) where {$(constraints_expr...)}
+                  s = $f($(getindex.(generic_vars, 2)...))
+                  SymbolicUtils.Term{s}($f ,[$(getindex.(basicsym_bindings, 1)...)])
+              end
+              export $f
+          end))
+
+    return result
+end
+export @register
+
+function alias(x)
+    error("$x has no aliases")
+end
+
+"""
+Given a tuple of symbols ("aliases") and their canonical name (or "rep"), produces
+for each alias typechecking and nameof methods which call those for their rep.
+Example:
+@alias (d₀, d₁) => d
+"""
+macro alias(body)
+    (rep, aliases) = @match body begin
+        Expr(:call, :(=>), Expr(:tuple, aliases...), rep) => (rep, aliases)
+        _ => error("parse error")
+    end
+    result = quote end
+    foreach(aliases) do alias
+        push!(result.args,
+            esc(quote
+                function $alias(s...)
+                    $rep(s...) 
+                end
+                export $alias
+                Base.nameof(::typeof($alias), s) = Symbol("$alias")
+            end))
+    end
+    result
+end
+export alias
+
+macro see(body)
+    ph = @λ begin
+        Expr(:(=), Expr(:where, Expr(:call, foo, typebindings), params...), 
+                    Expr(:block, body...)) => (foo, ph(typebindings), params, body)
+        Expr(:(::), vars...) => ph.(vars)
+        Expr(:curly, :Type, Expr(:<:, Expr(:curly, type, params...))) => (type, params)
+        s => s
+    end
+    ph(body)
+    quote
+        $foo(arg, s1::B1, s2::B1) where {S1,S2,B1<:BasicSymbolic{S1},B2<:BasicSymbolic{S2}}
+
+    end
+end
+
+@see dim(::Type{<:Form{i,d,s,n}}) where {i,d,s,n} = i
+
+function Base.nameof(::typeof(∧), s1::B1, s2::B2) where {S1,S2,B1<:BasicSymbolic{S1}, B2<:BasicSymbolic{S2}}
+    Symbol("∧$(as_sub(dim(symtype(s1))))$(as_sub(dim(symtype(s2))))")
+end
+
+
+Expr(:=,
+     Expr(:where
+          [Expr(:call
+                foo,
+                Expr(:(::), e...)),
+           params...]),
+     Expr(:block, body...))
diff --git a/test/decasymbolic.jl b/test/decasymbolic.jl
index fbbfc15..15cb4f3 100644
--- a/test/decasymbolic.jl
+++ b/test/decasymbolic.jl
@@ -1,45 +1,45 @@
 using Test
-using DiagrammaticEquations
-using DiagrammaticEquations.ThDEC
+using DiagrammaticEquations.Deca.TheoryDEC
 using DiagrammaticEquations.decapodes
 using SymbolicUtils
-# what space are we working in?
-X = Space(:X, 2)
-lookup = SpaceLookup(X)
+using SymbolicUtils: symtype
 
 # load up some variable variables and expressions
-a, b = @syms a::Real b::Real
-u, v = @syms u::PrimalFormT{0, :X, 2} du::PrimalFormT{1, :X, 2}
-ω, η = @syms ω::PrimalFormT{1, :X, 2} η::DualFormT{2, :X, 2}
-ϕ, ψ = @syms ϕ::PrimalVFT{:X, 2} ψ::DualVFT{:X, 2}
+a, b = @syms a::Scalar b::Scalar
+u, v = @syms u::PrimalForm{0, :X, 2} du::PrimalForm{1, :X, 2}
+ω, η = @syms ω::PrimalForm{1, :X, 2} η::DualForm{2, :X, 2}
+ϕ, ψ = @syms ϕ::PrimalVF{:X, 2} ψ::DualVF{:X, 2}
 # TODO would be nice to pass the space globally to avoid duplication
 
 @testset "Term Construction" begin
-  
+ 
+    # TODO implement symtype
     # test conversion to underlying type
-    @test Sort(a) == Scalar()
-    @test Sort(u) == PrimalForm(0, X)
-    @test Sort(ω) == PrimalForm(1, X)
-    @test Sort(η) == DualForm(2, X)
-    @test Sort(ϕ) == PrimalVF(X)
-    @test Sort(ψ) == DualVF(X)
+    @test symtype(a) == Scalar
+    @test symtype(u) == PrimalForm{0, :X, 2}
+    @test symtype(ω) == PrimalForm{1, :X, 2}
+    @test symtype(η) == DualForm{2, :X, 2}
+    @test symtype(ϕ) == PrimalVF{:X, 2}
+    @test symtype(ψ) == DualVF{:X, 2}
 
-    @test_throws ThDEC.SortError ThDEC.♯(u)
+    @test symtype(u ∧ ω) == PrimalForm{1, :X, 2}
+    @test symtype(ω ∧ ω) == PrimalForm{2, :X, 2}
+    # @test_throws ThDEC.SortError ThDEC.♯(u)
 
     # test unary operator conversion to decaexpr
-    @test Term(1) == DiagrammaticEquations.decapodes.Lit(Symbol("1"))
+    @test Term(1) == Lit(Symbol("1"))
     @test Term(a) == Var(:a)
-    @test Term(ThDEC.∂ₜ(u)) == Tan(Var(:u))
-    @test Term(ThDEC.⋆(ω)) == App1(:⋆₁, Var(:ω))
-    @test_broken Term(ThDEC.♭(ψ)) == App1(:♭s, Var(:ψ)) 
+    @test Term(∂ₜ(u)) == Tan(Var(:u))
+    @test Term(⋆(ω)) == App1(:⋆₁, Var(:ω))
+    # @test_broken Term(ThDEC.♭(ψ)) == App1(:♭s, Var(:ψ)) 
     # @test Term(DiagrammaticEquations.ThDEC.♯(du))
     
-    @test_throws ThDEC.SortError ThDEC.⋆(ϕ)
+    # @test_throws ThDEC.SortError ThDEC.⋆(ϕ)
     
     # test binary operator conversion to decaexpr
     @test Term(a + b) == Plus(Term[Var(:a), Var(:b)])
-    @test Term(a * b) == DiagrammaticEquations.decapodes.Mult(Term[Var(:a), Var(:b)])
-    @test Term(ThDEC.:∧(ω, du)) == App2(:∧₁₁, Var(:ω), Var(:du)) 
+    @test Term(a * b) == Mult(Term[Var(:a), Var(:b)])
+    @test Term(ω ∧ du) == App2(:∧₁₁, Var(:ω), Var(:du)) 
 
 end
 
diff --git a/test/klausmeier.jl b/test/klausmeier.jl
index 9c88e46..54fdaee 100644
--- a/test/klausmeier.jl
+++ b/test/klausmeier.jl
@@ -1,10 +1,10 @@
 using DiagrammaticEquations
 using DiagrammaticEquations.SymbolicUtilsInterop
-
+#
 using Test
 using MLStyle
 using SymbolicUtils
-using SymbolicUtils: BasicSymbolic
+using SymbolicUtils: BasicSymbolic, symtype
 
 # See Klausmeier Equation 2.a
 Hydrodynamics = @decapode begin
@@ -42,6 +42,8 @@ Phytodynamics = parse_decapode(quote
   ∂ₜ(n) == w - m*n + Δ(n)
 end)
 
+@test_broken DecaSymbolic(lookup, Phytodynamics)
+
 import .ThDEC: d, ⋆, SortError
 
 @register Δ(s::Sort) begin
@@ -55,6 +57,11 @@ end
 ω, = @syms ω::PrimalFormT{1, :X, 2}
 
 @test Δ(PrimalForm(1, X)) == PrimalForm(1, X)
-@test Δ(ω) |> typeof == BasicSymbolic{PrimalFormT{1, :X, 2}}
+@test symtype(Δ(ω)) == PrimalFormT{1, :X, 2}
+
+# TODO propagating module information is suited for a macro
+symbmodel = DecaSymbolic(lookup, Phytodynamics, Main)
+
+DecaExpr(symbmodel)
+
 
-DecaSymbolic(lookup, Phytodynamics)