diff --git a/.gitignore b/.gitignore
index 3629a223..5d6c467f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,6 +7,8 @@
 # Files generated by invoking Julia with --track-allocation
 *.jl.mem
 
+lcov.info
+
 # System-specific files and directories generated by the BinaryProvider and BinDeps packages
 # They contain absolute paths specific to the host computer, and so should not be committed
 deps/deps.jl
diff --git a/docs/src/concepts/scopes.md b/docs/src/concepts/scopes.md
index ce68e78c..610614fc 100644
--- a/docs/src/concepts/scopes.md
+++ b/docs/src/concepts/scopes.md
@@ -2,17 +2,26 @@
 
 Design rationale:
 
-Namespacing should be first class. This doesn't play nicely with deBruijn
-levels; we don't want to do a bunch of math to convert between flattened and
-unflattened versions of contexts. There is an accepted solution to the problem
-of organizing names: use refs! Mathematically speaking, a ref is just a list
+Namespacing, i.e. references which look like `britain.economy.GDP`, should be
+first class. This doesn't play nicely with the internal representation of names
+via [deBruijn levels](https://en.wikipedia.org/wiki/De_Bruijn_index); we don't
+want to do a bunch of math to convert between flattened and nested versions
+of contexts. Conceptually, we should then switch our identifiers to be *lists*
 of deBruijn levels.
 
-However, deBruijn levels are unfriendly for users; we want to be able to give
-names to our variables!
+But there are also significant subtleties in the translation between named and
+nameless representations of identifiers. Also in practice if we are referencing
+something that might change over time, like a C-set, we don't want to use
+deBruijn levels, because we don't want have to change all of our identifiers
+when we delete something, so in the rest of this I will instead say "local
+identifier" instead of deBruijn level to refer to a nameless representation of
+an identifier.
 
-In general, naming is given by a *relation* between symbols and bindings (as
-referred to by deBruijn levels). Each binding may be associated with zero or
+(the name "local identifier" and also some of this philosophy is taken from
+[chit](https://github.com/davidad/chit))
+
+In general, naming is given by a *relation* between symbols and *bindings* (as
+refered to by local identifiers).  Each binding may be associated with zero or
 more symbols, and each symbol might be associated with zero or more bindings.
 
 We name the failure of this relation to be a bijection in several ways.
@@ -55,11 +64,11 @@ scopes, and the most recent scope "wins".
 
 Parsing turns a `Symbol` into an `Ident`. The `Ident` contains the original
 `Symbol` for printing, but it also contains a reference to a scope via ScopeTag,
-and an deBruijn level within that scope. Thus, the name in the `Ident` is never
-needed for later stages of programatic manipulation.
+and an local identifier ("lid") within that scope. Thus, the name in the `Ident`
+is never needed for later stages of programatic manipulation.
 
 Scopes cache the relation between names and bindings, by providing a way to go
-from binding (as reified by deBruijn level) to a set of aliases with
+from binding (as reified by local identifier) to a set of aliases with
 distinguished primary alias, and to go from name to the set of bindings that
 have that name that we need to disambiguate between in the case of an overload.
 
diff --git a/src/models/GATExprUtils.jl b/src/models/GATExprUtils.jl
new file mode 100644
index 00000000..91d713c0
--- /dev/null
+++ b/src/models/GATExprUtils.jl
@@ -0,0 +1,104 @@
+""" Rewriting for GAT expressions.
+
+The current content of this module exists purely for backwards compatibility
+with the existing rewriting in Catlab; the more advanced implementation uses
+e-graphs and works with AlgTerms instead of GATExprs.
+"""
+module GATExprUtils
+export associate, associate_unit_inv, associate_unit,
+  distribute_unary, involute, normalize_zero
+
+using ..SymbolicModels
+
+#Warning: assumes expr has only two args!
+""" Simplify associative binary operation.
+
+Maintains the normal form `op(e1,e2,...)` where `e1`,`e2`,... are expressions
+that are *not* applications of `op()`
+"""
+function associate(expr::E)::E where E <: GATExpr
+  op, e1, e2 = head(expr), first(expr), last(expr)
+  args1 = head(e1) == op ? args(e1) : [e1]
+  args2 = head(e2) == op ? args(e2) : [e2]
+  E([args1; args2], gat_type_args(expr))
+end
+
+""" Simplify associative binary operation with unit.
+
+Reduces a freely generated (typed) monoid to normal form.
+"""
+function associate_unit(expr::GATExpr, unit::Function)::GATExpr
+  e1, e2 = first(expr), last(expr)
+  if (head(e1) == nameof(unit)) e2
+  elseif (head(e2) == nameof(unit)) e1
+  else associate(expr) end
+end
+
+""" Simplify associative binary operation with unit and inverses.
+"""
+function associate_unit_inv(expr::E, unit::Function,
+                            inverse::Function)::GATExpr where E <: GATExpr
+  op, e1, e2 = head(expr), first(expr), last(expr)
+  if (head(e1) == nameof(unit)) e2
+  elseif (head(e2) == nameof(unit)) e1
+  else
+    args1 = head(e1) == op ? args(e1) : [e1]
+    args2 = head(e2) == op ? args(e2) : [e2]
+    while !isempty(args1) && !isempty(args2)
+      l = args1[end]; r = args2[1]
+      if (head(l) == nameof(inverse) && first(l) == r ||
+          head(r) == nameof(inverse) && l == first(r))
+        pop!(args1); popfirst!(args2)
+      else break end
+    end
+    newargs = [args1; args2]
+    # XXX: Assumes that the unit/identity takes exactly one argument, hence this
+    # function will not work for the algebraic theory of groups.
+    if (isempty(newargs)) unit(only(unique(gat_type_args(expr))))
+    elseif (length(newargs) == 1) only(newargs)
+    else E(newargs, gat_type_args(expr)) end
+  end
+end
+
+""" Distribute unary operation over binary operation.
+"""
+function distribute_unary(expr::GATExpr, unary::Function, binary::Function;
+                          unit::Union{Function,Nothing}=nothing,
+                          contravariant::Bool=false)::GATExpr
+  if (head(expr) != nameof(unary)) return expr end
+  @assert length(args(expr)) == 1
+  arg = first(expr)
+  if head(arg) == nameof(binary)
+    binary(map(unary, (contravariant ? reverse : identity)(args(arg)))...)
+  elseif !isnothing(unit) && head(arg) == nameof(unit)
+    arg
+  else
+    expr
+  end
+end
+
+""" Simplify involutive unary operation.
+"""
+function involute(expr::GATExpr)
+  @assert length(args(expr)) == 1
+  arg = first(expr)
+  head(expr) == head(arg) ? first(arg) : expr
+end
+
+"""
+If given GATExpr contains a zero morphism,
+collapse the expression to a single zero morphism.
+"""
+function normalize_zero(expr::E;zname=:zeromap) where E <: GATExpr
+  ztype = E
+  for subexpr in args(expr)
+    if head(subexpr) == zname
+      ztype = typeof(subexpr)
+      s,t = gat_type_args(expr)
+      return ztype([s,t],[s,t])
+    end
+  end
+  expr
+end
+
+end
diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 17306c3b..7e0e957c 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -85,7 +85,7 @@ implements(m::Model, theory_module::Module) =
   all(!isnothing(implements(m, gettag(scope))) for scope in theory_module.THEORY.segments.scopes)
 
 struct TypeCheckFail <: Exception
-  model::Model
+  model::Union{Model, Nothing}
   theory::GAT
   type::Ident
   val::Any
@@ -150,10 +150,13 @@ macro instance(head, model, body)
   # Parse the body into functions defined here and functions defined elsewhere
   functions, ext_functions = parse_instance_body(body)
 
+  oldinstance = isnothing(model)
+
   # Checks that all the functions are defined with the correct types Add default
   # methods for type constructors and type argument accessors if these methods
   # are missing
-  typechecked_functions = typecheck_instance(theory, functions, ext_functions, jltype_by_sort)
+  typechecked_functions =
+    typecheck_instance(theory, functions, ext_functions, jltype_by_sort; oldinstance)
 
   # Adds keyword arguments to the functions, and qualifies them by
   # `theory_module`, i.e. changes `Ob(x) = blah` to `ThCategory.Ob(x; model::M,
@@ -249,11 +252,18 @@ function julia_signature(
   theory::GAT,
   x::Ident,
   termcon::AlgTermConstructor,
-  jltype_by_sort::Dict{AlgSort}
+  jltype_by_sort::Dict{AlgSort};
+  oldinstance=false
 )
+  sortsig = sortsignature(termcon)
+  args = if oldinstance && isempty(sortsig)
+    Expr0[Expr(:curly, :Type, jltype_by_sort[AlgSort(termcon.type)])]
+  else
+    Expr0[jltype_by_sort[sort] for sort in sortsignature(termcon)]
+  end
   JuliaFunctionSig(
     nameof(x),
-    Expr0[jltype_by_sort[sort] for sort in sortsignature(termcon)]
+    args
   )
 end
 
@@ -306,7 +316,8 @@ function typecheck_instance(
   theory::GAT,
   functions::Vector{JuliaFunction},
   ext_functions::Vector{Symbol},
-  jltype_by_sort::Dict{AlgSort}
+  jltype_by_sort::Dict{AlgSort};
+  oldinstance=false,
 )::Vector{JuliaFunction}
   typechecked = JuliaFunction[]
 
@@ -317,7 +328,7 @@ function typecheck_instance(
 
   for x in theory.termcons
     if nameof(x) ∉ ext_functions
-      sig = julia_signature(theory, x, getvalue(theory[x]), jltype_by_sort)
+      sig = julia_signature(theory, x, getvalue(theory[x]), jltype_by_sort; oldinstance)
       if haskey(undefined_signatures, sig)
         error(overload_errormsg)
       end
@@ -359,22 +370,34 @@ function typecheck_instance(
   for f in functions
     sig = parse_function_sig(f)
 
-    sig ∈ keys(undefined_signatures) ||
-      throw(SignatureMismatchError(f.name, toexpr(sig), expected_signatures[f.name]))
+    if !haskey(undefined_signatures, sig)
+      try
+        x = ident(theory; name=f.name)
+      catch e
+        throw(SignatureMismatchError(f.name, toexpr(sig), expected_signatures[f.name]))
+      end
+      judgment = getvalue(theory, x)
+      # We allow overloading for type constructors
+      if !(judgment isa AlgTypeConstructor)
+        throw(SignatureMismatchError(f.name, toexpr(sig), expected_signatures[f.name]))
+      end
 
-    x = undefined_signatures[sig]
+      push!(typechecked, expand_fail(judgment, theory, x, f))
+    else
+      x = undefined_signatures[sig]
 
-    if x isa Ident
-      judgment = getvalue(theory, x)
+      if x isa Ident
+        judgment = getvalue(theory, x)
 
-      if judgment isa AlgTypeConstructor
-        f = expand_fail(judgment, theory, x, f)
+        if judgment isa AlgTypeConstructor
+          f = expand_fail(judgment, theory, x, f)
+        end
       end
-    end
 
-    delete!(undefined_signatures, sig)
+      delete!(undefined_signatures, sig)
 
-    push!(typechecked, f)
+      push!(typechecked, f)
+    end
   end
 
   for (_, n) in undefined_signatures
@@ -427,7 +450,7 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
       Expr(:let, Expr(:(=), :model, :($m.model)), fun.impl)
     )
   else
-    (fun.args, fun.impl)
+    (fun.args, Expr(:let, Expr(:(=), :model, nothing), fun.impl))
   end
 
   JuliaFunction(
diff --git a/src/models/SymbolicModels.jl b/src/models/SymbolicModels.jl
index 26401b5e..37b1a037 100644
--- a/src/models/SymbolicModels.jl
+++ b/src/models/SymbolicModels.jl
@@ -1,53 +1,291 @@
 module SymbolicModels
-export GATExpr, @symbolic_model, SyntaxDomainError
+export GATExpr, @symbolic_model, SyntaxDomainError, head, args, gat_typeof, gat_type_args,
+  functor, to_json_sexpr, parse_json_sexpr,
+  show_sexpr, show_unicode, show_unicode_infix,
+  show_latex, show_latex_infix, show_latex_postfix, show_latex_script
 
+using ...Util
 using ...Syntax
+import ...Syntax: invoke_term
 
 using Base.Meta: ParseError
 using MLStyle
 
+# Data types
+############
+
+""" Base type for expressions in the syntax of a GAT. This is an alternative
+to `AlgTerm` used for backwards compatibility with Catlab.
+
+We define Julia types for each *type constructor* in the theory, e.g., object,
+morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's
+type system does not support dependent types, so the type parameters are
+incorporated in the Julia types. (They are stored as extra data in the
+expression instances.)
+
+The concrete types are structurally similar to the core type `Expr` in Julia.
+However, the *term constructor* is represented as a type parameter, rather than
+as a `head` field. This makes dispatch using Julia's type system more
+convenient.
+"""
 abstract type GATExpr{T} end
 
+head(::GATExpr{T}) where T = T
+args(expr::GATExpr) = expr.args
+Base.first(expr::GATExpr) = first(args(expr))
+Base.last(expr::GATExpr) = last(args(expr))
+gat_typeof(expr::GATExpr) = nameof(typeof(expr))
+gat_type_args(expr::GATExpr) = expr.type_args
+
+
+""" Get name of GAT generator expression as a `Symbol`.
+
+If the generator has no name, returns `nothing`.
+"""
+function Base.nameof(expr::GATExpr{:generator})
+  name = first(expr)
+  isnothing(name) ? nothing : Symbol(name)
+end
+
+function Base.:(==)(e1::GATExpr{T}, e2::GATExpr{S}) where {T,S}
+  T == S && e1.args == e2.args && e1.type_args == e2.type_args
+end
+
+function Base.hash(e::GATExpr, h::UInt)
+  hash(args(e), hash(head(e), h))
+end
+
+function Base.show(io::IO, expr::GATExpr)
+  print(io, head(expr))
+  print(io, "(")
+  join(io, args(expr), ",")
+  print(io, ")")
+end
+
+function Base.show(io::IO, expr::GATExpr{:generator})
+  print(io, first(expr))
+end
+
+function Base.show(io::IO, ::MIME"text/plain", expr::GATExpr)
+  show_unicode(io, expr)
+end
+
+function Base.show(io::IO, ::MIME"text/latex", expr::GATExpr)
+  print(io, "\$")
+  show_latex(io, expr)
+  print(io, "\$")
+end
+
+struct SyntaxDomainError <: Exception
+  constructor::Symbol
+  args::Vector
+end
+
+function Base.showerror(io::IO, exc::SyntaxDomainError)
+  print(io, "Domain error in term constructor $(exc.constructor)(")
+  join(io, exc.args, ",")
+  print(io, ")")
+end
+
+# Syntax
+########
 """
-This module is for backwards compatibility with Catlab's @syntax macro.
+@symbolic_model generates the free model of a theory, generated by
+symbols.
+
+This is backwards compatible with the @syntax macro in Catlab.
+
+One way of thinking about this is that for every type constructor, we
+add an additional term constructor that builds a "symbolic" element
+of that type from any Julia value. This term constructor is called "generator".
+
+An invocation of `@symbolic_model` creates the following.
+
+1. A module with a struct for each type constructor, which has a single type
+parameter `T` and two fields, `args` and `type_args`. Instances of this struct
+are thought of as elements of the type given by the type constructor applied to
+`type_args`. The type parameter refers to the term constructor that was used
+to generate the element, including the special term constructor `:generator`,
+which has as its single argument an `Any`.
+
+For instance, in the theory of categories, we might have the following elements.
+
+```
+using .FreeCategory
+x = Ob{:generator}([:x], [])
+y = Ob{:generator}([:y], [])
+f = Hom{:generator}([:f], [x, y])
+g = Hom{:generator}([:g], [y, x])
+h = Hom{:compose}([f, g], [x, x])
+```
+
+2. Methods inside the module (not exported) for all of the term constructors and
+field accessors (i.e. stuff like `compose, id, dom, codom`), which construct terms.
+
+3. A default instance (i.e., without a model parameter) of the theory using the
+types in this generated model. Methods in this instance can be overridden by
+the body of `@symbolic_model` to perform rewriting for the sake of normalization,
+for instance flattening associative and unital operations.
+
+4. Coercion methods of the type constructors that allow one to introduce generators.
+
+```
+x = ThCategory.Ob(FreeCategory.Ob, :x)
+y = ThCategory.Ob(FreeCategory.Ob, :y)
+f = ThCategory.Hom(:f, x, y)
+```
+
+Note that in both the instance and in these coercion methods, we must give the
+expected type as the first argument when it cannot be infered by the other arguments.
+For instance, instead of
+
+```
+munit() = ...
+```
 
+we have
+
+```
+munit(::Type{FreeSMC.Ob}) = ...
+```
+
+and likewise instead of
+
+```
+ThCategory.Ob(x::Any) = ...
+```
+
+we have
+
+```
+ThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ...
+```
+
+Example:
+
+```julia
 @symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin
+  compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
 end
+```
+
+This generates:
 
 ```julia
 module FreeCategory
-export Ob,Hom
+export Ob, Hom
 using ..__module__
 
-theory() = ThCategory
+const THEORY_MODULE = ThCategory
 
-struct Ob{T} <: ObExpr{T} # T is :generator or a Symbol
+struct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol
   args::Vector
   type_args::Vector{GATExpr}
 end
 
-struct Hom{T} <: HomExpr{T}
+struct Hom{T} <: __module__.HomExpr{T}
   args::Vector
   type_args::Vector{GATExpr}
 end
 
+dom(x::Hom) = x.type_args[1]
+
+codom(x::Hom) = x.type_args[2]
+
+function compose(f::Hom, g::Hom; strict=true)
+  if strict && !(codom(f) == dom(g))
+    throw(SyntaxDomainError(:compose, [f, g]))
+  end
+  Hom{:compose}([f, g], [dom(f), codom(g)])
+end
+
+function id(x::Ob)
+  Ob{:id}([x], [x, x])
+end
+end
+
 # default implementations 
 
-function ThCategory.dom(x::Hom)::Ob
-  x.type_args[1]
+function ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob
+  FreeCategory.dom(x)
 end
 
-function Ob(::Typ{Ob}, __value__::Any)::Ob
-  Ob{:generator}([__value__], [])
+function ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob
+  FreeCategory.Ob{:generator}([__value__], [])
 end
 
-function ThCategory.id(A::Ob)::Hom
-  Hom{:id}([A], [A, A])
+function ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom
+  FreeCategory.id(A)
 end
 
-end #module
+function ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true)
+  associate_unit(FreeCategory.compose(f, g; strict), id)
+end
 ```
 """
+macro symbolic_model(decl, theoryname, body)
+  # Part 0: Parsing input
+  
+  theory = macroexpand(__module__, :($theoryname.@theory))
+  
+  (name, abstract_types) = @match decl begin
+    Expr(:curly, name, abstract_types...) => (name, abstract_types)
+    _ => throw(ParseError("Ill-formed head of @symbolic_model $decl"))
+  end
+
+  overrides = Dict{Ident, JuliaFunction}()
+
+  if !isnothing(body)
+    body.head == :block || error("expected a block as the body of @symbolic_model")
+
+    for line in body.args
+      if line isa LineNumberNode
+        continue
+      end
+      f = parse_function(line)
+      juliasig = parse_function_sig(f)
+      gatsig = AlgSort.(idents(theory; name=juliasig.types))
+      x = ident(theory; name=f.name, sig=gatsig)
+      overrides[x] = f
+    end
+  end
+
+  theorymodule = :($__module__.$theoryname)
+
+  # Part 1: Generating structs
+
+  module_structs = symbolic_structs(theory, abstract_types, __module__)
+  
+  # Part 2: Generating internal methods
+
+  module_methods = [internal_accessors(theory)..., 
+                    internal_constructors(theory)...]
+
+  module_decl = :(module $(esc(name))
+    export $(nameof.(typecons(theory))...)
+    using ..($(nameof(__module__)))
+    import ..($(nameof(__module__))): $theoryname
+    const $(esc(:THEORY_MODULE)) = $(esc(theoryname))
+
+    $(module_structs...)
+    $(generate_function.(module_methods)...)
+  end)
+
+  # Part 3: Generating instance of theory
+  theory_overloads = symbolic_instance_methods(theory, theoryname, name, overrides)
+
+  # Part 4: Generating generators.
+
+  # generator_overloads = symbolic_generators(theorymodule, theory)
+  generator_overloads = []
+
+  Expr(
+    :toplevel,
+    module_decl,
+    :(Core.@__doc__ $(esc(name))),
+    esc.(generate_function.([theory_overloads; generator_overloads]))...,
+  )
+end
 
 function symbolic_struct(name, abstract_type, parentmod)::Expr
   quote
@@ -59,105 +297,403 @@ function symbolic_struct(name, abstract_type, parentmod)::Expr
 end
 
 function symbolic_structs(theory::GAT, abstract_types, parentmod)::Vector{Expr}
-  Expr[
+  map(zip(theory.typecons, abstract_types)) do (X, abstract_type)
     symbolic_struct(nameof(X), abstract_type, parentmod)
-    for (X, abstract_type) in zip(theory.typecons, abstract_types)
-  ]
+  end
 end
 
-function symbolic_accessor(theoryname, argname, typename, rettypename, argindex, parentmod)
-  quote
-    function $parentmod.$theoryname.$argname(x::$(esc(typename)))::$(rettypename)
-      x.type_args[$argindex]
+function typename(theory::GAT, type::AlgType; parentmod=nothing)
+  name = nameof(sortname(theory, type))
+  if !isnothing(parentmod)
+    Expr(:(.), parentmod, QuoteNode(name))
+  else
+    esc(name)
+  end
+end
+
+function internal_accessors(theory::GAT)
+  map(typecons(theory)) do X
+    map(enumerate(getvalue(theory[X]).args)) do (i, binding)
+      JuliaFunction(
+        name=esc(nameof(binding)),
+        args=[:(x::$(esc(nameof(X))))],
+        return_type = typename(theory, getvalue(binding)),
+        impl=:(x.type_args[$i])
+      )
+    end
+  end |> Iterators.flatten
+end
+
+function internal_constructors(theory::GAT)::Vector{JuliaFunction}
+  map(termcons(theory)) do f
+    name = nameof(f)
+    termcon = getvalue(theory, f)
+    args = map(termcon.args) do binding 
+      Expr(:(::), nameof(binding), typename(theory, getvalue(binding)))
+    end  
+
+    eqs = equations(termcon.args, termcon.localcontext, theory)
+
+    throw_expr = Expr(
+      :call,
+      throw,
+      Expr(
+        :call,
+        SyntaxDomainError,
+        Expr(:quote, name),
+        Expr(:vect, nameof.(termcon.args)...)
+      )
+    )
+
+    check_expr = Expr(
+      :&&,
+      map(filter(exprs -> length(exprs) > 1, collect(values(eqs)))) do exprs
+        cmp_expr = []
+        for e in exprs 
+          append!(cmp_expr, [build_infer_expr(e), esc(:(==))])
+        end
+        Expr(:comparison, cmp_expr[1:end-1]...)
+      end...
+    )
+
+    check_or_error = Expr(:(||), :(!strict), check_expr, throw_expr)
+    exprs = [idents(termcon.args)..., idents(termcon.localcontext)...]
+    expr_lookup = Dict{Ident, Any}(map(exprs) do x 
+      x => build_infer_expr(first(eqs[x]))
+    end)
+
+    build = Expr(
+      :call,
+      Expr(:curly, typename(theory, termcon.type), Expr(:quote, name)),
+      Expr(:vect, nameof.(termcon.args)...),
+      Expr(:ref, GATExpr, compile.(Ref(expr_lookup), termcon.type.args)...)
+    )
+
+    JuliaFunction(
+      ;name=esc(name),
+      args=args,
+      kwargs=[Expr(:kw, :strict, false)],
+      impl=Expr(:block, check_or_error, build)
+    )
+  end
+end 
+
+macro symbolic_model(decl, theoryname)
+  esc(:(@symbolic_model $decl $theoryname $nothing))
+end
+
+"""Julia function for every type constructor, accessor, and term constructor.
+Term constructors can be overwritten by `overrides`. """
+function symbolic_instance_methods(
+  theory::GAT, theorymodule, syntaxname::Symbol, 
+  overrides::Dict{Ident, JuliaFunction})::Vector{JuliaFunction}
+
+  type_con_funs = []
+  accessors_funs = []
+  for type_con_id in typecons(theory) 
+    type_con = getvalue(theory[type_con_id])
+    symgen = symbolic_generator(theorymodule, syntaxname, type_con_id, type_con, theory)
+    push!(type_con_funs, symgen)
+    for binding in type_con.args
+      push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, type_con_id, binding))
+    end
+  end
+
+  type_replacements = [nameof(X) => Expr(:(.), syntaxname, QuoteNode(nameof(X))) for X in typecons(theory)]
+
+  term_con_funs = map(termcons(theory)) do term_con_id
+    if haskey(overrides, term_con_id)
+      replace_symbols(
+        Dict([
+          :new => Expr(:(.), syntaxname, QuoteNode(nameof(term_con_id))); type_replacements
+        ]),
+        setname(overrides[term_con_id], Expr(:(.), theorymodule, QuoteNode(nameof(term_con_id))))
+      )
+    else
+      symbolic_termcon(theorymodule, theory, syntaxname, term_con_id)
     end
   end
+  [type_con_funs..., accessors_funs..., term_con_funs...]
 end
 
-function symbolic_accessors(theoryname, theory::GAT, parentmod)::Vector{Expr}
-  Expr[
-    symbolic_accessor(theoryname, nameof(binding), nameof(X), typename(theory, getvalue(binding)), i, parentmod)
-    for X in typecons(theory) for (i, binding) in enumerate(getvalue(theory[X]).args)
+
+function symbolic_generator(theorymodule, syntaxname, X::Ident, typecon::AlgTypeConstructor, theory::GAT)
+  value_param = gensym(:value)
+  name = nameof(X)
+  args = [
+    Expr(:(::), value_param, Any);
+    [Expr(:(::), nameof(binding), typename(theory, getvalue(binding); parentmod=syntaxname))
+     for binding in typecon.args]
   ]
+
+  if isempty(typecon.args)
+    args = [Expr(:(::), Expr(:curly, Type, Expr(:(.), syntaxname, QuoteNode(name)))); args]
+  end
+  impl = quote 
+    $(Expr(:(.), syntaxname, QuoteNode(name))){:generator}(
+    $(Expr(:vect, value_param, nameof.(typecon.args)...)),
+    $(Expr(:ref, GATExpr, nameof.(typecon.args)...))
+  )
+  end
+  JuliaFunction(name=Expr(:(.), theorymodule, QuoteNode(name)), args=args,impl=impl )
 end
 
-function typename(theory::GAT, type::AlgType)
-  esc(nameof(sortname(theory, type)))
+function symbolic_accessor(theorymodule, theory, name, typecon::Ident, accessor::Binding, )
+  typcon_name = QuoteNode(nameof(typecon))
+  accessor_name = QuoteNode(nameof(accessor))
+  JuliaFunction(
+    name=Expr(:(.), theorymodule, accessor_name),
+    args=[:(x::$(Expr(:(.), name, typcon_name)))],
+    return_type = typename(theory, getvalue(accessor); parentmod=name),
+    impl=Expr(:call, Expr(:(.), name, accessor_name), :x)
+  )
 end
 
-struct SyntaxDomainError <: Exception
-  constructor::Symbol
-  args::Vector
+function symbolic_termcon(theorymodule, theory, syntaxname, termcon_id::Ident )
+  termcon_name = QuoteNode(nameof(termcon_id))
+  termcon = getvalue(theory[termcon_id])
+  return_type = typename(theory, termcon.type; parentmod=syntaxname)
+  args = if !isempty(termcon.args)
+    map(termcon.args) do argbinding
+      type = typename(theory, getvalue(argbinding); parentmod=syntaxname)
+      Expr(:(::), nameof(argbinding), type)
+    end
+  else
+    [Expr(:(::), Expr(:curly, Type, return_type))]
+  end
+  JuliaFunction(
+    name=Expr(:(.), theorymodule, termcon_name),
+    args=args,
+    return_type=return_type,
+    impl=Expr(:call, Expr(:(.), syntaxname, termcon_name), nameof.(termcon.args)...)
+  )
 end
 
-function Base.showerror(io::IO, exc::SyntaxDomainError)
-  print(io, "Domain error in term constructor $(exc.constructor)(")
-  join(io, exc.args, ",")
-  print(io, ")")
+
+# Reflection
+############
+
+function invoke_term(syntax_module::Module, constructor_name::Symbol, args)
+  theory_module = syntax_module.THEORY_MODULE
+  theory = theory_module.THEORY
+  syntax_types = Tuple(getfield(syntax_module, nameof(cons)) for cons in typecons(theory))
+  invoke_term(theory_module, syntax_types, constructor_name, args)
 end
 
-function symbolic_constructor(theoryname, name::Ident, termcon::AlgTermConstructor, theory::GAT, parentmod)
-  eqs = equations(termcon.args, termcon.localcontext, theory)
-  eq_exprs = Expr[]
+""" Name of constructor that created expression.
+"""
+constructor_name(expr::GATExpr) = head(expr)
+constructor_name(expr::GATExpr{:generator}) = gat_typeof(expr)
+
+"""
+Get syntax module of given expression.
+"""
+syntax_module(expr::GATExpr) = parentmodule(typeof(expr))
+
+# Functors
+##########
 
-  theorymodule = :($parentmod.$theoryname)
-  for expr_set in values(eqs)
-    exprs = build_infer_expr.(Ref(theorymodule), [expr_set...])
-    for (a, b) in zip(exprs, exprs[2:end])
-      errexpr = Expr(:call, throw, Expr(:call, GlobalRef(SymbolicModels, :SyntaxDomainError),
-                     Expr(:quote, nameof(name)),
-                     Expr(:vect, nameof.(termcon.args)...)))
+""" Functor from GAT expression to GAT instance.
 
-      push!(eq_exprs, Expr(:(||), Expr(:call, :(==), a, b), errexpr))
+Strictly speaking, we should call these "structure-preserving functors" or,
+better, "model homomorphisms of GATs". But this is a category theory library,
+so we'll go with the simpler "functor".
+
+A functor is completely determined by its action on the generators. There are
+several ways to specify this mapping:
+
+  1. Specify a Julia instance type for each GAT type, using the required `types`
+     tuple. For this to work, the generator constructors must be defined for the
+     instance types.
+
+  2. Explicitly map each generator term to an instance value, using the
+     `generators` dictionary.
+
+  3. For each GAT type (e.g., object and morphism), specify a function mapping
+     generator terms of that type to an instance value, using the `terms`
+     dictionary.
+
+The `terms` dictionary can also be used for special handling of non-generator
+expressions. One use case for this capability is defining forgetful functors,
+which map non-generators to generators.
+
+FIXME
+"""
+function functor(types::Tuple, expr::GATExpr;
+                 generators::AbstractDict=Dict(), terms::AbstractDict=Dict())
+  # Special case: look up a specific generator.
+  if head(expr) == :generator && haskey(generators, expr)
+    return generators[expr]
+  end
+
+  # Special case: look up by type of term (usually a generator).
+  name = constructor_name(expr)
+  if haskey(terms, name)
+    return terms[name](expr)
+  end
+
+  # Otherwise, we need to call a term constructor (possibly for a generator).
+  # Recursively evalute the arguments.
+  term_args = []
+  for arg in args(expr)
+    if isa(arg, GATExpr)
+      arg = functor(types, arg; generators=generators, terms=terms)
     end
+    push!(term_args, arg)
+  end
+
+  # Invoke the constructor in the codomain category!
+  theory_module = syntax_module(expr).THEORY_MODULE
+  invoke_term(theory_module, types, name, term_args)
+end
+
+# Serialization
+###############
+
+""" Serialize expression as JSON-able S-expression.
+
+The format is an S-expression encoded as JSON, e.g., "compose(f,g)" is
+represented as ["compose", f, g].
+"""
+function to_json_sexpr(expr::GATExpr; by_reference::Function = x->false)
+  if head(expr) == :generator && by_reference(first(expr))
+    to_json_sexpr(first(expr))
+  else
+    [ string(constructor_name(expr));
+      [ to_json_sexpr(arg; by_reference=by_reference) for arg in args(expr) ] ]
   end
+end
+to_json_sexpr(x::Union{Bool,Real,String,Nothing}; kw...) = x
+to_json_sexpr(x; kw...) = string(x)
+
+""" Deserialize expression from JSON-able S-expression.
 
-  expr_lookup = Dict{Reference, Any}(
-    [Reference(x) => build_infer_expr(theorymodule, first(eqs[x]))
-     for x in [idents(termcon.args)..., idents(termcon.localcontext)...]]
+If `symbols` is true (the default), strings are converted to symbols.
+"""
+function parse_json_sexpr(syntax_module::Module, sexpr;
+    parse_head::Function = identity,
+    parse_reference::Function = x->error("Loading terms by name is disabled"),
+    parse_value::Function = identity,
+    symbols::Bool = true,
+  )
+  theory_module = syntax_module.THEORY_MODULE
+  theory = theory_module.THEORY
+  type_lens = Dict(
+    nameof(binding) => length(getvalue(binding).args) for binding in [theory[tc] for tc in typecons(theory)]
   )
 
-  quote
-    function $theorymodule.$(nameof(name))(
-      $([Expr(:(::), nameof(binding), typename(theory, getvalue(binding))) for binding in termcon.args]...)
-    )
-      $(eq_exprs...)
-      $(typename(theory, termcon.type)){$(Expr(:quote, nameof(name)))}(
-        $(Expr(:vect, nameof.(termcon.args)...)),
-        $(Expr(:ref, GlobalRef(SymbolicModels, :GATExpr),
-          [compile(theorymodule, expr_lookup, arg) for arg in termcon.type.args]...))
-      )
+  function parse_impl(sexpr::Vector, ::Type{Val{:expr}})
+    name = Symbol(parse_head(symbols ? Symbol(sexpr[1]) : sexpr[1]))
+    nargs = length(sexpr) - 1
+    args = map(enumerate(sexpr[2:end])) do (i, arg)
+      arg_kind = ((i == 1 && get(type_lens, name, nothing) == nargs-1) ||
+                  arg isa Union{Bool,Number,Nothing}) ? :value : :expr
+      parse_impl(arg, Val{arg_kind})
     end
+    invoke_term(syntax_module, name, args)
   end
-end
+  parse_impl(x, ::Type{Val{:value}}) = parse_value(x)
+  parse_impl(x::String, ::Type{Val{:expr}}) =
+    parse_reference(symbols ? Symbol(x) : x)
+  parse_impl(x::String, ::Type{Val{:value}}) =
+    parse_value(symbols ? Symbol(x) : x)
 
-function symbolic_constructors(theoryname, theory::GAT, parentmod)::Vector{Expr}
-  Expr[symbolic_constructor(theoryname, x, getvalue(theory[x]), theory, parentmod) for x in termcons(theory)]
+  parse_impl(sexpr, Val{:expr})
 end
 
-macro symbolic_model(decl, theoryname, body)
-  theory = macroexpand(__module__, :($theoryname.@theory))
-  
-  (name, abstract_types) = @match decl begin
-    Expr(:curly, name, abstract_types...) => (name, abstract_types)
-    _ => throw(ParseError("Ill-formed head of @symbolic_model $decl"))
+# Pretty-print
+##############
+
+""" Show the syntax expression as an S-expression.
+
+Cf. the standard library function `Meta.show_sexpr`.
+"""
+show_sexpr(expr::GATExpr) = show_sexpr(stdout, expr)
+
+function show_sexpr(io::IO, expr::GATExpr)
+  if head(expr) == :generator
+    print(io, repr(first(expr)))
+  else
+    print(io, "(")
+    join(io, [string(head(expr));
+              [sprint(show_sexpr, arg) for arg in args(expr)]], " ")
+    print(io, ")")
   end
+end
 
-  structs = symbolic_structs(theory, abstract_types, __module__)
+""" Show the expression in infix notation using Unicode symbols.
+"""
+show_unicode(expr::GATExpr) = show_unicode(stdout, expr)
+show_unicode(io::IO, x::Any; kw...) = show(io, x)
+
+function show_unicode(io::IO, expr::GATExpr; kw...)
+  # By default, show in prefix notation.
+  print(io, head(expr))
+  print(io, "{")
+  join(io, [sprint(show_unicode, arg) for arg in args(expr)], ",")
+  print(io, "}")
+end
 
-  accessors = symbolic_accessors(theoryname, theory, __module__)
+function show_unicode(io::IO, expr::GATExpr{:generator}; kw...)
+  print(io, first(expr))
+end
 
-  constructors = symbolic_constructors(theoryname, theory, __module__)
+function show_unicode_infix(io::IO, expr::GATExpr, op::String;
+                            paren::Bool=false)
+  show_unicode_paren(io, expr) = show_unicode(io, expr; paren=true)
+  if (paren) print(io, "(") end
+  join(io, [sprint(show_unicode_paren, arg) for arg in args(expr)], op)
+  if (paren) print(io, ")") end
+end
 
-  Expr(:toplevel,
-    :(module $(esc(name))
-      using ..($(nameof(__module__)))
-      $(structs...)
+""" Show the expression in infix notation using LaTeX math.
 
-      $(accessors...)
+Does *not* include `\$` or `\\[begin|end]{equation}` delimiters.
+"""
+show_latex(expr::GATExpr) = show_latex(stdout, expr)
+show_latex(io::IO, sym::Symbol; kw...) = print(io, sym)
+show_latex(io::IO, x::Any; kw...) = show(io, x)
+
+function show_latex(io::IO, expr::GATExpr; kw...)
+  # By default, show in prefix notation.
+  print(io, "\\mathop{\\mathrm{$(head(expr))}}")
+  print(io, "\\left[")
+  join(io, [sprint(show_latex, arg) for arg in args(expr)], ",")
+  print(io, "\\right]")
+end
 
-      $(constructors...)
-    end)
-  )
+function show_latex(io::IO, expr::GATExpr{:generator}; kw...)
+  # Try to be smart about using text or math mode.
+  content = string(first(expr))
+  if all(isletter, content) && length(content) > 1
+    print(io, "\\mathrm{$content}")
+  else
+    print(io, content)
+  end
+end
+
+function show_latex_infix(io::IO, expr::GATExpr, op::String;
+                          paren::Bool=false, kw...)
+  show_latex_paren(io, expr) = show_latex(io, expr, paren=true)
+  sep = op == " " ? op : " $op "
+  if (paren) print(io, "\\left(") end
+  join(io, [sprint(show_latex_paren, arg) for arg in args(expr)], sep)
+  if (paren) print(io, "\\right)") end
+end
+
+function show_latex_postfix(io::IO, expr::GATExpr, op::String; kw...)
+  @assert length(args(expr)) == 1
+  print(io, "{")
+  show_latex(io, first(expr), paren=true)
+  print(io, "}")
+  print(io, op)
+end
+
+function show_latex_script(io::IO, expr::GATExpr, head::String;
+                           super::Bool=false, kw...)
+  print(io, head, super ? "^" : "_", "{")
+  join(io, [sprint(show_latex, arg) for arg in args(expr)], ",")
+  print(io, "}")
 end
 
 end
diff --git a/src/models/module.jl b/src/models/module.jl
index 1a9c9b6c..d44fc8d2 100644
--- a/src/models/module.jl
+++ b/src/models/module.jl
@@ -4,8 +4,10 @@ using Reexport
 
 include("ModelInterface.jl")
 include("SymbolicModels.jl")
+include("GATExprUtils.jl")
 
 @reexport using .ModelInterface
 @reexport using .SymbolicModels
+@reexport using .GATExprUtils
 
 end
diff --git a/src/stdlib/models/ScopeTrees.jl b/src/stdlib/models/ScopeTrees.jl
deleted file mode 100644
index 5625e170..00000000
--- a/src/stdlib/models/ScopeTrees.jl
+++ /dev/null
@@ -1,137 +0,0 @@
-module ScopeTrees
-export ScopeTree, ScopeLeaf, ScopeNode, pure, wrap, unwrap, isleaf, isnode,
-  ScopeTreeHom, ScopeTreeC
-
-using ....Syntax, ....Models, ...StdTheories
-using MLStyle
-
-using StructEquality
-
-# Scope Tree
-############
-
-@data ScopeTree{T} <: HasContext begin
-  ScopeLeaf(T)
-  ScopeNode(Scope{ScopeTree{T}, Nothing})
-end
-
-Scopes.getcontext(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => EmptyContext()
-  ScopeNode(s) => s
-end
-
-pure(x::T) where {T} = ScopeLeaf{T}(x)
-
-wrap(s::Scope{ScopeTree{T}}) where {T} = ScopeNode{T}(s)
-
-wrap(p::Pair{Symbol,<:ScopeTree{T}}...) where {T} = wrap(Scope{ScopeTree{T}}(p...))
-
-unwrap(t::ScopeTree) = @match t begin
-  ScopeLeaf(x) => x
-  ScopeNode(s) => s
-end
-
-isleaf(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => true
-  ScopeNode(_) => false
-end
-
-isnode(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => false
-  ScopeNode(_) => true
-end
-
-Base.keys(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => [Reference()]
-  ScopeNode(s) => vcat([map(r -> Reference(x, r), keys(t)) for (x,t) in identvalues(s)]...)
-end
-
-Base.haskey(t::ScopeTree, k::Reference) = @match t begin
-  ScopeLeaf(_) && if isempty(k) end => true
-  ScopeNode(s) && if !isempty(k) && hasident(s, first(k)) end => haskey(getvalue(s, first(k)), rest(k))
-  _ => false
-end
-
-Base.getindex(t::ScopeTree, k::Reference) = @match t begin
-  ScopeLeaf(x) && if isempty(k) end => x
-  ScopeNode(s) && if !isempty(k) && hasident(s, first(k)) end => getvalue(s, first(k))[rest(k)]
-  _ => throw(KeyError(k))
-end
-
-@struct_hash_equal struct ScopeTreeHom{S}
-  map::Dict{Reference, Tuple{Reference, S}}
-end
-
-function ScopeTreeHom(pairs::Pair{Reference, Tuple{Reference, S}}...) where {S}
-  ScopeTreeHom{S}(Dict{Reference, Tuple{Reference, S}}(pairs...))
-end
-
-@struct_hash_equal struct ScopeTreeC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ScopeTree{ObT}, ScopeTreeHom{HomT}}}
-  c::C
-end
-
-using .ThCategory
-
-function seteq(x, y)
-  (x ⊆ y) && (y ⊆ x)
-end
-
-@instance ThCategory{ScopeTree{ObT}, ScopeTreeHom{HomT}} (;model::ScopeTreeC{ObT, HomT, C}) where {ObT, HomT, C} begin
-  function Ob(t::ScopeTree{ObT})
-    @match t begin
-      ScopeLeaf(x) => try
-        Ob(x; model=model.c)
-      catch e
-        @fail ("leaf failed", e)
-      end
-      ScopeNode(s) => begin
-        for (x, t′) in identvalues(s)
-          try
-            Ob(t′; model)
-          catch e
-            @fail ("branch $x failed", e)
-          end
-        end
-      end
-    end
-    t
-  end
-
-  function Hom(f::ScopeTreeHom{HomT}, x::ScopeTree{ObT}, y::ScopeTree{ObT})
-    # TODO: report exactly which key was not in
-    seteq(keys(f.map), keys(x)) || @fail "keys of morphism not equal to keys of domain"
-    seteq(first.(values(f.map)), keys(y)) || @fail "values of morphism not equal to keys of codomain"
-    for (i, (j, f₀)) in f.map
-      try
-        Hom(f₀, x[i], y[j]; model=model.c)
-      catch e
-        @fail ("morphism at $i not valid", e)
-      end
-    end
-    f
-  end
-
-  id(x::ScopeTree{ObT}) = ScopeTreeHom{HomT}(Dict(k => (k, id(x[k]; model=model.c)) for k in keys(x)))
-
-  function compose(f::ScopeTreeHom{HomT}, g::ScopeTreeHom{HomT}; context)
-    if !isnothing(context)
-      [:a,:b,:c] ⊂ keys(context) || error("must provide full context or nothing")
-    end
-
-    ScopeTreeHom{HomT}(
-      Dict{Reference, Tuple{Reference, HomT}}(k => begin
-        (k′, f₀) = f.map[k]
-        (k″, g₀) = g.map[k′]
-        localcontext = if !isnothing(context)
-          (a=context.a[k], b=context.b[k′], c=context.c[k″])
-        else
-          nothing
-        end
-        (k″, compose(f₀, g₀; context=localcontext, model=model.c))
-      end
-      for k in keys(f.map))
-    )
-  end
-end
-
-end
diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl
index 1a5f992f..b7613e4e 100644
--- a/src/stdlib/models/module.jl
+++ b/src/stdlib/models/module.jl
@@ -6,14 +6,12 @@ include("FinSets.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Nothings.jl")
-include("ScopeTrees.jl")
 include("GATs.jl")
 
 @reexport using .FinSets
 @reexport using .FinMatrices
 @reexport using .SliceCategories
 @reexport using .Nothings
-@reexport using .ScopeTrees
 @reexport using .GATs
 
 end
diff --git a/src/syntax/ExprInterop.jl b/src/syntax/ExprInterop.jl
index 15a4db6c..de6b0417 100644
--- a/src/syntax/ExprInterop.jl
+++ b/src/syntax/ExprInterop.jl
@@ -69,68 +69,4 @@ function fromexpr(c::Context, e, ::Type{Ident}; sig=nothing)
   end
 end
 
-function reftolist(c::Context, ref::Reference; kw...)
-  symbols = []
-  while !isempty(ref)
-    x = first(ref)
-    push!(symbols, toexpr(c, x; kw...))
-    ref = rest(ref)
-    if !isempty(ref)
-      c = getvalue(c, x)
-    end
-  end
-  symbols
-end
-
-function toexpr(c::Context, ref::Reference; kw...)
-  symbols = reftolist(c, ref; kw...)
-  if isempty(symbols)
-    :(_)
-  else
-    expr = symbols[1]
-    for x in symbols[2:end]
-      expr = Expr(:(.), expr, QuoteNode(x))
-    end
-    expr
-  end
-end
-
-function flattendotexpr(e)
-  syms = Symbol[]
-  while !(e isa Symbol)
-    @match e begin
-      Expr(:(.), e′, QuoteNode(y)) => begin
-        push!(syms, y)
-        e = e′
-      end
-      _ => error("unexpected syntax for reference: $e")
-    end
-  end
-  @match e begin
-    :(_) => nothing
-    x::Symbol => push!(syms, x)
-  end
-  reverse(syms)
-end
-
-function reffromlist(c::Context, syms::AbstractVector{Symbol}; sig=nothing)
-  if isempty(syms)
-    Reference()
-  else
-    x = fromexpr(c, syms[1], Ident; sig)
-    c′ = getvalue(c, x)
-    r = if c′ isa Context
-      reffromlist(c′, @view syms[2:end])
-    else
-      length(syms) == 1 || error("the value of $x is not a context: $(c′)")
-      Reference()
-    end
-    Reference(x, r)
-  end
-end
-
-function fromexpr(c::Context, e, ::Type{Reference}; sig=nothing)
-  reffromlist(c, flattendotexpr(e); sig)
-end
-
 end # module
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index dc38ae93..25450d59 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -33,17 +33,15 @@ One syntax tree to rule all the terms.
 Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant
 """
 @struct_hash_equal struct AlgTerm <: TrmTyp
-  head::Union{Reference, AbstractConstant}
+  head::Union{Ident, AbstractConstant}
   args::Vector{AlgTerm}
-  function AlgTerm(head::Union{Reference, AbstractConstant}, args::Vector{AlgTerm}=EMPTY_ARGS)
+  function AlgTerm(head::Union{Ident, AbstractConstant}, args::Vector{AlgTerm}=EMPTY_ARGS)
     new(head, args)
   end
 end
 
 const EMPTY_ARGS = AlgTerm[]
 
-AlgTerm(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgTerm(Reference(head), args)
-
 """
 Some expr may have already been bound (e.g. by an explicit context) and thus 
 oughtn't be interpreted as `default` type.
@@ -54,22 +52,22 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{AlgTerm}; bound=nothing)
     s::Symbol => begin
       scope = getscope(c, getlevel(c, s))
       ref = if sigtype(scope) == Union{Nothing, AlgSorts}
-        fromexpr(c, s, Reference; sig=AlgSort[])
+        fromexpr(c, s, Ident; sig=AlgSort[])
       else
-        fromexpr(c, s, Reference)
+        fromexpr(c, s, Ident)
       end
       AlgTerm(ref)
     end
     Expr(:call, head, argexprs...) => begin
       args = Vector{AlgTerm}(fromexpr.(Ref(c), argexprs, Ref(AlgTerm)))
       argsorts = AlgSorts(AlgSort.(Ref(c), args))
-      AlgTerm(fromexpr(c, head, Reference; sig=argsorts), args)
+      AlgTerm(fromexpr(c, head, Ident; sig=argsorts), args)
     end
     Expr(:(::), val, type) => 
       AlgTerm(Constant(val, get(bound, val, fromexpr(c, type, AlgType; bound=bound))))
     e::Expr => error("could not parse AlgTerm from $e")
     constant::Constant => AlgTerm(constant)
-    i::Ident => AlgTerm(Reference(i))
+    i::Ident => AlgTerm(i)
   end
 end
 
@@ -81,15 +79,13 @@ One syntax tree to rule all the types.
 `head` must be reference to a `AlgTypeConstructor`
 """
 @struct_hash_equal struct AlgType <: TrmTyp
-  head::Reference
+  head::Ident
   args::Vector{AlgTerm}
-  function AlgType(head::Reference, args::Vector{AlgTerm}=EMPTY_ARGS)
+  function AlgType(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS)
     new(head, args)
   end
 end
 
-AlgType(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgType(Reference(head), args)
-
 """
 Some expr may have already been bound (e.g. by an explicit context) and thus 
 oughtn't be interpreted as `default` type.
@@ -97,9 +93,9 @@ oughtn't be interpreted as `default` type.
 function ExprInterop.fromexpr(c::Context, e, ::Type{AlgType}; bound=nothing)::AlgType
   bound = isnothing(bound) ? Dict{Symbol, AlgType}() : bound
   @match e begin
-    s::Symbol => AlgType(fromexpr(c, s, Reference))
+    s::Symbol => AlgType(fromexpr(c, s, Ident))
     Expr(:call, head, args...) =>
-      AlgType(fromexpr(c, head, Reference), fromexpr.(Ref(c), args, Ref(AlgTerm); bound=bound))
+      AlgType(fromexpr(c, head, Ident), fromexpr.(Ref(c), args, Ref(AlgTerm); bound=bound))
     _ => error("could not parse AlgType from $e")
   end
 end
@@ -139,17 +135,16 @@ A *sort*, which is essentially a type constructor without arguments
 `ref` must be reference to a `AlgTypeConstructor`
 """
 @struct_hash_equal struct AlgSort
-  ref::Reference
+  ref::Ident
 end
 
-AlgSort(i::Ident) = AlgSort(Reference(i))
 AlgSort(t::AlgType) = AlgSort(t.head)
 
 function AlgSort(c::Context, t::AlgTerm)
   if t.head isa AbstractConstant
     AlgSort(t.head.type.head)
   else
-    binding = c[only(t.head)]
+    binding = c[t.head]
     value = getvalue(binding)
     if value isa AlgType
       AlgSort(value.head)
@@ -197,7 +192,7 @@ Throw an error if a the head of an AlgTerm (which refers to a term constructor)
 has arguments of the wrong sort. Returns the sort of the term.
 """
 function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
-  if t.head isa Reference
+  if t.head isa Ident
     judgment = ctx[t.head] |> getvalue
     if judgment isa AlgType
       isempty(t.args) || error("Cannot apply a variable to arguments: $t")
@@ -394,7 +389,7 @@ function allnames(theory::GAT; aliases=false)
 end
 
 function sortname(theory::GAT, type::AlgType)
-  canonicalize(theory, only(type.head))
+  canonicalize(theory, type.head)
 end
 
 Base.issubset(t1::GAT, t2::GAT) = 
@@ -409,11 +404,17 @@ end
 
 const InferExpr = Union{Ident, AccessorApplication}
 
-function build_infer_expr(theorymodule, e::InferExpr)
+function build_infer_expr(e::InferExpr; theorymodule=nothing)
   if e isa Ident
     nameof(e)
   else
-    Expr(:call, :($theorymodule.$(nameof(e.accessor))), build_infer_expr(theorymodule, e.to))
+    name = nameof(e.accessor)
+    accessor = if !isnothing(theorymodule)
+      :($theorymodule.$name)
+    else
+      esc(name)
+    end
+    Expr(:call, accessor, build_infer_expr(e.to; theorymodule))
   end
 end
 
@@ -461,12 +462,12 @@ function equations(args::TypeScope, localcontext::TypeScope, theory::GAT)
     for (i, arg) in enumerate(xtype.args)
       if arg.head isa Constant
         continue
-      elseif first(arg.head) ∈ theory
+      elseif arg.head ∈ theory
         continue
       else
-        @assert first(arg.head) ∈ context
+        @assert arg.head ∈ context
         a = ident(xtypecon.args; lid=LID(i))
-        y = first(arg.head)
+        y = arg.head
         expr′ = AccessorApplication(a, expr)
         push!(to_expand, y => expr′)
       end
@@ -480,18 +481,20 @@ equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]);
   equations(x.args, x.localcontext, theory) 
 end
 
-function compile(theorymodule, expr_lookup::Dict{Reference}, term::AlgTerm)
+function compile(expr_lookup::Dict{Ident}, term::AlgTerm; theorymodule=nothing)
   if term.head isa Constant
     term.head.value
   else
     if haskey(expr_lookup, term.head)
       expr_lookup[term.head]
     else
-      Expr(
-        :call,
-        :($theorymodule.$(nameof(only(term.head)))),
-        [compile(theorymodule, expr_lookup, arg) for arg in term.args]...
-      )
+      name = nameof(term.head)
+      fun = if !isnothing(theorymodule)
+        :($theorymodule.$name)
+      else
+        esc(name)
+      end
+      Expr(:call, fun, [compile(expr_lookup, arg; theorymodule) for arg in term.args]...)
     end
   end
 end
@@ -501,7 +504,7 @@ function TermInCtx(g::GAT, k::Ident)
   tcon = getvalue(g[k])
   lc = argcontext(tcon)
   ids = reverse(reverse(idents(lc))[1:(length(tcon.args))])
-  TermInCtx(lc, AlgTerm(Reference(k), AlgTerm.(ids)))
+  TermInCtx(lc, AlgTerm(k, AlgTerm.(ids)))
 end
 
 """
@@ -526,7 +529,7 @@ we use `equations` which tell us, e.g., that `a = dom(f)`. So we can grab the
 first argument of the *type* of `f` (i.e. grab `x` from `Hom(x,x)`). 
 """
 function infer_type(theory::GAT, t::TermInCtx)
-  head = only(headof(t.trm))
+  head = headof(t.trm)
   if hasident(t.ctx, head) 
     getvalue(t.ctx[head]) # base case
   else
@@ -558,7 +561,7 @@ Take a term constructor and determine terms of its local context.
 This function is mutually recursive with `infer_type`. 
 """ 
 function bind_localctx(theory::GAT, t::TermInCtx)
-  head = only(headof(t.trm))
+  head = headof(t.trm)
 
   tc = getvalue(theory[head])
   eqs = equations(theory, head)
@@ -583,7 +586,7 @@ end
 
 """ Replace idents with AlgTerms. """
 function substitute_term(t::TrmTyp, dic::Dict{Ident,AlgTerm})
-  iden = only(headof(t))
+  iden = headof(t)
   if haskey(dic, iden)
     isempty(t.args) || error("Cannot substitute a term with arguments")
     dic[iden]
@@ -615,7 +618,7 @@ ExprInterop.toexpr(c::Context, term::AlgSort; kw...) =
   ExprInterop.toexpr(c, term.ref; kw...)
 
 ExprInterop.fromexpr(c::Context, e, ::Type{AlgSort}) = 
-  AlgSort(ExprInterop.fromexpr(c, e, Reference))
+  AlgSort(ExprInterop.fromexpr(c, e, Ident))
 
 
 function bindingexprs(c::Context, s::Scope)
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index 55e7891d..a4cb9fea 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -4,7 +4,6 @@ export
   ScopeTagError,
   LID,
   Ident, gettag, getlid, isnamed,
-  Reference, rest,
   Binding, getaliases, getvalue, getsignature, getline, setline,
   Context, getscope, nscopes, getlevel, hasname, hastag,
   HasContext, getcontext,
@@ -171,75 +170,6 @@ rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::Ident) =
     x
   end
 
-# References
-############
-
-"""
-`Reference`
-
-A path of identifiers. We optimize for the (frequent) case where there is only
-one identifier by making this a linked list.
-"""
-@struct_hash_equal struct Reference
-  body::Union{Nothing, Tuple{Ident, Reference}}
-end
-
-function Reference(xs::Ident...)
-  if isempty(xs)
-    Reference(nothing)
-  else
-    Reference(xs[1], Reference(xs[2:end]...))
-  end
-end
-
-function Reference(first::Ident, rest::Reference)
-  Reference((first, rest))
-end
-
-Base.isempty(p::Reference) = isnothing(p.body)
-
-Base.first(p::Reference) = !isempty(p) ? p.body[1] : throw(BoundsError(p, 1))
-
-Base.rest(p::Reference) = !isempty(p) ? p.body[2] : p
-
-function Base.only(p::Reference)
-  if isempty(p)
-    throw(ArgumentError("Reference is empty, must contain exactly 1 element"))
-  end
-  (x, r) = p.body
-  if !isempty(r)
-    throw(ArgumentError("Reference has multiple elements, must contain exactly 1 element"))
-  end
-  x
-end
-
-function Base.show(io::IO, p::Reference)
-  if isempty(p)
-    print(io, "_")
-    return
-  end
-  cur = p
-  show(io, first(cur))
-  while !isempty(rest(cur))
-    cur = rest(cur)
-    id = first(cur)
-    if isnamed(id)
-      print(io, ".")
-      show(io, id)
-    else
-      print(io, "[")
-      print(io, getlid(id))
-      print(io, "]")
-    end
-  end
-end
-
-retag(replacements::Dict{ScopeTag, ScopeTag}, p::Reference) =
-  isempty(p) ? p : Reference(retag(replacements, first(p)), retag(replacements, rest(p)))
-
-rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, p::Reference) =
-  isempty(p) ? p : Reference(rename(tag, replacements, first(p)), rename(tag, replacements, rest(p)))
-
 # Bindings
 ##########
 
@@ -758,7 +688,6 @@ function idents(
 end
 
 Base.getindex(c::Context, x::Ident) = getbinding(getscope(c, x), x)
-Base.getindex(c::Context, x::Reference) = c[only(x)]
 
 getvalue(c::Context, x::Ident) = getvalue(c[x])
 getvalue(c::Context, name::Symbol) = getvalue(c[ident(c; name)])
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index a9bdf063..6522864c 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -1,5 +1,5 @@
 module TheoryInterface
-export @theory, Model
+export @theory, Model, invoke_term
 
 using ..Scopes, ..GATs, ..ExprInterop
 
@@ -97,11 +97,33 @@ macro theory(head, body)
   push!(modulelines, :($(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name))
 
   esc(
-    Expr(:toplevel, :(
-      module $name
-      $(modulelines...)
-      end
-    )))
+    Expr(
+      :toplevel,
+      :(
+        module $name
+        $(modulelines...)
+        end
+      ),
+      :(Core.@__doc__ $(name))
+    )
+  )
+end
+
+function invoke_term(theory_module, types, name, args; model=nothing)
+  theory = theory_module.THEORY
+  method = getproperty(theory_module, name)
+  type_idx = findfirst(==(name), nameof.(typecons(theory)))
+  if !isnothing(type_idx) && length(args) <= 1
+    args = method(types[type_idx], args...)
+  elseif isnothing(model) && isempty(args)
+    termcon = getvalue(theory, ident(theory; name, sig=AlgSort[]))
+    idx = findfirst(==(termcon.type.head), typecons(theory))
+    method(types[idx])
+  elseif isnothing(model)
+    method(args...)
+  else
+    method(WithModel(model), args...)
+  end
 end
 
 end
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 131d5d70..544c1b84 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -40,7 +40,7 @@ dom(f::AbsTheoryMap)::GAT = f.dom # assume this exists by default
 codom(f::AbsTheoryMap)::GAT = f.codom # assume this exists by default
 
 function compose(f::AbsTheoryMap, g::AbsTheoryMap)
-  typmap = Dict(k => typemap(g)[only(v.ref)] for (k,v) in pairs(typemap(f)))
+  typmap = Dict(k => typemap(g)[v.ref] for (k,v) in pairs(typemap(f)))
   trmmap = Dict(k => g(v) for (k, v) in pairs(termmap(f)))
   TheoryMap(dom(f), codom(g), typmap, trmmap)
 end
@@ -63,8 +63,8 @@ function (f::AbsTheoryMap)(ctx::TypeScope)
   scope = TypeScope()
   cache = Dict{Symbol, AlgTerm}()
   for b in ctx
-    argnames = nameof.(only.(headof.(b.value.args)))
-    val = AlgType(f(only(b.value.head)).ref, AlgTerm[cache[a] for a in argnames])
+    argnames = nameof.(headof.(b.value.args))
+    val = AlgType(f(b.value.head).ref, AlgTerm[cache[a] for a in argnames])
     new_binding = Binding{AlgType, Nothing}(b.primary, b.aliases, val, b.sig)
     cache[nameof(b)] = AlgTerm(Ident(gettag(scope), LID(length(scope)+1), 
                                nameof(new_binding)))
@@ -81,7 +81,7 @@ end
 """ Map a term `t` in context `c` along `f`. """
 function (f::AbsTheoryMap)(ctx::TypeScope, t::AlgTerm, fctx=nothing)::AlgTerm
   fctx = isnothing(fctx) ? f(ctx) : fctx
-  head = only(headof(t))
+  head = headof(t)
   if hasident(ctx, head)
     retag(Dict(gettag(ctx)=>gettag(fctx)), t) # term is already in the context
   else 
@@ -182,7 +182,7 @@ TODO: check that it is well-formed, axioms are preserved.
     # Check type constructors are coherent
     for (k, v) in pairs(typmap)
       f_args = f(argcontext(getvalue(dom[k])))
-      arg_fs = argcontext(getvalue(codom[only(v.ref)]))
+      arg_fs = argcontext(getvalue(codom[v.ref]))
       err = "Bad type map $k => $v ($f_args != $arg_fs)"
       Scopes.equiv(f_args, arg_fs) || error(err)
     end
@@ -223,7 +223,7 @@ function fromexpr(dom::GAT, codom::GAT, e, ::Type{TheoryMap})
       key = fromexpr(dom, e1, TermInCtx)
 
       # Check that dom ctx is the same (modulo retagging) with term argcontext
-      khead = only(key.trm.head)
+      khead = key.trm.head
       a_c = argcontext(getvalue(dom[khead]))
       Scopes.equiv(key.ctx, a_c) || error("CONTEXT ERROR\n$(key.ctx)\n$a_c")
 
diff --git a/src/util/MetaUtils.jl b/src/util/MetaUtils.jl
index 5c15ec56..e6708a0f 100644
--- a/src/util/MetaUtils.jl
+++ b/src/util/MetaUtils.jl
@@ -1,7 +1,7 @@
 """ General-purpose tools for metaprogramming in Julia.
 """
 module MetaUtils
-export JuliaFunction, setimpl,
+export JuliaFunction, setimpl, setname,
   JuliaFunctionSig, parse_docstring, parse_function,
   parse_function_sig, generate_docstring, generate_function,
   replace_symbols, strip_lines,
@@ -29,11 +29,19 @@ const Expr0 = Union{Symbol,Expr}
                          return_type=nothing, impl=nothing, doc=nothing)
     new(name, args, kwargs, whereparams, return_type, impl, doc)
   end
+
+  function JuliaFunction(;name::Expr0, args=Expr0[], kwargs=Expr0[], whereparams=Expr0[],
+                         return_type=nothing, impl=nothing, doc=nothing)
+    new(name, args, kwargs, whereparams, return_type, impl, doc)
+  end
 end
 
 setimpl(f::JuliaFunction, impl) =
   JuliaFunction(f.name, f.args, f.kwargs, f.whereparams, f.return_type, impl, f.doc)
 
+setname(f::JuliaFunction, name) =
+  JuliaFunction(name, f.args, f.kwargs, f.whereparams, f.return_type, f.impl, f.doc)
+
 @struct_hash_equal struct JuliaFunctionSig
   name::Expr0
   types::Vector{Expr0}
@@ -155,7 +163,7 @@ end
 """
 function replace_symbols(bindings::AbstractDict, f::JuliaFunction)::JuliaFunction
   JuliaFunction(
-    replace_symbols(bindings, f.name),
+    f.name,
     replace_symbols.(Ref(bindings), f.args),
     replace_symbols.(Ref(bindings), f.kwargs),
     replace_symbols.(Ref(bindings), f.whereparams),
diff --git a/test/cover.jl b/test/cover.jl
new file mode 100644
index 00000000..35325e71
--- /dev/null
+++ b/test/cover.jl
@@ -0,0 +1,12 @@
+using Pkg, Coverage
+
+bashit(str) = run(`bash -c "$str"`)
+
+Pkg.test("GATlab"; coverage=true)
+coverage = process_folder()
+open("lcov.info", "w") do io
+    LCOV.write(io, coverage)
+end;
+bashit("find . -name *.cov -delete")
+
+@show get_summary(coverage)
\ No newline at end of file
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 566984c8..76fcc476 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -28,9 +28,11 @@ end
   dom(f::Vector{Int}) = length(f)
 end
 
-@test ThCategory.Ob(-1; model=FinSetC()) == -1
-@test ThCategory.Hom([1,2,3], 3, 3; model=FinSetC()) == [1,2,3]
-@test_throws TypeCheckFail ThCategory.Hom([1,2,3], 3, 2; model=FinSetC())
+using .ThCategory
+
+@test Ob(-1; model=FinSetC()) == -1
+@test Hom([1,2,3], 3, 3; model=FinSetC()) == [1,2,3]
+@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
 
 try
   ThCategory.Hom([1,2,3], 3, 2; model=FinSetC())
@@ -44,14 +46,14 @@ catch e
   @test sprint(showerror, e) isa String
 end
 
-@test_throws TypeCheckFail ThCategory.Hom([1,2,3], 3, 2; model=FinSetC())
-@test_throws TypeCheckFail ThCategory.Hom([1,2,3], 2, 3; model=FinSetC())
-@test ThCategory.compose([1,3,2], [1,3,2]; model=FinSetC()) == [1,2,3]
+@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
+@test_throws TypeCheckFail Hom([1,2,3], 2, 3; model=FinSetC())
+@test compose([1,3,2], [1,3,2]; model=FinSetC()) == [1,2,3]
 
-@test ThCategory.id(2; model=FinSetC()) == [1,2]
+@test id(2; model=FinSetC()) == [1,2]
 
-@test ThCategory.dom([1,2,3]; model=FinSetC()) == 3
-@test_throws ErrorException ThCategory.codom([1,2,3]; model=FinSetC())
+@test dom([1,2,3]; model=FinSetC()) == 3
+@test_throws ErrorException codom([1,2,3]; model=FinSetC())
 
 @test implements(FinSetC(), ThCategory)
 
@@ -83,10 +85,25 @@ end
 @struct_hash_equal struct FinFunction 
   values::Vector{Int}
   dom::FinSet 
-  codom::FinSet 
+  codom::FinSet
+  function FinFunction(values::AbstractVector, dom::FinSet, codom::FinSet)
+    new(ThCategory.Hom(Vector{Int}(values), dom.n, codom.n; model=FinSetC()), dom, codom)
+  end
 end 
 
 @instance ThCategory{FinSet, FinFunction} begin
+  Ob(x::FinSet) = x.n ≥ 0 ? x : @fail "expected nonnegative integer"
+
+  function Hom(f::FinFunction, x::FinSet, y::FinSet)
+    dom(f) == x || @fail "domain mismatch"
+    codom(f) == y || @fail "codomain mismatch"
+    f
+  end
+
+  function Hom(values::Vector{Int}, dom::FinSet, codom::FinSet)
+    FinFunction(values, dom, codom)
+  end
+
   dom(f::FinFunction) = f.dom 
   codom(f::FinFunction) = f.codom
   
@@ -100,6 +117,9 @@ f = FinFunction([2,3],A,B)
 g = FinFunction([1,1,1],B,A)
 @test id(A) == FinFunction([1,2], A, A)
 @test compose(f,g) == FinFunction([1,1], A, A)
+@test Hom(f, A, B) == f
+@test Hom([2,3], A, B) == f
+@test_throws TypeCheckFail Hom(f, A, A)
 
 @withmodel FinSetC() (mcompose, id) begin
   @test mcompose(id(2), id(2); context=(;B₁=2)) == id(4)
diff --git a/test/models/SymbolicModels.jl b/test/models/SymbolicModels.jl
index fb51a0db..00867257 100644
--- a/test/models/SymbolicModels.jl
+++ b/test/models/SymbolicModels.jl
@@ -9,6 +9,7 @@ abstract type ObExpr{T} <: CategoryExpr{T} end
 abstract type HomExpr{T} <: CategoryExpr{T} end
 
 @symbolic_model FreeCategory{ObExpr, HomExpr} ThCategory begin
+  compose(f::Hom, g::Hom) = associate_unit(new(f,g), ThCategory.id)
 end
 
 x, y = FreeCategory.Ob{:generator}([:x], []), FreeCategory.Ob{:generator}([:y], [])
@@ -16,13 +17,382 @@ f = FreeCategory.Hom{:generator}([:f], [x, y])
 
 @test x isa ObExpr{:generator}
 @test ThCategory.id(x) isa HomExpr{:id}
-@test ThCategory.compose(ThCategory.id(x), f) isa HomExpr{:compose}
-@test_throws SyntaxDomainError ThCategory.compose(f, f)
+@test ThCategory.compose(ThCategory.id(x), f) == f
+
+# Monoid
+########
+
+""" Theory of monoids.
+"""
+@theory ThMonoid begin
+  Elem::TYPE
+  munit()::Elem
+  mtimes(x::Elem,y::Elem)::Elem
+end
+
+""" Syntax for the theory of monoids.
+"""
+@symbolic_model FreeMonoid{GATExpr} ThMonoid
+
+import .ThMonoid: Elem
+using .ThMonoid
+
+Elem(mod::Module, args...) = Elem(mod.Elem, args...)
+
+@test isa(FreeMonoid, Module)
+# @test occursin("theory of monoids", string(Docs.doc(FreeMonoid)))
+# @test sort(names(FreeMonoid)) == sort([:FreeMonoid, :Elem])
+
+x, y, z = Elem(FreeMonoid,:x), Elem(FreeMonoid,:y), Elem(FreeMonoid,:z)
+@test nameof(x) == :x
+@test isa(mtimes(x,y), FreeMonoid.Elem)
+@test isa(munit(FreeMonoid.Elem), FreeMonoid.Elem)
+@test gat_typeof(x) == :Elem
+@test gat_typeof(mtimes(x,y)) == :Elem
+@test mtimes(mtimes(x,y),z) != mtimes(x,mtimes(y,z))
+
+# # Test equality
+@test x == Elem(FreeMonoid,:x)
+@test x != y
+@test Elem(FreeMonoid,"X") == Elem(FreeMonoid,"X")
+@test Elem(FreeMonoid,"X") != Elem(FreeMonoid,"Y")
+
+# Test hash
+@test hash(x) == hash(x)
+@test hash(x) != hash(y)
+@test hash(mtimes(x,y)) == hash(mtimes(x,y))
+@test hash(mtimes(x,y)) != hash(mtimes(x,z))
+
+@symbolic_model FreeMonoidAssoc{GATExpr} ThMonoid begin
+  mtimes(x::Elem, y::Elem) = associate(new(x,y))
+end
+
+x, y, z = [ Elem(FreeMonoidAssoc,sym) for sym in [:x,:y,:z] ]
+e = munit(FreeMonoidAssoc.Elem)
+@test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z))
+@test mtimes(e,x) != x && mtimes(x,e) != x
+
+@symbolic_model FreeMonoidAssocUnit{GATExpr} ThMonoid begin
+  mtimes(x::Elem, y::Elem) = associate_unit(new(x,y), munit)
+end
+
+x, y, z = [ Elem(FreeMonoidAssocUnit,sym) for sym in [:x,:y,:z] ]
+e = munit(FreeMonoidAssocUnit.Elem)
+@test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z))
+@test mtimes(e,x) == x && mtimes(x,e) == x
+
+abstract type MonoidExpr{T} <: GATExpr{T} end
+@symbolic_model FreeMonoidTyped{MonoidExpr} ThMonoid
+
+x = Elem(FreeMonoidTyped.Elem, :x)
+@test FreeMonoidTyped.Elem <: MonoidExpr
+@test isa(x, FreeMonoidTyped.Elem) && isa(x, MonoidExpr)
+
+# @signature ThMonoidNumeric{Elem} <: ThMonoid{Elem} begin
+#   elem_int(x::Int)::Elem
+# end
+
+# @syntax FreeMonoidNumeric ThMonoidNumeric
+
+# x = elem_int(FreeMonoidNumeric.Elem, 1)
+# @test isa(x, FreeMonoidNumeric.Elem)
+# @test first(x) == 1
+
+""" A monoid with two distinguished elements.
+"""
+@theory ThMonoidTwo <: ThMonoid begin
+  one()::Elem
+  two()::Elem
+end
+
+""" The free monoid on two generators.
+"""
+# @symbolic_model FreeMonoidTwo{GATExpr} ThMonoidTwo begin
+#   Elem(::Type{Elem}, value) = error("No extra generators allowed!")
+# end
+
+# x, y = one(FreeMonoidTwo.Elem), two(FreeMonoidTwo.Elem)
+# @test all(isa(expr, FreeMonoidTwo.Elem) for expr in [x, y, mtimes(x,y)])
+# @test_throws ErrorException Elem(FreeMonoidTwo, :x)
+
+# Category
+##########
+
+module CatTests
+
+using GATlab, Test
+
+@theory ThCategory begin
+  Ob::TYPE
+  Hom(dom::Ob, codom::Ob)::TYPE
+
+  id(X::Ob)::Hom(X,X)
+  compose(f::Hom(X,Y), g::Hom(Y,Z))::Hom(X,Z) ⊣ [X::Ob, Y::Ob, Z::Ob]
+end
+
+@symbolic_model FreeCategory{GATExpr, GATExpr} ThCategory begin
+  compose(f::Hom, g::Hom) = associate(new(f,g))
+end
+
+@test isa(FreeCategory, Module)
+@test sort(names(FreeCategory)) == sort([:FreeCategory, :Ob, :Hom])
+
+using .ThCategory
+
+X, Y, Z, W = [ Ob(FreeCategory.Ob, sym) for sym in [:X, :Y, :Z, :W] ]
+f, g, h = Hom(:f, X, Y), Hom(:g, Y, Z), Hom(:h, Z, W)
+@test isa(X, FreeCategory.Ob) && isa(f, FreeCategory.Hom)
+@test_throws MethodError FreeCategory.Hom(:f)
+@test dom(f) == X
+@test codom(f) == Y
+
+@test isa(id(X), FreeCategory.Hom)
+@test dom(id(X)) == X
+@test codom(id(X)) == X
+
+@test isa(compose(f,g), FreeCategory.Hom)
+@test dom(compose(f,g)) == X
+@test codom(compose(f,g)) == Z
+@test isa(compose(f,f), FreeCategory.Hom) # Doesn't check domains.
+@test compose(compose(f,g),h) == compose(f,compose(g,h))
+
+@symbolic_model FreeCategoryStrict{GATExpr, GATExpr} ThCategory begin
+  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
+end
+
+X, Y = Ob(FreeCategoryStrict.Ob, :X), Ob(FreeCategoryStrict.Ob, :Y)
+f, g = Hom(:f, X, Y), Hom(:g, Y, X)
+
+@test isa(compose(f,g), FreeCategoryStrict.Hom)
+@test_throws SyntaxDomainError compose(f,f)
 
 try
-  ThCategory.compose(f, f)
+  compose(f,f)
 catch e
-  @test sprint(show, e) isa String
+  @test sprint(showerror, e) isa String
+end
+
+end
+
+# Functor
+#########
+
+@instance ThMonoid{String} begin
+  munit(::Type{String}) = ""
+  mtimes(x::String, y::String) = string(x,y)
 end
 
+F(expr; kw...) = functor((String,), expr; kw...)
+
+x, y, z = Elem(FreeMonoid,:x), Elem(FreeMonoid,:y), Elem(FreeMonoid,:z)
+gens = Dict(x => "x", y => "y", z => "z")
+@test F(mtimes(x,mtimes(y,z)); generators=gens) == "xyz"
+@test F(mtimes(x,munit(FreeMonoid.Elem)); generators=gens) == "x"
+
+terms = Dict(:Elem => (x) -> string(first(x)))
+@test F(mtimes(x,mtimes(y,z)); terms=terms) == "xyz"
+@test F(mtimes(x,munit(FreeMonoid.Elem)); terms=terms) == "x"
+
+# Serialization
+###############
+
+using .ThCategory
+ThCategory.Ob(m::Module, x) = Ob(m.Ob, x)
+
+# To JSON
+X, Y, Z = [ Ob(FreeCategory.Ob, sym) for sym in [:X, :Y, :Z] ]
+f = Hom(:f, X, Y)
+g = Hom(:g, Y, Z)
+@test to_json_sexpr(X) == ["Ob", "X"]
+@test to_json_sexpr(f) == ["Hom", "f", ["Ob", "X"], ["Ob", "Y"]]
+@test to_json_sexpr(compose(f,g)) == [
+  "compose",
+  ["Hom", "f", ["Ob", "X"], ["Ob", "Y"]],
+  ["Hom", "g", ["Ob", "Y"], ["Ob", "Z"]],
+]
+@test to_json_sexpr(f, by_reference=x->true) == "f"
+@test to_json_sexpr(compose(f,g), by_reference=x->true) == ["compose","f","g"]
+@test to_json_sexpr(true)
+
+# From JSON
+@test parse_json_sexpr(FreeMonoid, [:Elem, "x"]) == Elem(FreeMonoid, :x)
+@test parse_json_sexpr(FreeMonoid, [:munit]) == munit(FreeMonoid.Elem)
+@test parse_json_sexpr(FreeCategory, ["Ob", "X"]) == X
+@test parse_json_sexpr(FreeCategory, ["Ob", "X"]; symbols=false) ==
+  Ob(FreeCategory.Ob, "X")
+@test parse_json_sexpr(FreeCategory, ["Hom", "f", ["Ob", "X"], ["Ob", "Y"]]) == f
+@test parse_json_sexpr(FreeCategory, ["Hom", "f", ["Ob", "X"], ["Ob", "Y"]]; symbols=false) ==
+  Hom("f", Ob(FreeCategory.Ob, "X"), Ob(FreeCategory.Ob, "Y"))
+@test parse_json_sexpr(FreeCategory, ["Ob", true]) == Ob(FreeCategory, true)
+@test_throws ErrorException parse_json_sexpr(FreeCategory, "X")
+
+# Round trip
+@test parse_json_sexpr(FreeCategory, to_json_sexpr(compose(f,g))) == compose(f,g)
+@test parse_json_sexpr(FreeCategory, to_json_sexpr(id(X))) == id(X)
+
+# Pretty Printing
+#################
+
+sexpr(expr::GATExpr) = sprint(show_sexpr, expr)
+unicode(expr::GATExpr; all::Bool=false) =
+  all ? sprint(show, MIME("text/plain"), expr) : sprint(show_unicode, expr)
+latex(expr::GATExpr; all::Bool=false) =
+  all ? sprint(show, MIME("text/latex"), expr) : sprint(show_latex, expr)
+
+# Monoids
+
+x, y, z = Elem.(Ref(FreeMonoid), [:x, :y, :z])
+
+@test sexpr(mtimes(x,y)) == "(mtimes :x :y)"
+@test unicode(mtimes(x,y)) == "mtimes{x,y}"
+@test latex(mtimes(x, y)) == raw"\mathop{\mathrm{mtimes}}\left[x,y\right]"
+
+# Categories
+
+
+A, B = Ob(FreeCategory, :A), Ob(FreeCategory, :B)
+f, g = Hom(:f, A, B), Hom(:g, B, A)
+
+ThCategory.compose(f, g, h...) = compose(f, compose(g, h...))
+
+import .SymbolicModels: show_unicode, show_latex
+
+show_unicode(io::IO, expr::CategoryExpr{:compose}; kw...) =
+  show_unicode_infix(io, expr, "⋅"; kw...)
+
+show_latex(io::IO, expr::CategoryExpr{:id}; kw...) =
+  show_latex_script(io, expr, "\\mathrm{id}")
+show_latex(io::IO, expr::CategoryExpr{:compose}; paren::Bool=false, kw...) =
+  show_latex_infix(io, expr, "\\cdot"; paren=paren)
+
+function Base.show(io::IO, ::MIME"text/plain", expr::HomExpr)
+  show_unicode(io, expr)
+  print(io, ": ")
+  show_unicode(io, dom(expr))
+  print(io, " → ")
+  show_unicode(io, codom(expr))
+end
+
+function Base.show(io::IO, ::MIME"text/latex", expr::HomExpr)
+  print(io, "\$")
+  show_latex(io, expr)
+  print(io, " : ")
+  show_latex(io, dom(expr))
+  print(io, " \\to ")
+  show_latex(io, codom(expr))
+  print(io, "\$")
+end
+
+# String format
+@test string(A) == "A"
+@test string(f) == "f"
+@test string(compose(f,g)) == "compose(f,g)"
+@test string(compose(f,g,f)) == "compose(f,g,f)"
+@test string(Ob(FreeCategory, nothing)) != ""
+
+# S-expressions
+@test sexpr(A) == ":A"
+@test sexpr(f) == ":f"
+@test sexpr(compose(f,g)) == "(compose :f :g)"
+@test sexpr(compose(f,g,f)) == "(compose :f :g :f)"
+
+# Infix notation (Unicode)
+@test unicode(A) == "A"
+@test unicode(A, all=true) == "A"
+@test unicode(f) == "f"
+@test unicode(f, all=true) == "f: A → B"
+@test unicode(id(A)) == "id{A}"
+@test unicode(compose(f,g)) == "f⋅g"
+
+# Infix notation (LaTeX)
+@test latex(A) == "A"
+@test latex(A, all=true) == raw"$A$"
+@test latex(f) == "f"
+@test latex(f, all=true) == raw"$f : A \to B$"
+@test latex(id(A)) == "\\mathrm{id}_{A}"
+@test latex(compose(f,g)) == "f \\cdot g"
+
+@test latex(Ob(FreeCategory, "x")) == "x"
+@test latex(Ob(FreeCategory, "sin")) == "\\mathrm{sin}"
+@test latex(Ob(FreeCategory, "\\alpha")) == "\\alpha"
+
+@test sprint(show_latex_postfix, id(A), "i") == "{A}i"
+
+# Groupoid
+
+""" Theory of *groupoids*.
+"""
+@theory ThGroupoid <: ThCategory begin
+  invert(f::(A → B))::(B → A) ⊣ [A::Ob, B::Ob]
+
+  (f ⋅ invert(f) == id(A)) :: Hom(A, A) ⊣ [A::Ob, B::Ob, f::(A → B)]
+  (invert(f) ⋅ f == id(B)) :: Hom(B, B) ⊣ [A::Ob, B::Ob, f::(A → B)]
+end
+
+using .ThGroupoid
+
+@symbolic_model FreeGroupoid{ObExpr,HomExpr} ThGroupoid begin
+  compose(f::Hom, g::Hom) = associate_unit_inv(new(f,g; strict=true), id, invert)
+  invert(f::Hom) = distribute_unary(involute(new(f)), invert, compose,
+                                 unit=id, contravariant=true)
+end
+
+A, B, C = Ob(FreeGroupoid, :A), Ob(FreeGroupoid, :B), Ob(FreeGroupoid, :C)
+f, g, h, k = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, B, A), Hom(:k, C, B)
+
+# Domains and codomains
+@test dom(invert(f)) == B
+@test codom(invert(f)) == A
+
+# Associativity and unitality
+@test compose(compose(f,g),k) == compose(f,compose(g,k))
+@test compose(id(A), f) == f
+@test compose(f, id(B)) == f
+
+# Inverse laws
+@test compose(f,invert(f)) == id(A)
+@test compose(invert(f),f) == id(B)
+@test compose(invert(f),compose(f,g)) == g
+@test compose(h,compose(invert(h),g)) == g
+@test compose(compose(f,g),invert(g)) == f
+@test compose(compose(k,invert(f)),f) == k
+@test compose(compose(f,invert(k)),compose(k,invert(f))) == id(A)
+
+# Inverses and composition
+@test invert(compose(f,g)) == compose(invert(g),invert(f))
+@test invert(id(A)) == id(A)
+
+# Involution
+@test invert(invert(f)) == f
+
+# PointedSetCategory
+
+"""
+Theory of a pointed set-enriched category.
+We axiomatize a category equipped with zero morphisms.
+
+A functor from an ordinary category into a freely generated
+pointed-set enriched category,
+equivalently, a pointed-set enriched category in which no two nonzero maps
+compose to a zero map, is a good notion
+of a functor that's total on objects and partial on morphisms.
+"""
+@theory ThPointedSetCategory <: ThCategory begin
+  zeromap(A::Ob,B::Ob)::Hom(A,B)
+  (compose(zeromap(A,B),f::(B→C))==zeromap(A,C)) :: Hom(A, C) ⊣ [A::Ob,B::Ob,C::Ob]
+  (compose(g::(A→B),zeromap(A,B))==zeromap(A,C)) :: Hom(A, C) ⊣ [A::Ob,B::Ob,C::Ob]
+end
+
+@symbolic_model FreePointedSetCategory{ObExpr,HomExpr} ThPointedSetCategory begin
+  compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id)
+end
+
+using .ThPointedSetCategory
+
+A,B,C,D = map(x->Ob(FreePointedSetCategory,x),[:A,:B,:C,:D])
+f,g,h = Hom(:f,A,B),Hom(:g,B,C),Hom(:h,C,D)
+zAB,zBC,zAC = zeromap(A,B),zeromap(B,C),zeromap(A,C)
+@test zAC == compose(f,zBC) == compose(zAB,g)
+@test compose(f,zBC,h) == zeromap(A,D)
+
 end
diff --git a/test/stdlib/models/ScopeTrees.jl b/test/stdlib/models/ScopeTrees.jl
deleted file mode 100644
index 4e2c0b81..00000000
--- a/test/stdlib/models/ScopeTrees.jl
+++ /dev/null
@@ -1,45 +0,0 @@
-module TestScopeTrees
-
-using Test, GATlab
-
-t = wrap(
-  :a => pure(1),
-  :b => wrap(:x => pure(2), :y => pure(1)),
-  :c => wrap(:f => wrap(:g => pure(4)))
-)
-
-r = fromexpr(t, :(c.f.g), Reference)
-
-@test toexpr(t, r) == :(c.f.g)
-
-@test isnode(t)
-@test unwrap(t) isa Scope
-@test isleaf(getvalue(t, :a))
-@test unwrap(getvalue(t, :a)) == 1
-@test nameof.(first.(keys(t))) == [:a, :b, :b, :c]
-@test keys(t)[3] == fromexpr(t, :(b.y), Reference)
-@test haskey(t, r)
-@test t[r] == 4
-@test_throws KeyError t[fromexpr(t, :(c.f), Reference)]
-@test_throws KeyError t[fromexpr(t, :(_), Reference)]
-
-using .ThCategory
-
-t1 = wrap(:a => pure(1), :b => pure(1), :c => pure(2))
-t2 = wrap(:x => wrap(:p => pure(3), :q => pure(2)), :y => pure(7))
-a, b, c = fromexpr.(Ref(t1), [:a, :b, :c], Ref(Reference))
-xp, xq, y = fromexpr.(Ref(t2), [:(x.p), :(x.q), :y], Ref(Reference))
-f = ScopeTreeHom(a => (y, [6]), b => (xp, [2]), c => (xq, [2,2]))
-id_t1 = ScopeTreeHom(a => (a, [1]), b => (b, [1]), c => (c, [1,2]))
-
-@withmodel ScopeTreeC(FinSetC()) (Ob, Hom, compose, id) begin
-  @test Ob(t) == t
-  @test_throws TypeCheckFail Ob(wrap(:x => pure(-1)))
-  @test Hom(f, t1, t2) == f
-  @test_throws TypeCheckFail Hom(f, t1, t1)
-  @test_throws TypeCheckFail Hom(ScopeTreeHom(a => (a, [2]), b => (b, [1]), c => (c, [1,2])), t1, t2)
-  @test id(t1) == id_t1
-  @test compose(id(t1), f) == f
-end
-
-end
diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl
index eff8aa21..6e7e807a 100644
--- a/test/stdlib/models/tests.jl
+++ b/test/stdlib/models/tests.jl
@@ -4,7 +4,6 @@ include("FinSets.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Nothings.jl")
-include("ScopeTrees.jl")
 include("GATs.jl")
 
 end
diff --git a/test/syntax/ExprInterop.jl b/test/syntax/ExprInterop.jl
index a71466ee..706ed4cf 100644
--- a/test/syntax/ExprInterop.jl
+++ b/test/syntax/ExprInterop.jl
@@ -27,10 +27,4 @@ c = ScopeList([scope, scope′])
 @test fromexpr(c, :(var"#1!1"), Ident) == x
 @test fromexpr(c, :(var"#1"), Ident) == x′
 
-@test toexpr(c, Reference(x)) == :x!1
-@test fromexpr(c, :x!1, Reference) == Reference(x)
-
-@test toexpr(c, Reference()) == :(_)
-@test fromexpr(c, :(_), Reference) == Reference()
-
 end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 610c0126..e374ecc8 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -11,7 +11,7 @@ end
 
 scope = Scope(:number, :(+), :(*))
 
-number, plus, times = Reference.(idents(scope; name=[:number, :(+), :(*)]))
+number, plus, times = idents(scope; name=[:number, :(+), :(*)])
 
 one = AlgTerm(Constant(1, AlgType(number)))
 
diff --git a/test/syntax/Presentations.jl b/test/syntax/Presentations.jl
index eddee259..678adb9b 100644
--- a/test/syntax/Presentations.jl
+++ b/test/syntax/Presentations.jl
@@ -40,7 +40,7 @@ end
 src, tgt = idents(SchGraph; name=[:src, :tgt])
 Hom = ident(SchGraph; name=:Hom)
 
-@test getvalue(SchGraph[src]).head == Reference(Hom)
+@test getvalue(SchGraph[src]).head == Hom
 
 @present Z(ThGroup) begin
   (a,)
@@ -49,7 +49,7 @@ end
 t = fromexpr(Z, :(i(a) ⋅ (2::default)), AlgTerm)
 a = ident(Z; name=:a)
 
-@test compile(ThGroup, Dict(Reference(a) => :a), t) == :($(ThGroup).:(⋅)($(ThGroup).i(a), 2))
+@test compile(Dict(a => :a), t; theorymodule=ThGroup) == :($(ThGroup).:(⋅)($(ThGroup).i(a), 2))
 
 @present D₄(ThGroup) begin
   (r,f) :: default
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index 3c61b04d..f55f00bd 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -54,32 +54,7 @@ nameless = Ident(tag1, LID(1), nothing)
 
 @test gettag(retag(Dict(tag1 => tag2), x)) == tag2
 @test nameof(rename(tag1, Dict(:x => :y), x)) == :y
-
-# References
-############
-@test_throws ArgumentError only(Reference())
-@test basicprinted(Reference()) == "_"
-
-y = Ident(tag2, LID(1), :y)
-xdoty = Reference(x, Reference(y))
-@test xdoty == Reference(x,y)
-
-@test first(xdoty) == x
-@test rest(xdoty) == Reference(y)
-@test_throws ArgumentError only(xdoty)
-@test only(Reference(x)) == x
-
-@test basicprinted(xdoty) == "x.y"
-
-xsub1 = Reference(x, nameless)
-
-@test basicprinted(xsub1) == "x[1]"
-
-@test gettag(first(retag(Dict(tag1 => tag2), xdoty))) == tag2
-@test gettag(first(retag(Dict(tag2 => tag2), xdoty))) == tag1
-@test gettag(first(rest(retag(Dict(tag2 => tag1), xdoty)))) == tag1
-@test basicprinted(rename(tag1, Dict(:x => :y, :y => :z), xdoty)) == "y.y"
-@test basicprinted(rename(tag2, Dict(:x => :y, :y => :z), xdoty)) == "x.z"
+@test rename(tag1, Dict{Symbol, Symbol}(), x) == x
 
 # Bindings
 ##########
@@ -144,6 +119,8 @@ xy_scope′ = Scope([bind_x]; tag=tag1)
 @test hasident(xy_scope, x)
 @test !hasident(xy_scope; tag=tag1)
 
+value_scope = Scope{Union{Int, String}}(:x => 1, :y => 1) isa Scope{Union{Int, String}}
+
 s = Scope{String, Int}()
 
 bind_x_typed = Binding{String, Int}(:x, Set([:x]), "ex", 2)